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 (* Sviluppo: 2008-2010 *)
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 ]);
39 nlemma nat_destruct_0_S : ∀n:nat.O = S n → False.
41 nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
48 nlemma nat_destruct_S_0 : ∀n:nat.S n = O → False.
50 nchange with (match S n with [ O ⇒ True | S a ⇒ False ]);
56 nlemma eq_to_eqnat : ∀n1,n2:nat.n1 = n2 → eq_nat n1 n2 = true.
62 ##[ ##1: #H; napply refl_eq
63 ##| ##2: #n3; #H; #H1; ndestruct (*nelim (nat_destruct_0_S ? H1)*)
65 ##| ##2: #n2; #H; #n3; #H1;
66 ncases n3 in H1:(%) ⊢ %;
68 ##[ ##1: #H1; ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
70 napply (H n4 (nat_destruct_S_S … H1))
75 nlemma neqnat_to_neq : ∀n1,n2:nat.(eq_nat n1 n2 = false → n1 ≠ n2).
77 napply (not_to_not (n1 = n2) (eq_nat n1 n2 = true) …);
78 ##[ ##1: napply (eq_to_eqnat n1 n2)
79 ##| ##2: napply (eqfalse_to_neqtrue … H)
83 nlemma eqnat_to_eq : ∀n1,n2:nat.(eq_nat n1 n2 = true → n1 = n2).
89 ##[ ##1: #H; napply refl_eq
90 ##| ##2: #n3; #H; #H1; ndestruct (*napply (bool_destruct … (O = S n3) H1)*)
92 ##| ##2: #n2; #H; #n3; #H1;
93 ncases n3 in H1:(%) ⊢ %;
95 ##[ ##1: #H1; ndestruct (*napply (bool_destruct … (S n2 = O) H1)*)
103 nlemma neq_to_neqnat : ∀n1,n2:nat.n1 ≠ n2 → eq_nat n1 n2 = false.
105 napply (neqtrue_to_eqfalse (eq_nat n1 n2));
106 napply (not_to_not (eq_nat n1 n2 = true) (n1 = n2) ? H);
107 napply (eqnat_to_eq n1 n2).
110 nlemma decidable_nat : ∀x,y:nat.decidable (x = y).
112 napply (or2_elim (eq_nat x y = true) (eq_nat x y = false) ? (decidable_bexpr ?));
113 ##[ ##1: #H; napply (or2_intro1 (x = y) (x ≠ y) (eqnat_to_eq … H))
114 ##| ##2: #H; napply (or2_intro2 (x = y) (x ≠ y) (neqnat_to_neq … H))
118 nlemma symmetric_eqnat : symmetricT nat bool eq_nat.
120 napply (or2_elim (n1 = n2) (n1 ≠ n2) ? (decidable_nat n1 n2));
121 ##[ ##1: #H; nrewrite > H; napply refl_eq
122 ##| ##2: #H; nrewrite > (neq_to_neqnat n1 n2 H);
123 napply (symmetric_eq ? (eq_nat n2 n1) false);
124 napply (neq_to_neqnat n2 n1 (symmetric_neq ? n1 n2 H))
128 nlemma Sn_p_n_to_S_npn : ∀n1,n2.(S n1) + n2 = S (n1 + n2).
131 ##[ ##1: nnormalize; #n2; napply refl_eq
132 ##| ##2: #n; #H; #n2; nrewrite > (H n2);
133 ncases n in H:(%) ⊢ %;
134 ##[ ##1: nnormalize; #H; napply refl_eq
135 ##| ##2: #n3; nnormalize; #H; napply refl_eq
140 nlemma n_p_Sn_to_S_npn : ∀n1,n2.n1 + (S n2) = S (n1 + n2).
143 ##[ ##1: nnormalize; #n2; napply refl_eq
144 ##| ##2: #n; #H; #n2;
145 nrewrite > (Sn_p_n_to_S_npn n (S n2));
151 nlemma Opn_to_n : ∀n.O + n = n.
152 #n; nnormalize; napply refl_eq.
155 nlemma npO_to_n : ∀n.n + O = n.
158 ##[ ##1: nnormalize; napply refl_eq
160 nrewrite > (Sn_p_n_to_S_npn n1 O);
166 nlemma symmetric_plusnat : symmetricT nat nat plus.
169 ##[ ##1: #n2; nrewrite > (npO_to_n n2); nnormalize; napply refl_eq
170 ##| ##2: #n2; #H; #n3;
171 nrewrite > (Sn_p_n_to_S_npn n2 n3);
172 nrewrite > (n_p_Sn_to_S_npn n3 n2);