1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(* Evgeny Makarov, INRIA, 2007 *)
(************************************************************************)
(*i $Id$ i*)
Require Export NBase.
Module NPlusPropFunct (Import NAxiomsMod : NAxiomsSig).
Module Export NBasePropMod := NBasePropFunct NAxiomsMod.
Open Local Scope NatScope.
Theorem plus_wd :
forall n1 n2 : N, n1 == n2 -> forall m1 m2 : N, m1 == m2 -> n1 + m1 == n2 + m2.
Proof NZplus_wd.
Theorem plus_0_l : forall n : N, 0 + n == n.
Proof NZplus_0_l.
Theorem plus_succ_l : forall n m : N, (S n) + m == S (n + m).
Proof NZplus_succ_l.
(** Theorems that are valid for both natural numbers and integers *)
Theorem plus_0_r : forall n : N, n + 0 == n.
Proof NZplus_0_r.
Theorem plus_succ_r : forall n m : N, n + S m == S (n + m).
Proof NZplus_succ_r.
Theorem plus_comm : forall n m : N, n + m == m + n.
Proof NZplus_comm.
Theorem plus_assoc : forall n m p : N, n + (m + p) == (n + m) + p.
Proof NZplus_assoc.
Theorem plus_shuffle1 : forall n m p q : N, (n + m) + (p + q) == (n + p) + (m + q).
Proof NZplus_shuffle1.
Theorem plus_shuffle2 : forall n m p q : N, (n + m) + (p + q) == (n + q) + (m + p).
Proof NZplus_shuffle2.
Theorem plus_1_l : forall n : N, 1 + n == S n.
Proof NZplus_1_l.
Theorem plus_1_r : forall n : N, n + 1 == S n.
Proof NZplus_1_r.
Theorem plus_cancel_l : forall n m p : N, p + n == p + m <-> n == m.
Proof NZplus_cancel_l.
Theorem plus_cancel_r : forall n m p : N, n + p == m + p <-> n == m.
Proof NZplus_cancel_r.
(* Theorems that are valid for natural numbers but cannot be proved for Z *)
Theorem eq_plus_0 : forall n m : N, n + m == 0 <-> n == 0 /\ m == 0.
Proof.
intros n m; induct n.
(* The next command does not work with the axiom plus_0_l from NPlusSig *)
rewrite plus_0_l. intuition reflexivity.
intros n IH. rewrite plus_succ_l.
setoid_replace (S (n + m) == 0) with False using relation iff by
(apply -> neg_false; apply neq_succ_0).
setoid_replace (S n == 0) with False using relation iff by
(apply -> neg_false; apply neq_succ_0). tauto.
Qed.
Theorem eq_plus_succ :
forall n m : N, (exists p : N, n + m == S p) <->
(exists n' : N, n == S n') \/ (exists m' : N, m == S m').
Proof.
intros n m; cases n.
split; intro H.
destruct H as [p H]. rewrite plus_0_l in H; right; now exists p.
destruct H as [[n' H] | [m' H]].
symmetry in H; false_hyp H neq_succ_0.
exists m'; now rewrite plus_0_l.
intro n; split; intro H.
left; now exists n.
exists (n + m); now rewrite plus_succ_l.
Qed.
Theorem eq_plus_1 : forall n m : N,
n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
Proof.
intros n m H.
assert (H1 : exists p : N, n + m == S p) by now exists 0.
apply -> eq_plus_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
left. rewrite H1 in H; rewrite plus_succ_l in H; apply succ_inj in H.
apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H2 in H1; now split.
right. rewrite H1 in H; rewrite plus_succ_r in H; apply succ_inj in H.
apply -> eq_plus_0 in H. destruct H as [H2 H3]; rewrite H3 in H1; now split.
Qed.
Theorem succ_plus_discr : forall n m : N, m ~= S (n + m).
Proof.
intro n; induct m.
apply neq_symm. apply neq_succ_0.
intros m IH H. apply succ_inj in H. rewrite plus_succ_r in H.
unfold not in IH; now apply IH.
Qed.
Theorem plus_pred_l : forall n m : N, n ~= 0 -> P n + m == P (n + m).
Proof.
intros n m; cases n.
intro H; now elim H.
intros n IH; rewrite plus_succ_l; now do 2 rewrite pred_succ.
Qed.
Theorem plus_pred_r : forall n m : N, m ~= 0 -> n + P m == P (n + m).
Proof.
intros n m H; rewrite (plus_comm n (P m));
rewrite (plus_comm n m); now apply plus_pred_l.
Qed.
(* One could define n <= m as exists p : N, p + n == m. Then we have
dichotomy:
forall n m : N, n <= m \/ m <= n,
i.e.,
forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n) (1)
We will need (1) in the proof of induction principle for integers
constructed as pairs of natural numbers. The formula (1) can be proved
using properties of order and truncated subtraction. Thus, p would be
m - n or n - m and (1) would hold by theorem minus_plus from Minus.v
depending on whether n <= m or m <= n. However, in proving induction
for integers constructed from natural numbers we do not need to
require implementations of order and minus; it is enough to prove (1)
here. *)
Theorem plus_dichotomy :
forall n m : N, (exists p : N, p + n == m) \/ (exists p : N, p + m == n).
Proof.
intros n m; induct n.
left; exists m; apply plus_0_r.
intros n IH.
destruct IH as [[p H] | [p H]].
destruct (zero_or_succ p) as [H1 | [p' H1]]; rewrite H1 in H.
rewrite plus_0_l in H. right; exists (S 0); rewrite H; rewrite plus_succ_l; now rewrite plus_0_l.
left; exists p'; rewrite plus_succ_r; now rewrite plus_succ_l in H.
right; exists (S p). rewrite plus_succ_l; now rewrite H.
Qed.
End NPlusPropFunct.
|
