← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Numbers/Natural/Abstract/NAdd.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Numbers/Natural/Abstract/NAdd.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
(*                      Evgeny Makarov, INRIA, 2007                     *)
 
9
(************************************************************************)
 
10
 
 
11
(*i $Id: NAdd.v 11674 2008-12-12 19:48:40Z letouzey $ i*)
 
12
 
 
13
Require Export NBase.
 
14
 
 
15
Module NAddPropFunct (Import NAxiomsMod : NAxiomsSig).
 
16
Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
 
17
 
 
18
Open Local Scope NatScope.
 
19
 
 
20
Theorem add_wd :
 
21
  forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2.
 
22
Proof NZadd_wd.
 
23
 
 
24
Theorem add_0_l : forall n : N, 0 + n == n.
 
25
Proof NZadd_0_l.
 
26
 
 
27
Theorem add_succ_l : forall n m : N, (S n) + m == S (n + m).
 
28
Proof NZadd_succ_l.
 
29
 
 
30
(** Theorems that are valid for both natural numbers and integers *)
 
31
 
 
32
Theorem add_0_r : forall n : N, n + 0 == n.
 
33
Proof NZadd_0_r.
 
34
 
 
35
Theorem add_succ_r : forall n m : N, n + S m == S (n + m).
 
36
Proof NZadd_succ_r.
 
37
 
 
38
Theorem add_comm : forall n m : N, n + m == m + n.
 
39
Proof NZadd_comm.
 
40
 
 
41
Theorem add_assoc : forall n m p : N, n + (m + p) == (n + m) + p.
 
42
Proof NZadd_assoc.
 
43
 
 
44
Theorem add_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q).
 
45
Proof NZadd_shuffle1.
 
46
 
 
47
Theorem add_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p).
 
48
Proof NZadd_shuffle2.
 
49
 
 
50
Theorem add_1_l : forall n : N, 1 + n == S n.
 
51
Proof NZadd_1_l.
 
52
 
 
53
Theorem add_1_r : forall n : N, n + 1 == S n.
 
54
Proof NZadd_1_r.
 
55
 
 
56
Theorem add_cancel_l : forall n m p : N, p + n == p + m <-> n == m.
 
57
Proof NZadd_cancel_l.
 
58
 
 
59
Theorem add_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
 
60
Proof NZadd_cancel_r.
 
61
 
 
62
(* Theorems that are valid for natural numbers but cannot be proved for Z *)
 
63
 
 
64
Theorem eq_add_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
 
65
Proof.
 
66
intros n m; induct n.
 
67
(* The next command does not work with the axiom add_0_l from NAddSig *)
 
68
rewrite add_0_l. intuition reflexivity.
 
69
intros n IH. rewrite add_succ_l.
 
70
setoid_replace (S (n + m) == 0) with False using relation iff by
 
71
 (apply -> neg_false; apply neq_succ_0).
 
72
setoid_replace (S n == 0) with False using relation iff by
 
73
 (apply -> neg_false; apply neq_succ_0). tauto.
 
74
Qed.
 
75
 
 
76
Theorem eq_add_succ :
 
77
  forall n m : N, (exists p : N, n + m == S p) <->
 
78
                    (exists n' : N, n == S n') \/ (exists m' : N, m == S m').
 
79
Proof.
 
80
intros n m; cases n.
 
81
split; intro H.
 
82
destruct H as [p H]. rewrite add_0_l in H; right; now exists p.
 
83
destruct H as [[n' H] | [m' H]].
 
84
symmetry in H; false_hyp H neq_succ_0.
 
85
exists m'; now rewrite add_0_l.
 
86
intro n; split; intro H.
 
87
left; now exists n.
 
88
exists (n + m); now rewrite add_succ_l.
 
89
Qed.
 
90
 
 
91
Theorem eq_add_1 : forall n m : N,
 
92
  n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
 
93
Proof.
 
94
intros n m H.
 
95
assert (H1 : exists p : N, n + m == S p) by now exists 0.
 
96
apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
 
97
left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
 
98
apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
 
99
right. rewrite H1 in H; rewrite add_succ_r in H; apply succ_inj in H.
 
100
apply -> eq_add_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
 
101
Qed.
 
102
 
 
103
Theorem succ_add_discr : forall n m : N, m ~= S (n + m).
 
104
Proof.
 
105
intro n; induct m.
 
106
apply neq_sym. apply neq_succ_0.
 
107
intros m IH H. apply succ_inj in H. rewrite add_succ_r in H.
 
108
unfold not in IH; now apply IH.
 
109
Qed.
 
110
 
 
111
Theorem add_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).
 
112
Proof.
 
113
intros n m; cases n.
 
114
intro H; now elim H.
 
115
intros n IH; rewrite add_succ_l; now do 2 rewrite pred_succ.
 
116
Qed.
 
117
 
 
118
Theorem add_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m).
 
119
Proof.
 
120
intros n m H; rewrite (add_comm n (P m));
 
121
rewrite (add_comm n m); now apply add_pred_l.
 
122
Qed.
 
123
 
 
124
(* One could define n <= m as exists p : N, p + n == m. Then we have
 
125
dichotomy:
 
126
 
 
127
forall n m : N, n <= m \/ m <= n,
 
128
 
 
129
i.e.,
 
130
 
 
131
forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n)     (1)
 
132
 
 
133
We will need (1) in the proof of induction principle for integers
 
134
constructed as pairs of natural numbers. The formula (1) can be proved
 
135
using properties of order and truncated subtraction. Thus, p would be
 
136
m - n or n - m and (1) would hold by theorem sub_add from Sub.v
 
137
depending on whether n <= m or m <= n. However, in proving induction
 
138
for integers constructed from natural numbers we do not need to
 
139
require implementations of order and sub; it is enough to prove (1)
 
140
here. *)
 
141
 
 
142
Theorem add_dichotomy :
 
143
  forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n).
 
144
Proof.
 
145
intros n m; induct n.
 
146
left; exists m; apply add_0_r.
 
147
intros n IH.
 
148
destruct IH as [[p H] | [p H]].
 
149
destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H.
 
150
rewrite add_0_l in H. right; exists (S 0); rewrite H; rewrite add_succ_l; now rewrite add_0_l.
 
151
left; exists p'; rewrite add_succ_r; now rewrite add_succ_l in H.
 
152
right; exists (S p). rewrite add_succ_l; now rewrite H.
 
153
Qed.
 
154
 
 
155
End NAddPropFunct.
 
156