1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Ultima modifica: 05/08/2009 *)
21 (* ********************************************************************** *)
23 include "common/nat.ma".
24 include "num/bool_lemmas.ma".
30 nlemma nat_destruct_S_S : ∀n1,n2:nat.S n1 = S n2 → n1 = n2.
32 nchange with (match S n2 with [ O ⇒ False | S a ⇒ n1 = a ]);
38 nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
40 nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
46 nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
48 nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
54 nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
61 ##[ ##1: napply refl_eq
62 ##| ##2: #n3; #H; napply refl_eq
64 ##| ##2: #n2; #H; #n3;
68 ##[ ##1: napply refl_eq
69 ##| ##2: #n4; napply (H n4)
74 nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
80 ##[ ##1: #H; napply refl_eq
81 ##| ##2: #n3; #H; #H1; nelim (nat_destruct_0_S ? H1)
83 ##| ##2: #n2; #H; #n3; #H1;
84 ncases n3 in H1:(%) ⊢ %;
86 ##[ ##1: #H1; nelim (nat_destruct_S_0 ? H1)
88 napply (H n4 (nat_destruct_S_S … H1))
93 nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
99 ##[ ##1: #H; napply refl_eq
100 ##| ##2: #n3; #H; #H1; napply (bool_destruct … (O = S n3) H1)
102 ##| ##2: #n2; #H; #n3; #H1;
103 ncases n3 in H1:(%) ⊢ %;
105 ##[ ##1: #H1; napply (bool_destruct … (S n2 = O) H1)
107 nrewrite > (H n4 H1);
113 nlemma decidable_nat : ∀x,y:nat.decidable (x = y).
114 #x; nelim x; nnormalize;
115 ##[ ##1: #y; ncases y;
116 ##[ ##1: napply (or2_intro1 (O = O) (O ≠ O) (refl_eq …))
117 ##| ##2: #n2; napply (or2_intro2 (O = (S n2)) (O ≠ (S n2)) ?);
118 nnormalize; #H; napply (nat_destruct_0_S n2 H)
120 ##| ##2: #n1; #H; #y; ncases y;
121 ##[ ##1: napply (or2_intro2 ((S n1) = O) ((S n1) ≠ O) ?);
122 nnormalize; #H1; napply (nat_destruct_S_0 n1 H1)
123 ##| ##2: #n2; napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (H n2) …);
124 ##[ ##1: #H1; napply (or2_intro1 (? = ?) (? ≠ ?) …);
125 nrewrite > H1; napply refl_eq
126 ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) …);
127 nnormalize; #H2; napply (H1 (nat_destruct_S_S … H2))
133 nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false.
135 ##[ ##1: #n2; ncases n2;
136 ##[ ##1: nnormalize; #H; nelim (H (refl_eq …))
137 ##| ##2: #nn2; #H; nnormalize; napply refl_eq
139 ##| ##2: #nn1; #H; #n2; ncases n2;
140 ##[ ##1: #H1; nnormalize; napply refl_eq
141 ##| ##2: #nn2; nnormalize; #H1;
142 napply (H nn2 ?); nnormalize; #H2;
143 nrewrite > H2 in H1:(%); #H1;
144 napply (H1 (refl_eq …))
149 nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2).
151 ##[ ##1: #n2; ncases n2;
152 ##[ ##1: nnormalize; #H; napply (bool_destruct … H)
153 ##| ##2: #nn2; nnormalize; #H; #H1; nelim (nat_destruct_0_S … H1)
155 ##| ##2: #nn1; #H; #n2; ncases n2;
156 ##[ ##1: nnormalize; #H1; #H2; nelim (nat_destruct_S_0 … H2)
157 ##| ##2: #nn2; nnormalize; #H1; #H2; napply (H nn2 H1 ?);
158 napply (nat_destruct_S_S … H2)
163 nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
166 ##[ ##1: nnormalize; #n2; napply refl_eq
167 ##| ##2: #n; #H; #n2; nrewrite > (H n2);
168 ncases n in H:(%) ⊢ %;
169 ##[ ##1: nnormalize; #H; napply refl_eq
170 ##| ##2: #n3; nnormalize; #H; napply refl_eq
175 nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2).
178 ##[ ##1: nnormalize; #n2; napply refl_eq
179 ##| ##2: #n; #H; #n2;
180 nrewrite > (Sn_p_n_to_S_npn n (S n2));
186 nlemma Opn_to_n : ∀n.O + n = n.
187 #n; nnormalize; napply refl_eq.
190 nlemma npO_to_n : ∀n.n + O = n.
193 ##[ ##1: nnormalize; napply refl_eq
195 nrewrite > (Sn_p_n_to_S_npn n1 O);
201 nlemma symmetric_plusnat : symmetricT nat nat plus.
204 ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply refl_eq
205 ##| ##2: #n2; #H; #n3;
206 nrewrite > (Sn_p_n_to_S_npn n2 n3);
207 nrewrite > (n_p_Sn_to_S_npn n3 n2);