# Changeset 487 for Deliverables/D3.1/C-semantics/binary

Ignore:
Timestamp:
Feb 9, 2011, 11:49:17 AM (9 years ago)
Message:

Port Clight semantics to the new-new matita syntax.

Location:
Deliverables/D3.1/C-semantics/binary
Files:
2 edited

Unmodified
Added
Removed
• ## Deliverables/D3.1/C-semantics/binary/Z.ma

 r400 comments may no longer be applicable. *) include "arithmetics/compare.ma". (*include "arithmetics/compare.ma".*) include "binary/positive.ma". ninductive Z : Type ≝ inductive Z : Type[0] ≝ OZ  : Z | pos : Pos → Z | neg : Pos → Z. interpretation "Integers" 'Z = Z. ndefinition Z_of_nat ≝ (*interpretation "Integers" 'D = Z.*) definition Z_of_nat ≝ λn. match n with [ O ⇒ OZ | S n ⇒ pos (succ_pos_of_nat n)]. ncoercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z. ndefinition neg_Z_of_nat \def coercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z. definition neg_Z_of_nat \def λn. match n with [ O ⇒ OZ | S n ⇒ neg (succ_pos_of_nat n)]. ndefinition abs ≝ definition abs ≝ λz.match z with [ OZ ⇒ O | neg n ⇒ nat_of_pos n]. ndefinition OZ_test ≝ definition OZ_test ≝ λz.match z with [ OZ ⇒ true | neg _ ⇒ false]. ntheorem OZ_test_to_Prop : ∀z:Z. theorem OZ_test_to_Prop : ∀z:Z. match OZ_test z with [true ⇒ z=OZ |false ⇒ z ≠ OZ]. #z;ncases z ##[napply refl ##|##*:#z1;napply nmk;#H;ndestruct] nqed. #z cases z [ @refl |*:#z1 @nmk #H destruct] qed. (* discrimination *) ntheorem injective_pos: injective Pos Z pos. #n;#m;#H;ndestruct;//; nqed. theorem injective_pos: injective Pos Z pos. #n #m #H destruct // qed. (* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m \def injective_pos. *) ntheorem injective_neg: injective Pos Z neg. #n;#m;#H;ndestruct;//; nqed. theorem injective_neg: injective Pos Z neg. #n #m #H destruct // qed. (* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m \def injective_neg. *) ntheorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n. #n;napply nmk;#H;ndestruct; nqed. ntheorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n. #n;napply nmk;#H;ndestruct; nqed. ntheorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m. #n;#m;napply nmk;#H;ndestruct; nqed. ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y). #x;#y;ncases x; ##[ncases y; ##[@;// ##|##*:#n;@2;napply nmk;#H;ndestruct] ##|#n;ncases y; ##[@2;napply nmk;#H;ndestruct; ##|#m;ncases (decidable_eq_pos n m);#H; ##[nrewrite > H;@;// ##|@2;napply nmk;#H2;nelim H; (* bug if you don't introduce H3 *)#H3;ndestruct; napply H3;@] ##|#m;@2;napply nmk;#H;ndestruct] ##|#n;ncases y; ##[@2;napply nmk;#H;ndestruct; ##|#m;@2;napply nmk;#H;ndestruct ##|#m;ncases (decidable_eq_pos n m);#H; ##[nrewrite > H;@;// ##|@2;napply nmk;#H2;nelim H;#H3;ndestruct; napply H3;@]##]##] nqed. ndefinition Zsucc ≝ theorem not_eq_OZ_pos: ∀n:Pos. OZ ≠ pos n. #n @nmk #H destruct; qed. theorem not_eq_OZ_neg :∀n:Pos. OZ ≠ neg n. #n @nmk #H destruct; qed. theorem not_eq_pos_neg : ∀n,m:Pos. pos n ≠ neg m. #n #m @nmk #H destruct; qed. theorem decidable_eq_Z : ∀x,y:Z. decidable (x=y). #x #y cases x; [cases y; [% // |*:#n %2 @nmk #H destruct] |#n cases y; [%2 @nmk #H destruct; |#m cases (decidable_eq_pos n m) #H [>H % // |%2 @(not_to_not … H) #E destruct @refl ] |#m %2 @nmk #H destruct] |#n cases y; [%2 @nmk #H destruct; |#m %2 @nmk #H destruct |#m cases (decidable_eq_pos n m);#H [>H % // |%2 @(not_to_not … H) #E destruct @refl ]]] qed. definition Zsucc ≝ λz. match z with [ OZ ⇒ pos one | _ ⇒ neg (pred n)]]. ndefinition Zpred ≝ definition Zpred ≝ λz. match z with [ OZ ⇒ neg one | neg n ⇒ neg (succ n)]. nlemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))). //; nqed. ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z. #z;ncases z; ##[ // ##| #n; nnormalize; ncases n; /2/; ##| #n; ncases n; //; #n'; nrewrite > (pred_succ_unfold_hack …); nrewrite < (succ_pred_n …); //; @; #H; ndestruct; nqed. nlemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))). //; nqed. ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z. #z;ncases z ##[ // ##| #n; ncases n;//; #n'; nrewrite > (succ_pred_unfold_hack …); nrewrite < (succ_pred_n …); //; @; #H; ndestruct; ##| #n; ncases n;/3/; ##] nqed. nlet rec Zle (x:Z) (y:Z) on x : Prop ≝ lemma pred_succ_unfold_hack: ∀p. Zpred (Zsucc (neg (p0 p))) = neg (succ (pred (p0 p))). //; qed. theorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z. #z cases z; [ // | #n normalize; cases n; /2/; | #n cases n; //; #n' >(pred_succ_unfold_hack …) <(succ_pred_n …) //; % #H destruct; qed. lemma succ_pred_unfold_hack: ∀p. Zsucc (Zpred (pos (p0 p))) = pos (succ (pred (p0 p))). //; qed. theorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z. #z cases z [ // | #n cases n;//; #n' >(succ_pred_unfold_hack …) <(succ_pred_n …) //; % #H destruct; | #n cases n;/3/; ] qed. let rec Zle (x:Z) (y:Z) on x : Prop ≝ match x with [ OZ ⇒ interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)). nlet rec Zlt (x:Z) (y:Z) on x : Prop ≝ let rec Zlt (x:Z) (y:Z) on x : Prop ≝ match x with [ OZ ⇒ interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)). ntheorem irreflexive_Zlt: irreflexive Z Zlt. #x;ncases x ##[napply nmk;// ##|##*:#n;napply (not_le_succ_n n) (* XXX: auto?? *)] nqed. theorem irreflexive_Zlt: irreflexive Z Zlt. #x cases x [@nmk // |*:#n @(not_le_succ_n n) (* XXX: auto?? *)] qed. (* transitivity *) ntheorem transitive_Zle : transitive Z Zle. #x;#y;#z;ncases x ##[ncases y ##[// ##|##*:#n;ncases z;//] ##|#n;ncases y ##[#H;ncases H ##|(*##*:#m;#Hl;ncases z;//;*) #m;#Hl;ncases z;//;#p;#Hr; napply (transitive_le n m p);//; (* XXX: auto??? *) ##|#m;#Hl;ncases Hl] ##|#n;ncases y ##[#Hl;ncases z ##[##1,2:// ##|#m;#Hr;ncases Hr] ##|#m;#Hl;ncases z; ##[##1,2:// ##|#p;#Hr;ncases Hr] ##|#m;#Hl;ncases z;//;#p;#Hr; napply (transitive_le p m n);//; (* XXX: auto??? *) ##] nqed. theorem transitive_Zle : transitive Z Zle. #x #y #z cases x [cases y [// |*:#n cases z;//] |#n cases y [#H cases H |(**:#m #Hl cases z;//;*) #m #Hl cases z;//;#p #Hr @(transitive_le n m p) //; (* XXX: auto??? *) |#m #Hl cases Hl] |#n cases y [#Hl cases z [1,2:// |#m #Hr cases Hr] |#m #Hl cases z; [1,2:// |#p #Hr cases Hr] |#m #Hl cases z;//;#p #Hr @(transitive_le p m n) //; (* XXX: auto??? *) ] qed. (* variant trans_Zle: transitive Z Zle \def transitive_Zle.*) ntheorem transitive_Zlt: transitive Z Zlt. #x;#y;#z;ncases x ##[ncases y ##[// ##|#n;ncases z ##[#_;#Hr;ncases Hr ##|// ##|#m;#_;#Hr;ncases Hr] ##|#n;#Hl;ncases Hl] ##|#n;ncases y ##[#Hl;ncases Hl ##|#m;ncases z ##[// ##|#p;napply transitive_lt (* XXX: auto??? *) ##|//##] ##|#m;#Hl;ncases Hl] ##|#n;ncases y ##[ncases z; ##[##1,2:// ##|#m;#_;#Hr;ncases Hr] ##|#m;ncases z; ##[##1,2:// ##|#p;#_;#Hr;ncases Hr] ##|#m;ncases z ##[##1,2:// ##|#p;#Hl;#Hr;napply (transitive_lt … Hr Hl)] ##] ##] nqed. theorem transitive_Zlt: transitive Z Zlt. #x #y #z cases x [cases y [// |#n cases z [#_ #Hr cases Hr |// |#m #_ #Hr cases Hr] |#n #Hl cases Hl] |#n cases y [#Hl cases Hl |#m cases z [// |#p apply transitive_lt (* XXX: auto??? *) |//] |#m #Hl cases Hl] |#n cases y [cases z; [1,2:// |#m #_ #Hr cases Hr] |#m cases z; [1,2:// |#p #_ #Hr cases Hr] |#m cases z [1,2:// |#p #Hl #Hr apply (transitive_lt … Hr Hl)] ] ] qed. (* variant trans_Zlt: transitive Z Zlt \def irreflexive_Zlt.*) ntheorem Zlt_neg_neg_to_lt: theorem Zlt_neg_neg_to_lt: ∀n,m:Pos. neg n < neg m → m < n. //; nqed. ntheorem lt_to_Zlt_neg_neg: ∀n,m:Pos.m < n → neg n < neg m. qed. theorem lt_to_Zlt_neg_neg: ∀n,m:Pos.m < n → neg n < neg m. //; nqed. ntheorem Zlt_pos_pos_to_lt: qed. theorem Zlt_pos_pos_to_lt: ∀n,m:Pos. pos n < pos m → n < m. //; nqed. ntheorem lt_to_Zlt_pos_pos: ∀n,m:Pos.n < m → pos n < pos m. qed. theorem lt_to_Zlt_pos_pos: ∀n,m:Pos.n < m → pos n < pos m. //; nqed. nlemma Zsucc_neg_succ: ∀n:Pos. Zsucc (neg (succ n)) = neg n. #n; nnormalize; nrewrite < (pred_succ_n n); ncases n; //; nqed. ntheorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y. #x;#y;ncases x ##[ncases y ##[#H;ncases H ##|//; ##|#p;#H;ncases H] ##|#n;ncases y ##[#H;ncases H ##|#p;nnormalize;// ##|#p;#H;ncases H] ##|#n;ncases y ##[##1,2:ncases n;// ##|#p;napply (pos_cases … n); ##[#H;nelim (not_le_succ_one p);#H2;napply H2;napply H (*//;*) (* XXX: auto? *) ##|#m;nrewrite > (Zsucc_neg_succ m);napply le_S_S_to_le; (* XXX: auto? *) ##] ##] ##] nqed. qed. lemma Zsucc_neg_succ: ∀n:Pos. Zsucc (neg (succ n)) = neg n. #n normalize; <(pred_succ_n n) cases n; //; qed. theorem Zlt_to_Zle: ∀x,y:Z. x < y → Zsucc x ≤ y. #x #y cases x [cases y [#H cases H |//; |#p #H cases H] |#n cases y [#H cases H |#p normalize;// |#p #H cases H] |#n cases y [1,2:cases n;// |#p @(pos_cases … n) [#H elim (not_le_succ_one p);#H2 @H2 @H (*// *) (* XXX: auto? *) |#m >(Zsucc_neg_succ m) @le_S_S_to_le (* XXX: auto? *) ] ] ] qed. (*** COMPARE ***) (* boolean equality *) nlet rec eqZb (x:Z) (y:Z) on x : bool ≝ let rec eqZb (x:Z) (y:Z) on x : bool ≝ match x with [ OZ ⇒ | neg q ⇒ eqb p q]]. ntheorem eqZb_to_Prop: theorem eqZb_to_Prop: ∀x,y:Z. match eqZb x y with [ true ⇒ x=y | false ⇒ x ≠ y]. #x;#y;ncases x ##[ncases y; ##[// ##|napply not_eq_OZ_pos (* XXX: auto? *) ##|napply not_eq_OZ_neg (* XXX: auto? *)] ##|#n;ncases y; ##[napply nmk;#H;nelim (not_eq_OZ_pos n);#H2;/2/; ##|#m;napply eqb_elim; ##[// ##|#H;napply nmk;#H2;nelim H;#H3;ndestruct;/2/] ##|#m;napply not_eq_pos_neg] ##|#n;ncases y ##[napply nmk;#H;nelim (not_eq_OZ_neg n);#H;/2/; ##|#m;napply nmk;#H;ndestruct ##|#m;napply eqb_elim; ##[// ##|#H;napply nmk;#H2;ndestruct;nelim H;/2/] ##] ##] nqed. ntheorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop. #x #y cases x [cases y; [// |@not_eq_OZ_pos (* XXX: auto? *) |@not_eq_OZ_neg (* XXX: auto? *)] |#n cases y; [@nmk #H elim (not_eq_OZ_pos n);#H2 /2/; |#m @eqb_elim [// | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) // ] |#m @not_eq_pos_neg] |#n cases y [@nmk #H elim (not_eq_OZ_neg n);#H /2/; |#m @nmk #H destruct |#m @eqb_elim [// | * #H % #H' @H @(match H' return λx.λ_.n=match x with [pos m ⇒ m | neg m ⇒ m | OZ ⇒ one ] with [refl ⇒ ?]) // ] ] qed. theorem eqZb_elim: ∀x,y:Z.∀P:bool → Prop. (x=y → P true) → (x ≠ y → P false) → P (eqZb x y). #x;#y;#P;#HP1;#HP2; ncut #x #y #P #HP1 #HP2 cut (match (eqZb x y) with [ true ⇒ x=y | false ⇒ x ≠ y] → P (eqZb x y)) ##[ncases (eqZb x y);nnormalize; (* XXX: auto?? *) ##[napply HP1 ##|napply HP2] ##|#Hcut;napply Hcut;napply eqZb_to_Prop] nqed. nlet rec Z_compare (x:Z) (y:Z) : compare ≝ [cases (eqZb x y);normalize; (* XXX: auto?? *) [@HP1 |@HP2] |#Hcut @Hcut @eqZb_to_Prop] qed. let rec Z_compare (x:Z) (y:Z) : compare ≝ match x with [ OZ ⇒ | neg m ⇒ pos_compare m n ]]. ntheorem Z_compare_to_Prop : theorem Z_compare_to_Prop : ∀x,y:Z. match (Z_compare x y) with [ LT ⇒ x < y | EQ ⇒ x=y | GT ⇒ y < x]. #x;#y;nelim x ##[nelim y;//; ##|nelim y ##[##1,3:// ##|#n;#m;nnormalize; ncut (match (pos_compare m n) with #x #y elim x [elim y;//; |elim y [1,3:// |#n #m normalize; cut (match (pos_compare m n) with [ LT ⇒ m < n | EQ ⇒ m = n | EQ ⇒ pos m = pos n | GT ⇒ (succ n)  ≤ m]) ##[ncases (pos_compare m n);// ##|#Hcut;napply Hcut;napply pos_compare_to_Prop] ##] ##|nelim y ##[#n;// ##|nnormalize;// ##|nnormalize;#n;#m; ncut (match (pos_compare n m) with [cases (pos_compare m n);// |#Hcut @Hcut @pos_compare_to_Prop] ] |elim y [#n // |normalize;// |normalize;#n #m cut (match (pos_compare n m) with [ LT ⇒ n < m | EQ ⇒ n = m | EQ ⇒ neg m = neg n | GT ⇒ (succ m) ≤ n]) ##[ncases (pos_compare n m);// ##|#Hcut;napply Hcut;napply pos_compare_to_Prop] ##] ##] nqed. nlet rec Zplus (x:Z) (y:Z) on x : Z ≝ [cases (pos_compare n m);// |#Hcut @Hcut @pos_compare_to_Prop] ] ] qed. let rec Zplus (x:Z) (y:Z) on x : Z ≝ match x with [ OZ ⇒ y interpretation "integer plus" 'plus x y = (Zplus x y). ntheorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m. #n;#m;ncases n ##[// ##|#p;ncases m ##[nnormalize;// ##|#m';nnormalize;nrewrite > (nat_plus_pos_plus …);nrewrite > (succ_nat_pos ?);/2/] nqed. ntheorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m. //; nqed. ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z. #z;ncases z;//; nqed. ntheorem sym_Zplus : ∀x,y:Z. x+y = y+x. #x;#y;ncases x; ##[nrewrite > (Zplus_z_OZ ?) (*XXX*);// ##|#p;ncases y ##[// ##|nnormalize;// ##|#q;nnormalize;nrewrite > (pos_compare_n_m_m_n ??) (*XXX*); ncases (pos_compare q p);//] ##|#p;ncases y ##[//; ##|#q;nnormalize;nrewrite > (pos_compare_n_m_m_n ??) (*XXX*); ncases (pos_compare q p);// ##|nnormalize;//] ##] nqed. ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z. #z;ncases z ##[// ##|##*:#n;ncases n;//] nqed. ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z. #z;ncases z ##[// ##|##*:#n;ncases n;//] nqed. nlemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n. #n; nnormalize; ncases n; /2/; nqed. ntheorem Zplus_pos_pos: theorem eq_plus_Zplus: ∀n,m:nat. Z_of_nat (n+m) = Z_of_nat n + Z_of_nat m. #n #m cases n [// |#p cases m [normalize;// |#m' normalize;>(nat_plus_pos_plus …) >(succ_nat_pos ?) /2/] qed. theorem eq_pplus_Zplus: ∀n,m:Pos. pos (n+m) = pos n + pos m. //; qed. theorem Zplus_z_OZ: ∀z:Z. z+OZ = z. #z cases z;//; qed. theorem sym_Zplus : ∀x,y:Z. x+y = y+x. #x #y cases x; [>(Zplus_z_OZ ?) (*XXX*) // |#p cases y [// |normalize;// |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*) cases (pos_compare q p);//] |#p cases y [//; |#q normalize;>(pos_compare_n_m_m_n ??) (*XXX*) cases (pos_compare q p);// |normalize;//] ] qed. theorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg one)+z. #z cases z [// |*:#n cases n;//] qed. theorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos one)+z. #z cases z [// |*:#n cases n;//] qed. lemma Zpred_pos_succ: ∀n. Zpred (pos (succ n)) = pos n. #n normalize; cases n; /2/; qed. theorem Zplus_pos_pos: ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)). #n;#m;napply (pos_cases … n); ##[ napply (pos_cases … m); //; ##|#p;napply (pos_cases … m); ##[nnormalize; nrewrite < (succ_plus_one …); //; ##|#q; nrewrite > (Zsucc_Zplus_pos_O …); nrewrite > (Zpred_pos_succ ?); nnormalize; /2/; ##] ##] nqed. ntheorem Zplus_pos_neg: #n #m @(pos_cases … n) [ @(pos_cases … m) //; |#p @(pos_cases … m) [normalize; <(succ_plus_one …) //; |#q >(Zsucc_Zplus_pos_O …) >(Zpred_pos_succ ?) normalize; /2/; ] ] qed. theorem Zplus_pos_neg: ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)). #n m; nnormalize; nrewrite < (pos_compare_S_S …); nrewrite > (partialminus_S_S …); nrewrite > (partialminus_S_S …); //; nqed. nlemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q | p0 p ⇒ P n | p1 p ⇒ P n ] = P n. #A P Q n; napply succ_elim; //; nqed. nlemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n. #n; ncases n; //; #n'; nwhd in ⊢ (??%?); nnormalize; nrewrite < (pred_succ_n …); napply succ_elim; //; nqed. ntheorem Zplus_neg_pos : #n #m normalize; <(pos_compare_S_S …) >(partialminus_S_S …) >(partialminus_S_S …) //; qed. lemma pos_nonzero: ∀A.∀P:Pos→A.∀Q,n. match succ n with [ one ⇒ Q | p0 p ⇒ P n | p1 p ⇒ P n ] = P n. #A #P #Q #n @succ_elim //; qed. lemma partial_minus_S_one: ∀n. partial_minus (succ n) one = MinusPos n. #n cases n; //; #n' whd in ⊢ (??%?); normalize; <(pred_succ_n …) @succ_elim //; qed. theorem Zplus_neg_pos : ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)). #n m; napply (pos_cases … n); napply (pos_cases … m); ##[ //; ##| #m'; nrewrite > (Zpred_pos_succ …); nrewrite > (?:pos (succ m') = Zsucc (pos m')); //; ##| #m'; nnormalize; nrewrite > (pos_compare_S_one …); nnormalize; nrewrite > (partial_minus_S_one …); nnormalize; nrewrite > (pos_nonzero …); nrewrite < (pred_succ_n …); //; ##| #m'; #n'; nnormalize; nrewrite < (pos_compare_S_S …); nrewrite > (partialminus_S_S …); nrewrite > (partialminus_S_S …); nrewrite > (pos_nonzero …); nrewrite > (pos_nonzero …); nrewrite < (pred_succ_n …); nrewrite < (pred_succ_n …); nnormalize; //; ##] nqed. ntheorem Zplus_neg_neg: #n #m @(pos_cases … n) @(pos_cases … m) [ //; | #m' >(Zpred_pos_succ …) >(?:pos (succ m') = Zsucc (pos m')) //; | #m' normalize; >(pos_compare_S_one …) normalize; >(partial_minus_S_one …) normalize; >(pos_nonzero …) <(pred_succ_n …) //; | #m' #n' normalize; <(pos_compare_S_S …) >(partialminus_S_S …) >(partialminus_S_S …) >(pos_nonzero …) >(pos_nonzero …) <(pred_succ_n …) <(pred_succ_n …) normalize; //; ] qed. theorem Zplus_neg_neg: ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)). #n m; napply (pos_cases … n); napply (pos_cases … m); ##[ ##1,2: //; ##| #n'; nnormalize in ⊢ (???(?%?)); nrewrite > (pos_nonzero …); nrewrite < (pred_succ_n …); nnormalize; //; ##| #m';#n'; nnormalize; nrewrite > (pos_nonzero …); nrewrite < (pred_succ_n …); nnormalize; //; ##] nqed. ntheorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y). #x;#y;ncases x ##[ncases y ##[// ##|#n;nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zpred ?);// ##|#p;nrewrite < (Zsucc_Zplus_pos_O …); //] ##|ncases y;/2/; #p; nrewrite > (sym_Zplus ? (Zpred OZ)); nrewrite < Zpred_Zplus_neg_O; //; ##|ncases y ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?); nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);// ##|##*:/2/] nqed. ntheorem Zplus_Zsucc_pos_pos : #n #m @(pos_cases … n) @(pos_cases … m) [ 1,2: //; | #n' normalize in ⊢ (???(?%?)); >(pos_nonzero …) <(pred_succ_n …) normalize; //; | #m' #n' normalize; >(pos_nonzero …) <(pred_succ_n …) normalize; //; ] qed. theorem Zplus_Zsucc_Zpred: ∀x,y. x+y = (Zsucc x)+(Zpred y). #x #y cases x [cases y [// |#n <(Zsucc_Zplus_pos_O ?) >(Zsucc_Zpred ?) // |#p <(Zsucc_Zplus_pos_O …) //] |cases y;/2/; #p >(sym_Zplus ? (Zpred OZ)) (Zpred_Zsucc ?) // |*:/2/] qed. theorem Zplus_Zsucc_pos_pos : ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)). #n m;nrewrite > (Zsucc_Zplus_pos_O ?);nrewrite > (Zsucc_Zplus_pos_O ?);//; nqed. ntheorem Zplus_Zsucc_pos_neg: #n #m >(Zsucc_Zplus_pos_O ?) >(Zsucc_Zplus_pos_O ?) //; qed. theorem Zplus_Zsucc_pos_neg: ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))). #n;#m; napply (pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))) ##[#n1;nelim n1 ##[// ##|##*:#n2;#IH;nelim n2;//] ##|#n'; nrewrite > (sym_Zplus …); nrewrite < (Zpred_Zplus_neg_O ?); nrewrite > (sym_Zplus …); nrewrite < (Zpred_Zplus_neg_O ?); nrewrite > (Zpred_Zsucc …);  /2/ ##|#n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nrewrite > IH; nrewrite < (Zplus_pos_neg …); //] nqed. ntheorem Zplus_Zsucc_neg_neg : #n #m @(pos_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))) [#n1 elim n1 [// |*:#n2 #IH elim n2;//] |#n' >(sym_Zplus …) <(Zpred_Zplus_neg_O ?) >(sym_Zplus …) <(Zpred_Zplus_neg_O ?) >(Zpred_Zsucc …)  /2/ |#n1 #m1 #IH <(Zplus_pos_neg ? m1) >IH <(Zplus_pos_neg …) //] qed. theorem Zplus_Zsucc_neg_neg : ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m). #n;#m; napply (pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))) ##[napply pos_elim; ##[// ##|#n2;#IH;nnormalize;nrewrite < (pred_succ_n …); nrewrite > (pos_nonzero …); //] ##| #n'; nnormalize; nrewrite > (pos_nonzero …); nrewrite < (pred_succ_n …); nnormalize; nrewrite < (succ_plus_one …); nrewrite < (succ_plus_one …); nrewrite > (pos_nonzero …); //; ##| #n' m' IH; nnormalize; nrewrite > (pos_nonzero …); nnormalize; nrewrite < (pluss_succn_m …); nrewrite > (pos_nonzero …); //; ##] nqed. nlemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m. #n m; nnormalize; nrewrite < (pos_compare_S_S …); nrewrite > (partialminus_S_S …); nrewrite > (partialminus_S_S …); //; nqed. ntheorem Zplus_Zsucc_neg_pos: #n #m @(pos_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))) [@pos_elim [// |#n2 #IH normalize;<(pred_succ_n …) >(pos_nonzero …) //] | #n' normalize; >(pos_nonzero …) <(pred_succ_n …) normalize; <(succ_plus_one …) <(succ_plus_one …) >(pos_nonzero …) //; | #n' #m' #IH normalize; >(pos_nonzero …) normalize; <(pluss_succn_m …) >(pos_nonzero …) //; ] qed. lemma neg_pos_succ: ∀n,m:Pos. neg (succ n) + pos (succ m) = neg n + pos m. #n #m normalize; <(pos_compare_S_S …) >(partialminus_S_S …) >(partialminus_S_S …) //; qed. theorem Zplus_Zsucc_neg_pos: ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)). #n;#m; napply (pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m))) ##[napply pos_elim; ##[// ##|#n2;#IH;nnormalize; nrewrite > (pos_nonzero …); nnormalize; nrewrite > (partial_minus_S_one …); //] ##| #n'; nrewrite > (sym_Zplus …); nrewrite < (Zsucc_Zplus_pos_O …); nrewrite > (sym_Zplus …); nrewrite < (Zsucc_Zplus_pos_O …); //; ##|#n' m' IH; nrewrite > (neg_pos_succ …); //; ##] nqed. ntheorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y). #x;#y;ncases x ##[ncases y;//;(*#n;nnormalize;ncases n;//;*) ##|##*:#n;ncases y;//;#m;napply Zplus_Zsucc_neg_pos(* XXX: // didn't work! *)] nqed. ntheorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y). #x;#y;ncut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)) ##[nrewrite > (Zsucc_Zpred ?);// ##|#Hcut;nrewrite > Hcut;nrewrite > (Zplus_Zsucc ??);//] nqed. nlemma eq_rect_Type0_r: #n #m @(pos_elim2 (λn,m. (Zsucc (neg n)) + (pos m) = Zsucc (neg n + pos m))) [@pos_elim [// |#n2 #IH normalize; >(pos_nonzero …) normalize; >(partial_minus_S_one …) //] | #n' >(sym_Zplus …) <(Zsucc_Zplus_pos_O …) >(sym_Zplus …) <(Zsucc_Zplus_pos_O …) //; |#n' #m' #IH >(neg_pos_succ …) //; ] qed. theorem Zplus_Zsucc : ∀x,y:Z. (Zsucc x)+y = Zsucc (x+y). #x #y cases x [cases y;//;(*#n normalize;cases n;//;*) |*:#n cases y;//;#m @Zplus_Zsucc_neg_pos(* XXX: // didn't work! *)] qed. theorem Zplus_Zpred: ∀x,y:Z. (Zpred x)+y = Zpred (x+y). #x #y cut (Zpred (x+y) = Zpred ((Zsucc (Zpred x))+y)) [>(Zsucc_Zpred ?) // |#Hcut >Hcut >(Zplus_Zsucc ??) //] qed. lemma eq_rect_Type0_r: ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ??? p0); nassumption. nqed. ntheorem associative_Zplus: associative Z Zplus. #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption. qed. theorem associative_Zplus: associative Z Zplus. (* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*) #x;#y;#z;ncases x ##[// ##|napply pos_elim; ##[nrewrite < (Zsucc_Zplus_pos_O ?);nrewrite < (Zsucc_Zplus_pos_O ?);//; ##|#n1;#IH; nrewrite > (Zplus_Zsucc (pos n1) ?);nrewrite > (Zplus_Zsucc (pos n1) ?); nrewrite > (Zplus_Zsucc ((pos n1)+y) ?);//] ##|napply pos_elim; ##[nrewrite < (Zpred_Zplus_neg_O (y+z));nrewrite < (Zpred_Zplus_neg_O y);//; ##|#n1;#IH; nrewrite > (Zplus_Zpred (neg n1) ?);nrewrite > (Zplus_Zpred (neg n1) ?); nrewrite > (Zplus_Zpred ((neg n1)+y) ?);//] ##] nqed. #x #y #z cases x [// |@pos_elim [<(Zsucc_Zplus_pos_O ?) <(Zsucc_Zplus_pos_O ?) //; |#n1 #IH >(Zplus_Zsucc (pos n1) ?) >(Zplus_Zsucc (pos n1) ?) >(Zplus_Zsucc ((pos n1)+y) ?) //] |@pos_elim [<(Zpred_Zplus_neg_O (y+z)) <(Zpred_Zplus_neg_O y) //; |#n1 #IH >(Zplus_Zpred (neg n1) ?) >(Zplus_Zpred (neg n1) ?) >(Zplus_Zpred ((neg n1)+y) ?) //] ] qed. (* variant assoc_Zplus : \forall x,y,z:Z.  (x+y)+z = x+(y+z) (* Zopp *) ndefinition Zopp : Z → Z ≝ definition Zopp : Z → Z ≝ λx:Z. match x with [ OZ ⇒ OZ interpretation "integer unary minus" 'uminus x = (Zopp x). ntheorem eq_OZ_Zopp_OZ : OZ = (- OZ). theorem eq_OZ_Zopp_OZ : OZ = (- OZ). //; nqed. ntheorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y. #x;#y;ncases x ##[ncases y;// ##|##*:#n;ncases y;//;#m;nnormalize;napply pos_compare_elim;nnormalize;//] nqed. ntheorem Zopp_Zopp: ∀x:Z. --x = x. #x;ncases x;//; nqed. ntheorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ. #x;ncases x ##[// ##|##*:#n;nnormalize;nrewrite > (pos_compare_n_n ?);//] nqed. ntheorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x). #x;#z;#y;#H; nrewrite < (Zplus_z_OZ z);nrewrite < (Zplus_z_OZ y); nrewrite < (Zplus_Zopp x); nrewrite < (associative_Zplus ???);nrewrite < (associative_Zplus ???); qed. theorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y. #x #y cases x [cases y;// |*:#n cases y;//;#m normalize;@pos_compare_elim normalize;//] qed. theorem Zopp_Zopp: ∀x:Z. --x = x. #x cases x;//; qed. theorem Zplus_Zopp: ∀ x:Z. x+ -x = OZ. #x cases x [// |*:#n normalize;>(pos_compare_n_n ?) //] qed. theorem injective_Zplus_l: ∀x:Z.injective Z Z (λy.y+x). #x #z #y #H <(Zplus_z_OZ z) <(Zplus_z_OZ y) <(Zplus_Zopp x) <(associative_Zplus ???) <(associative_Zplus ???) //; nqed. ntheorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y). #x;#z;#y;#H; napply (injective_Zplus_l x); nrewrite < (sym_Zplus ??); qed. theorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y). #x #z #y #H @(injective_Zplus_l x) <(sym_Zplus ??) //; nqed. qed. (* minus *) ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y). definition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y). interpretation "integer minus" 'minus x y = (Zminus x y). ndefinition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n). ndefinition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n). ndefinition two_p : Z → Z ≝ definition Z_two_power_nat : nat → Z ≝ λn. pos (two_power_nat n). definition Z_two_power_pos : Pos → Z ≝ λn. pos (two_power_pos n). definition two_p : Z → Z ≝ λz.match z with [ OZ ⇒ pos one
• ## Deliverables/D3.1/C-semantics/binary/positive.ma

 r10 (* little endian positive binary numbers. *) include "basics/functions.ma". include "basics/eq.ma". include "basics/logic.ma". include "arithmetics/nat.ma". include "arithmetics/compare.ma". ninductive Pos : Type ≝ include "oldlib/eq.ma". (* arithmetics/comparison.ma --> *) inductive compare : Type[0] ≝ | LT : compare | EQ : compare | GT : compare. definition compare_invert: compare → compare ≝ λc.match c with [ LT ⇒ GT | EQ ⇒ EQ | GT ⇒ LT ]. (* <-- *) inductive Pos : Type[0] ≝ | one : Pos |  p1 : Pos → Pos |  p0 : Pos → Pos. nlet rec pred (n:Pos) ≝ let rec pred (n:Pos) ≝ match n with [ one ⇒ one ]. nremark test : pred (p0 (p0 (p0 one))) = p1 (p1 one). //; nqed. nlet rec succ (n:Pos) ≝ example test : pred (p0 (p0 (p0 one))) = p1 (p1 one). //; qed. let rec succ (n:Pos) ≝ match n with [ one ⇒ p0 one ]. nlemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n). #P H0 H1 n; ncases n; nnormalize; //; nqed. ntheorem pred_succ_n : ∀n. n = pred (succ n). #n; nelim n; ##[ ##1,3: // ##| #p'; nnormalize; napply succ_elim; /2/; ##] nqed. lemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n). #P #H0 #H1 #n cases n; normalize; //; qed. theorem pred_succ_n : ∀n. n = pred (succ n). #n elim n; [ 1,3: // | #p' normalize; @succ_elim /2/; ] qed. (* ntheorem succ_pred_n : ∀n. n≠one → n = succ (pred n). #n; nelim n; ##[ #H; napply False_ind; nelim H; /2/; ##| //; ##| #n'; ncases n'; /2/; #n''; #IH; #_; nrewrite < IH; nnormalize; theorem succ_pred_n : ∀n. n≠one → n = succ (pred n). #n elim n; [ #H @False_ind elim H; /2/; | //; | #n' cases n'; /2/; #n'' #IH #_ (IH m' ?); //; ##] ##] nqed. nremark test2 : nat_of_pos (p0 (p1 one)) = 6. //; nqed. theorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n). //; qed. theorem succ_pos_of_nat_inj: injective ?? succ_pos_of_nat. #n elim n; [ #m cases m; [ // | #m' normalize; @succ_elim #p #H destruct ] | #n' #IH #m cases m; [ normalize; @succ_elim #p #H destruct; | normalize; #m' #H >(IH m' ?) //; ] ] qed. example test2 : nat_of_pos (p0 (p1 one)) = 6. //; qed. (* Usual induction principle; proof roughly following Coq's, apparently due to Conor McBride. *) ninductive possucc : Pos → Prop ≝ inductive possucc : Pos → Prop ≝ | psone  : possucc one | pssucc : ∀n. possucc n → possucc (succ n). nlet rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝ let rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝ match p return λn',p'.possucc (p0 n') with [ psone ⇒ pssucc ? psone ]. nlet rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝ let rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝ match p return λn',p'. possucc (p1 n') with [ psone ⇒ pssucc ? (pssucc ? psone) ]. nlet rec possuccinj (n:Pos) : possucc n ≝ let rec possuccinj (n:Pos) : possucc n ≝ match n with [ one ⇒ psone ]. nlet rec possucc_elim let rec possucc_elim (P : Pos → Prop) (Pone : P one) ]. ndefinition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n. #P Pone Psucc n; napply (possucc_elim … (possuccinj n)); /2/; nqed. nlet rec possucc_cases definition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n. #P #Pone #Psucc #n @(possucc_elim … (possuccinj n)) /2/; qed. let rec possucc_cases (P : Pos → Prop) (Pone : P one) ]. ndefinition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n. #P Pone Psucc n; napply (possucc_cases … (possuccinj n)); /2/; nqed. ntheorem succ_pred_n : ∀n. n≠one → n = succ (pred n). napply pos_elim; ##[ #H; napply False_ind; nelim H; /2/; ##| //; ##] nqed. ntheorem not_eq_one_succ : ∀n:Pos. one ≠ succ n. #n; nelim n; nnormalize; ##[ @; #H; ndestruct; ##| ##2,3: #n' H; @; #H'; ndestruct; ##] nqed. ntheorem not_eq_n_succn: ∀n:Pos. n ≠ succ n. #n; nelim n; ##[ //; ##| ##*: #n' IH; nnormalize; @; #H; ndestruct ##] nqed. ntheorem pos_elim2: definition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n. #P #Pone #Psucc #n @(possucc_cases … (possuccinj n)) /2/; qed. theorem succ_pred_n : ∀n. n≠one → n = succ (pred n). @pos_elim [ #H @False_ind elim H; /2/; | //; ] qed. theorem not_eq_one_succ : ∀n:Pos. one ≠ succ n. #n elim n; normalize; [ % #H destruct; | 2,3: #n' #H % #H' destruct; ] qed. theorem not_eq_n_succn: ∀n:Pos. n ≠ succ n. #n elim n; [ //; | *: #n' #IH normalize; % #H destruct ] qed. theorem pos_elim2: ∀R:Pos → Pos → Prop. (∀n:Pos. R one n) → (∀n,m:Pos. R n m → R (succ n) (succ m)) → ∀n,m:Pos. R n m. #R ROn RSO RSS; napply pos_elim; //; #n0 Rn0m; napply pos_elim; /2/; nqed. ntheorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m). napply pos_elim2; #n; ##[ napply (pos_elim ??? n); /2/; ##| /3/; ##| #m Hind; ncases Hind; /3/; ##] nqed. nlet rec plus n m ≝ #R #ROn #RSO #RSS @pos_elim //; #n0 #Rn0m @pos_elim /2/; qed. theorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m). @pos_elim2 #n [ @(pos_elim ??? n) /2/; | /3/; | #m #Hind cases Hind; /3/; ] qed. let rec plus n m ≝ match n with [ one ⇒ succ m interpretation "positive plus" 'plus x y = (plus x y). ntheorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m). #n; nelim n; nnormalize; ##[ // ##| ##2,3: #n' IH m; ncases m; /3/; nnormalize; ncases n'; //; ##] nqed. ntheorem symmetric_plus : symmetric ? plus. #n; nelim n; ##[ #y; ncases y; nnormalize; //; ##| ##2,3: #n' IH y; ncases y; nnormalize; //; ##] nqed. ntheorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m. #n m; nrewrite > (symmetric_plus (succ n) m); nrewrite < (plus_n_succm …); //; nqed. ntheorem associative_plus : associative Pos plus. napply pos_elim; ##[ nnormalize; //; ##| #x' IHx; napply pos_elim; ##[ #z; nrewrite < (pluss_succn_m …); nrewrite < (pluss_succn_m …); nrewrite < (pluss_succn_m …); //; ##| #y' IHy' z; nrewrite < (pluss_succn_m y' …); nrewrite < (plus_n_succm …); nrewrite < (plus_n_succm …); nrewrite < (pluss_succn_m ? z); nrewrite > (IHy' …); //; ##] ##] nqed. ntheorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m). napply pos_elim; nnormalize; /3/; nqed. ntheorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n). /2/; nqed. ntheorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m). #n; nelim n; ##[ nnormalize; //; ##| #n' IH m; nnormalize; nrewrite > (IH m); nrewrite < (pluss_succn_m …); nrewrite < (pred_succ_n ?); nrewrite < (succ_pred_n …); //; nelim n'; nnormalize; /2/; ##] nqed. nlet rec times n m ≝ theorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m). #n elim n; normalize; [ // | 2,3: #n' #IH #m cases m; /3/; normalize; cases n'; //; ] qed. theorem commutative_plus : commutative ? plus. #n elim n; [ #y cases y; normalize; //; | 2,3: #n' #IH #y cases y; normalize; //; ] qed. theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m. #n #m >(commutative_plus (succ n) m) <(plus_n_succm …) //; qed. theorem associative_plus : associative Pos plus. @pos_elim [ normalize; //; | #x' #IHx @pos_elim [ #z <(pluss_succn_m …) <(pluss_succn_m …) <(pluss_succn_m …) //; | #y' #IHy' #z <(pluss_succn_m y' …) <(plus_n_succm …) <(plus_n_succm …) <(pluss_succn_m ? z) >(IHy' …) //; ] ] qed. theorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m). @pos_elim normalize; /3/; qed. theorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n). /2/; qed. theorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m). #n elim n; [ normalize; //; | #n' #IH #m normalize; >(IH m) <(pluss_succn_m …) <(pred_succ_n ?) <(succ_pred_n …) //; elim n'; normalize; /2/; ] qed. let rec times n m ≝ match n with [ one ⇒ m interpretation "positive times" 'times x y = (times x y). nlemma p0_times2: ∀n. p0 n = (succ one) * n. //; nqed. nlemma plus_times2: ∀n. n + n = (succ one) * n. #n; nelim n; ##[ //; ##| ##2,3: #n' IH; nnormalize; nrewrite > IH; //; ##] nqed. ntheorem times_succn_m: ∀n,m. m+n*m = (succ n)*m. #n; nelim n; ##[ /2/ ##| #n' IH; nnormalize; #m; nrewrite < (IH m); //; ##| /2/ ##] nqed. ntheorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m). napply pos_elim; ##[ // ##| #n IH m; nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); /3/; ##] nqed. ntheorem times_n_one: ∀n:Pos. n * one = n. #n; nelim n; /3/; nqed. ntheorem symmetric_times: symmetric Pos times. napply pos_elim; /2/; nqed. ntheorem distributive_times_plus : distributive Pos times plus. napply pos_elim; /2/; nqed. ntheorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a. //; nqed. ntheorem associative_times: associative Pos times. napply pos_elim; ##[ //; ##| #x IH y z; nrewrite < (times_succn_m …); nrewrite < (times_succn_m …); //; ##] nqed. nlemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z). //; nqed. lemma p0_times2: ∀n. p0 n = (succ one) * n. //; qed. lemma plus_times2: ∀n. n + n = (succ one) * n. #n elim n; [ //; | 2,3: #n' #IH normalize; >IH //; ] qed. theorem times_succn_m: ∀n,m. m+n*m = (succ n)*m. #n elim n; [ /2/ | #n' #IH normalize; #m <(IH m) //; | /2/ ] qed. theorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m). @pos_elim [ // | #n #IH #m <(times_succn_m …) <(times_succn_m …) /3/; ] qed. theorem times_n_one: ∀n:Pos. n * one = n. #n elim n; /3/; qed. theorem commutative_times: commutative Pos times. @pos_elim /2/; qed. theorem distributive_times_plus : distributive Pos times plus. @pos_elim /2/; qed. theorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a. //; qed. theorem associative_times: associative Pos times. @pos_elim [ //; | #x #IH #y #z <(times_succn_m …) <(times_succn_m …) //; ] qed. lemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z). //; qed. (*** ordering relations ***) but it means the proofs are much the same. *) ninductive le (n:Pos) : Pos → Prop ≝ inductive le (n:Pos) : Pos → Prop ≝ | le_n : le n n | le_S : ∀m:Pos. le n m → le n (succ m). interpretation "positive 'neither less than or equal to'" 'nleq x y = (Not (le x y)). ndefinition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m. definition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m. interpretation "positive 'less than'" 'lt x y = (lt x y). interpretation "positive 'not less than'" 'nless x y = (Not (lt x y)). ndefinition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n. definition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n. interpretation "positive 'greater than or equal to'" 'geq x y = (ge x y). interpretation "positive 'neither greater than or equal to'" 'ngeq x y = (Not (ge x y)). ndefinition gt: Pos → Pos → Prop ≝ λn,m. m (times_n_one …); nrewrite < (times_n_succm …); #H; napply False_ind; nelim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/; ##|#n; #m; #H; #le; napply le_succ_succ; napply H; /2/; ##] nqed. ntheorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m. #n; #m; #lenm;  (* interessante *) napplyS (le_plus n m); //; nqed. #a @pos_elim2 normalize; [//; |#n >(times_n_one …) <(times_n_succm …) #H @False_ind elim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/; |#n #m #H #le @le_succ_succ @H /2/; ] qed. theorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m. #n #m #lenm  (* interessante *) applyS (le_plus n m); //; qed. (* prove injectivity of times from above *) ntheorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m). #n m p H; napply le_to_le_to_eq; theorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m). #n #m #p #H @le_to_le_to_eq /2/; nqed. ntheorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n). /2/; nqed. qed. theorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n). /2/; qed. (* times & lt *) ntheorem monotonic_lt_times_l: theorem monotonic_lt_times_l: ∀c:Pos. monotonic Pos lt (λt.(t*c)). #c n m ltnm; nelim ltnm; nnormalize; ##[/2/; ##|#a; #_; #lt1; napply (transitive_le ??? lt1);//; ##] nqed. ntheorem monotonic_lt_times_r: #c #n #m #ltnm elim ltnm; normalize; [/2/; |#a #_ #lt1 @(transitive_le ??? lt1) //; ] qed. theorem monotonic_lt_times_r: ∀c:Pos. monotonic Pos lt (λt.(c*t)). #a b c H; nrewrite > (symmetric_times a b); nrewrite > (symmetric_times a c); /2/; nqed. ntheorem lt_to_le_to_lt_times: #a #b #c #H >(commutative_times a b) >(commutative_times a c) /2/; qed. theorem lt_to_le_to_lt_times: ∀n,m,p,q:Pos. n < m → p ≤ q → n*p < m*q. #n; #m; #p; #q; #ltnm; #lepq; napply (le_to_lt_to_lt ? (n*q)); ##[napply monotonic_le_times_r;//; ##|napply monotonic_lt_times_l;//; ##] nqed. ntheorem lt_times:∀n,m,p,q:Pos. n H; //; ##| ##3,6: #p; ncases p; ##[ ##1,4: nnormalize; #H; nrewrite > H; //; ##| ##2,3,5,6: #p'; nnormalize; #H; nrewrite > H; //; ##] ##] ##] ##| #n' IH m; ncases m; ##[ nnormalize; nrewrite < (pred_succ_n n'); ncases n'; //; ##| ##2,3: #m'; nnormalize; nlapply (IH m'); ncases (partial_minus (succ n') m'); ##[ ##1,2,4,5: nnormalize; #H; nrewrite > H; //; ##| ##3,6: #p; ncases p; ##[ ##1,4: nnormalize; #H; nrewrite > H; //; ##| ##2,3,5,6: #p'; nnormalize; #H; nrewrite > H; //; ##] ##] ##] ##] nqed. nlemma partialminus_n_S: ∀n,m:Pos. | #n' #IH #m cases m; [ normalize; <(pred_succ_n n') cases n'; //; | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m'); [ 1,2,4,5: normalize; #H >H //; | 3,6: #p cases p; [ 1,4: normalize; #H >H //; | 2,3,5,6: #p' normalize; #H >H //; ] ] ] | #n' #IH #m cases m; [ normalize; <(pred_succ_n n') cases n'; //; | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m'); [ 1,2,4,5: normalize; #H >H //; | 3,6: #p cases p; [ 1,4: normalize; #H >H //; | 2,3,5,6: #p' normalize; #H >H //; ] ] ] ] qed. lemma partialminus_n_S: ∀n,m:Pos. match partial_minus n m with [ MinusPos p ⇒ match p with [ one ⇒ partial_minus n (succ m) = MinusZero | _ ⇒ partial_minus n (succ m) = MinusNeg ]. #n; nelim n; ##[ #m; ncases m; //; #n elim n; [ #m cases m; //; (* Again, lots of unnecessary duplication! *) ##| #n' IH m; ncases m; ##[ nnormalize; ncases n'; //; ##| #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m'); ##[ ##1,2: nnormalize; #H; nrewrite > H; //; ##| #p; ncases p; nnormalize; ##[ #H; nrewrite > H; //; ##| ##2,3: #p'; #H; nrewrite > H; //; ##] ##] ##|  #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m'); ##[ ##1,2: nnormalize; #H; nrewrite > H; //; ##| #p; ncases p; nnormalize; ##[ #H; nrewrite > H; //; ##| ##2,3: #p'; #H; nrewrite > H; //; ##] ##] ##] ##| #n' IH m; ncases m; ##[ nnormalize; ncases n'; //; ##| #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m'); ##[ ##1,2: nnormalize; #H; nrewrite > H; //; ##| #p; ncases p; nnormalize; ##[ #H; nrewrite > H; //; ##| ##2,3: #p'; #H; nrewrite > H; //; ##] ##] ##|  #m'; nnormalize; nlapply (IH m'); ncases (partial_minus n' m'); ##[ ##1,2: nnormalize; #H; nrewrite > H; //; ##| #p; ncases p; nnormalize; ##[ #H; nrewrite > H; //; ##| ##2,3: #p'; #H; nrewrite > H; //; ##] ##] ##] ##] nqed. ntheorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m. #n; nelim n; ##[ #m; ncases m; ##[ //; ##| ##2,3: #m'; ncases m'; //; ##] ##| #n' IH m; ncases m; ##[ nnormalize; ncases n'; /2/; nnormalize; #n''; nrewrite < (pred_succ_n n''); ncases n'';//; ##| #m'; nnormalize; nrewrite > (IH ?); //; ##| #m'; nnormalize; nlapply (partialminus_S n' m'); ncases (partial_minus (succ n') m'); ##[ ##1,2: nnormalize; #H; nrewrite > H; //; ##| #p; ncases p; ##[ nnormalize; #H; nrewrite > H; //; ##| ##2,3: #p';nnormalize; #H; nrewrite > H; //; ##] ##] ##] ##|  #n' IH m; ncases m; ##[ nnormalize; ncases n'; /2/; ##| #m'; nnormalize; nlapply (partialminus_n_S n' m'); ncases (partial_minus n' m'); ##[ ##1,2: nnormalize; #H; nrewrite > H; //; ##| #p; ncases p;   ##[ nnormalize; #H; nrewrite > H; //; ##| ##2,3: #p';nnormalize; #H; nrewrite > H; //; ##] ##] ##| #m'; nnormalize; nrewrite > (IH ?); //; ##] ##] nqed. ntheorem minus_S_S: ∀n,m:Pos. (succ n) - (succ m) = n-m. #n m; nnormalize; nrewrite > (partialminus_S_S n m); //; nqed. ntheorem minus_one_n: ∀n:Pos.one=one-n. #n; ncases n; //; nqed. ntheorem minus_n_one: ∀n:Pos.pred n=n-one. #n; ncases n; //; nqed. nlemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero. #n; nelim n; ##[ //; ##| ##2,3: nnormalize; #n' IH; nrewrite > IH; // ##] nqed. ntheorem minus_n_n: ∀n:Pos.one=n-n. #n; nnormalize; nrewrite > (partial_minus_n_n n); //; nqed. ntheorem minus_Sn_n: ∀n:Pos. one = (succ n)-n. #n; ncut (partial_minus (succ n) n = MinusPos one); ##[ nelim n; ##[ //; ##| nnormalize; #n' IH; nrewrite > IH; //; ##| nnormalize; #n' IH; nrewrite > (partial_minus_n_n n'); //; ##] ##| #H; nnormalize; nrewrite > H; //; ##] nqed. ntheorem minus_Sn_m: ∀m,n:Pos. m < n → succ n -m = succ (n-m). | #n' #IH #m cases m; [ normalize; cases n'; //; | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p; normalize; [ #H >H //; | 2,3: #p' #H >H //; ] ] |  #m' normalize; lapply (IH m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p; normalize; [ #H >H //; | 2,3: #p' #H >H //; ] ] ] | #n' #IH #m cases m; [ normalize; cases n'; //; | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p; normalize; [ #H >H //; | 2,3: #p' #H >H //; ] ] |  #m' normalize; lapply (IH m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p; normalize; [ #H >H //; | 2,3: #p' #H >H //; ] ] ] ] qed. theorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m. #n elim n; [ #m cases m; [ //; | 2,3: #m' cases m'; //; ] | #n' #IH #m cases m; [ normalize; cases n'; /2/; normalize; #n'' <(pred_succ_n n'') cases n'';//; | #m' normalize; >(IH ?) //; | #m' normalize; lapply (partialminus_S n' m'); cases (partial_minus (succ n') m'); [ 1,2: normalize; #H >H //; | #p cases p; [ normalize; #H >H //; | 2,3: #p' normalize; #H >H //; ] ] ] |  #n' #IH #m cases m; [ normalize; cases n'; /2/; | #m' normalize; lapply (partialminus_n_S n' m'); cases (partial_minus n' m'); [ 1,2: normalize; #H >H //; | #p cases p;   [ normalize; #H >H //; | 2,3: #p' normalize; #H >H //; ] ] | #m' normalize; >(IH ?) //; ] ] qed. theorem minus_S_S: ∀n,m:Pos. (succ n) - (succ m) = n-m. #n #m normalize; >(partialminus_S_S n m) //; qed. theorem minus_one_n: ∀n:Pos.one=one-n. #n cases n; //; qed. theorem minus_n_one: ∀n:Pos.pred n=n-one. #n cases n; //; qed. lemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero. #n elim n; [ //; | 2,3: normalize; #n' #IH >IH // ] qed. theorem minus_n_n: ∀n:Pos.one=n-n. #n normalize; >(partial_minus_n_n n) //; qed. theorem minus_Sn_n: ∀n:Pos. one = (succ n)-n. #n cut (partial_minus (succ n) n = MinusPos one); [ elim n; [ //; | normalize; #n' #IH >IH //; | normalize; #n' #IH >(partial_minus_n_n n') //; ] | #H normalize; >H //; ] qed. theorem minus_Sn_m: ∀m,n:Pos. m < n → succ n -m = succ (n-m). (* qualcosa da capire qui #n; #m; #lenm; nelim lenm; napplyS refl_eq. *) napply pos_elim2; ##[#n H; napply (lt_one_n_elim n H); //; ##|#n; #abs; napply False_ind; /2/ ##|#n; #m; #Hind; #c; napplyS Hind; /2/; ##] nqed. ntheorem not_eq_to_le_to_le_minus: #n #m #lenm elim lenm; napplyS refl_eq. *) @pos_elim2 [#n #H @(lt_one_n_elim n H) //; |#n #abs @False_ind /2/ |#n #m #Hind #c applyS Hind; /2/; ] qed. theorem not_eq_to_le_to_le_minus: ∀n,m:Pos.n ≠ m → n ≤ m → n ≤ m - one. #n; napply pos_cases; //; #m; #H; #H1; napply le_S_S_to_le; napplyS (not_eq_to_le_to_lt n (succ m) H H1); nqed. ntheorem eq_minus_S_pred: ∀n,m:Pos. n - (succ m) = pred(n -m). napply pos_elim2; ##[ #n; ncases n; nnormalize; //; ##| #n; napply (pos_elim … n); //; ##| //; ##] nqed. nlemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m). #n m H; napply (lt_one_n_elim … H); /3/; nqed. ntheorem plus_minus: #n @pos_cases //; #m #H #H1 @le_S_S_to_le applyS (not_eq_to_le_to_lt n (succ m) H H1); qed. theorem eq_minus_S_pred: ∀n,m:Pos. n - (succ m) = pred(n -m). @pos_elim2 [ #n cases n; normalize; //; | #n @(pos_elim … n) //; | //; ] qed. lemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m). #n #m #H @(lt_one_n_elim … H) /3/; qed. theorem plus_minus: ∀m,n,p:Pos. m < n → (n-m)+p = (n+p)-m. napply pos_elim2; ##[ #n p H; nrewrite < (minus_n_one ?); nrewrite < (minus_n_one ?); /2/; ##|#n; #p; #abs; napply False_ind; /2/; ##|#n m IH p H; nrewrite > (eq_minus_S_pred …); nrewrite > (eq_minus_S_pred …); ncut (n (pred_Sn_plus …); ##[ nrewrite > (minus_Sn_m …); /2/; nrewrite < (pluss_succn_m …); nrewrite < (pluss_succn_m …); nrewrite > (minus_Sn_m …); ##[ nrewrite < (pred_succ_n …); nrewrite < (pred_succ_n …); napply IH; /2/; ##| /2/; ##] ##| nrewrite > (minus_Sn_m … H'); //; ##] ##] nqed. @pos_elim2 [ #n #p #H <(minus_n_one ?) <(minus_n_one ?) /2/; |#n #p #abs @False_ind /2/; |#n #m #IH #p #H >(eq_minus_S_pred …) >(eq_minus_S_pred …) cut (n(pred_Sn_plus …) [ >(minus_Sn_m …) /2/; <(pluss_succn_m …) <(pluss_succn_m …) >(minus_Sn_m …) [ <(pred_succ_n …) <(pred_succ_n …) @IH /2/; | /2/; ] | >(minus_Sn_m … H') //; ] ] qed. (* XXX: putting this in the appropriate case screws up auto?! *) ntheorem succ_plus_one: ∀n. succ n = n + one. #n; nelim n; //; nqed. ntheorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p). #p; nelim p; nnormalize; ##[ //; ##| #q IH; nrewrite < (plus_n_O …); nrewrite < (plus_n_O …); nrewrite > IH; nrewrite < (plus_n_Sm …); //; ##| //; ##] nqed. ntheorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n. #n; nelim n; //; nqed. ntheorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m. #n; napply pos_elim; ##[ //; ##| #m IH; nrewrite < (plus_n_succm …); nrewrite > (eq_minus_S_pred …); nrewrite > (minus_Sn_m …); /2/; ##] nqed. ntheorem plus_minus_m_m: ∀n,m:Pos. theorem succ_plus_one: ∀n. succ n = n + one. #n elim n; //; qed. theorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p). #p elim p; normalize; [ //; | #q #IH <(plus_n_O …) <(plus_n_O …) >IH <(plus_n_Sm …) //; | //; ] qed. theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n. #n elim n; //; qed. theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m. #n @pos_elim [ //; | #m #IH <(plus_n_succm …) >(eq_minus_S_pred …) >(minus_Sn_m …) /2/; ] qed. theorem plus_minus_m_m: ∀n,m:Pos. m < n → n = (n-m)+m. #n; #m; #lemn; napplyS sym_eq; napplyS (plus_minus m n m); //; nqed. ntheorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (n-m)+m. napply pos_elim; ##[// ##|#a; #Hind; napply pos_cases; //; #n; nrewrite > (minus_S_S …); #n #m #lemn applyS sym_eq; applyS (plus_minus m n m); //; qed. theorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (n-m)+m. @pos_elim [// |#a #Hind @pos_cases //; #n >(minus_S_S …) /2/; ##] nqed. ntheorem minus_to_plus :∀n,m,p:Pos. ] qed. theorem minus_to_plus :∀n,m,p:Pos. m < n → n-m = p → n = m+p. #n; #m; #p; #lemn; #eqp; napplyS plus_minus_m_m; //; nqed. ntheorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p. #n #m #p #lemn #eqp applyS plus_minus_m_m; //; qed. theorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p. (* /4/ done in 43.5 *) #n; #m; #p; #eqp; napply sym_eq; napplyS (minus_plus_m_m p m); nqed. ntheorem minus_pred_pred : ∀n,m:Pos. one < n → one < m → #n #m #p #eqp @sym_eq applyS (minus_plus_m_m p m); qed. theorem minus_pred_pred : ∀n,m:Pos. one < n → one < m → pred n - pred m = n - m. #n; #m; #posn; #posm; napply (lt_one_n_elim n posn); napply (lt_one_n_elim m posm);//. nqed. #n #m #posn #posm @(lt_one_n_elim n posn) @(lt_one_n_elim m posm) //. qed. (* monotonicity and galois *) ntheorem monotonic_le_minus_l: theorem monotonic_le_minus_l: ∀p,q,n:Pos. q ≤ p → q-n ≤ p-n. napply pos_elim2; #p; #q; ##[#lePO; napply (le_n_one_elim ? lePO);//; ##|//; ##|#Hind; napply pos_cases; ##[/2/; ##|#a; #leSS; nrewrite > (minus_S_S …); nrewrite > (minus_S_S …); napply Hind; /2/; ##] ##] nqed. ntheorem le_minus_to_plus: ∀n,m,p:Pos. n-m ≤ p → n≤ p+m. #n; #m; #p; #lep; napply transitive_le; ##[##|napply le_plus_minus_m_m ##|napply monotonic_le_plus_l;//; ##] nqed. ntheorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → n-m ≤ p. #n; #m; #p; #lep; @pos_elim2 #p #q [#lePO @(le_n_one_elim ? lePO) //; |//; |#Hind @pos_cases [/2/; |#a #leSS >(minus_S_S …) >(minus_S_S …) @Hind /2/; ] ] qed. theorem le_minus_to_plus: ∀n,m,p:Pos. n-m ≤ p → n≤ p+m. #n #m #p #lep @transitive_le [|apply le_plus_minus_m_m |@monotonic_le_plus_l //; ] qed. theorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → n-m ≤ p. #n #m #p #lep (* bello *) napplyS monotonic_le_minus_l;//; applyS monotonic_le_minus_l;//; (* /2/; *) nqed. ntheorem monotonic_le_minus_r: qed. theorem monotonic_le_minus_r: ∀p,q,n:Pos. q ≤ p → n-p ≤ n-q. #p; #q; #n; #lepq; napply le_plus_to_minus; napply (transitive_le ??? (le_plus_minus_m_m ? q));/2/; nqed. #p #q #n #lepq @le_plus_to_minus @(transitive_le ??? (le_plus_minus_m_m ? q)) /2/; qed. (*********************** boolean arithmetics ********************) include "basics/bool.ma". nlet rec eqb n m ≝ let rec eqb n m ≝ match n with [ one ⇒ match m with [ one ⇒ true | _ ⇒ false] | p1 p ⇒ match m with [ p1 q ⇒ eqb p q | _ ⇒ false] ]. ntheorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop. theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop. (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). #n; nelim n; ##[ #m; ncases m; nnormalize; ##[ /2/; ##| ##2,3: #m' P t f; napply f; @; #H; ndestruct; ##] ##| #n' IH m; ncases m; nnormalize; ##[ #P t f; napply f; @; #H; ndestruct; ##| #m' P t f; napply IH; ##[ /2/; ##| (* XXX: automation assertion *) #ne; napply f; @; #e; ndestruct; nelim ne; /2/; ##] ##| #m' P t f; napply f; @; #H; ndestruct; ##] ##| #n' IH m; ncases m; nnormalize; ##[ #P t f; napply f; @; #H; ndestruct; ##| #m' P t f; napply f; @; #H; ndestruct; ##| #m' P t f; napply IH; ##[ /2/; ##| (* XXX: automation assertion *) #ne; napply f; @; #e; ndestruct; nelim ne; /2/; ##] ##] ##] nqed. ntheorem eqb_n_n: ∀n:Pos. eqb n n = true. #n; nelim n; nnormalize; //. nqed. ntheorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m. #n; #m; napply (eqb_elim n m);//; #_; #abs; napply False_ind; /2/; nqed. ntheorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m. #n; #m; napply (eqb_elim n m);/2/; nqed. ntheorem eq_to_eqb_true: ∀n,m:Pos. #n elim n; [ #m cases m normalize [ /2/ | 2,3: #m' #P #t #f @f % #H destruct ] | #n' #IH #m cases m normalize [ #P #t #f @f % #H destruct | #m' #P #t #f @IH [ /2/ | * #ne @f % #e @ne destruct @refl ] | #m' #P #t #f @f % #H destruct; ] | #n' #IH #m cases m; normalize; [ #P #t #f @f % #H destruct; | #m' #P #t #f @f % #H destruct; | #m' #P #t #f @IH [ /2/; | * #ne @f % #e @ne destruct @refl ] ] ] qed. theorem eqb_n_n: ∀n:Pos. eqb n n = true. #n elim n; normalize; //. qed. theorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m. #n #m @(eqb_elim n m) //; #_ #abs @False_ind /2/; qed. theorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m. #n #m @(eqb_elim n m) /2/; qed. theorem eq_to_eqb_true: ∀n,m:Pos. n = m → eqb n m = true. //; nqed. ntheorem not_eq_to_eqb_false: ∀n,m:Pos. //; qed. theorem not_eq_to_eqb_false: ∀n,m:Pos. n ≠  m → eqb n m = false. #n; #m; #noteq; napply eqb_elim;//; #Heq; napply False_ind; /2/; nqed. nlet rec leb n m ≝ #n #m #noteq @eqb_elim //; #Heq @False_ind /2/; qed. let rec leb n m ≝ match partial_minus n m with [ MinusNeg ⇒ true ]. nlemma leb_unfold_hack: ∀n,m:Pos. leb n m = lemma leb_unfold_hack: ∀n,m:Pos. leb n m = match partial_minus n m with [ MinusNeg ⇒ true | MinusZero ⇒ true | MinusPos _ ⇒ false ]. #n m; (* XXX: why on earth do I need to case split? *) ncases n; //; nqed. ntheorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop. ]. #n #m (* XXX: why on earth do I need to case split? *) cases n; //; qed. theorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop. (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m). napply pos_elim2; ##[ #n; ncases n; nnormalize; /2/; ##| #n; ncases n; nnormalize; ##[ /2/; ##| ##2,3: #m' P t f; napply f; /2/; @; #H; ninversion H; ##[ #H'; ndestruct; ##| #p; /2/; ##] ##] ##| #n m IH P t f; nrewrite > (leb_unfold_hack …); nrewrite > (partialminus_S_S n m); nrewrite < (leb_unfold_hack …); napply IH; #H; /3/; ##] nqed. ntheorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m. #n; #m; napply leb_elim; ##[//; ##|#_; #abs; napply False_ind; /2/; ##] nqed. ntheorem leb_false_to_not_le:∀n,m:Pos. @pos_elim2 [ #n cases n; normalize; /2/; | #n cases n; normalize; [ /2/; | 2,3: #m' #P #t #f @f /2/; % #H inversion H; [ #H' destruct; | #p /2/; ] ] | #n #m #IH #P #t #f >(leb_unfold_hack …) >(partialminus_S_S n m) <(leb_unfold_hack …) @IH #H /3/; ] qed. theorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m. #n #m @leb_elim [//; |#_ #abs @False_ind /2/; ] qed. theorem leb_false_to_not_le:∀n,m:Pos. leb n m = false → n ≰ m. #n; #m; napply leb_elim; ##[#_; #abs; napply False_ind; /2/; ##|//; ##] nqed. ntheorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true. #n; #m; napply leb_elim; //; #H; #H1; napply False_ind; /2/; nqed. ntheorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false. #n; #m; napply leb_elim; //; #H; #H1; napply False_ind; /2/; nqed. ntheorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false. /3/; nqed. #n #m @leb_elim [#_ #abs @False_ind /2/; |//; ] qed. theorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true. #n #m @leb_elim //; #H #H1 @False_ind /2/; qed. theorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false. #n #m @leb_elim //; #H #H1 @False_ind /2/; qed. theorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false. /3/; qed. (***** comparison *****) ndefinition pos_compare : Pos → Pos → compare ≝ definition pos_compare : Pos → Pos → compare ≝ λn,m.match partial_minus n m with [ MinusNeg ⇒ LT ]. ntheorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ. #n; nnormalize; nrewrite > (partial_minus_n_n n); //; nqed. ntheorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m). #n m; nnormalize; nrewrite > (partialminus_S_S …); theorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ. #n normalize; >(partial_minus_n_n n) //; qed. theorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m). #n #m normalize; >(partialminus_S_S …) //; nqed. ntheorem pos_compare_pred_pred: qed. theorem pos_compare_pred_pred: ∀n,m.one < n → one < m → pos_compare n m = pos_compare (pred n) (pred m). #n;#m;#Hn;#Hm; napply (lt_one_n_elim n Hn); napply (lt_one_n_elim m Hm); #p;#q; nrewrite < (pred_succ_n ?); nrewrite < (pred_succ_n ?); nrewrite < (pos_compare_S_S …); //; nqed. ntheorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT. #n; nelim n; //; nqed. ntheorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT. #n; nelim n; //; nqed. ntheorem pos_compare_to_Prop: #n #m #Hn #Hm @(lt_one_n_elim n Hn) @(lt_one_n_elim m Hm) #p #q <(pred_succ_n ?) <(pred_succ_n ?) <(pos_compare_S_S …) //; qed. theorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT. #n elim n; //; qed. theorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT. #n elim n; //; qed. theorem pos_compare_to_Prop: ∀n,m.match (pos_compare n m) with [ LT ⇒ n < m | EQ ⇒ n = m | GT ⇒ m < n ]. #n;#m; napply (pos_elim2 (λn,m.match (pos_compare n m) with #n #m @(pos_elim2 (λn,m.match (pos_compare n m) with [ LT ⇒ n < m | EQ ⇒ n = m | GT ⇒ m < n ]) ?????) (* FIXME: don't want to put all these ?, especially when … does not work! *) ##[##1,2:napply pos_cases; ##[ ##1,3: /2/; ##| ##2,4: #m'; ncases m'; //; ##] ##|#n1;#m1;nnormalize;nrewrite < (pos_compare_S_S …); ncases (pos_compare n1 m1); ##[##1,3:nnormalize;#IH;napply le_succ_succ;//; ##|nnormalize;#IH;nrewrite > IH;//] nqed. ntheorem pos_compare_n_m_m_n: [1,2:@pos_cases [ 1,3: /2/; | 2,4: #m' cases m'; //; ] |#n1 #m1 normalize;<(pos_compare_S_S …) cases (pos_compare n1 m1); [1,3:normalize;#IH @le_succ_succ //; |normalize;#IH >IH //] qed. theorem pos_compare_n_m_m_n: ∀n,m:Pos.pos_compare n m = compare_invert (pos_compare m n). #n;#m; napply (pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n))) ##[##1,2:#n1;ncases n1;/2/; ##|#n1;#m1; nrewrite < (pos_compare_S_S …); nrewrite < (pos_compare_S_S …); #IH;nnormalize;napply IH] nqed. #n #m @(pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n))) [1,2:#n1 cases n1;/2/; |#n1 #m1 <(pos_compare_S_S …) <(pos_compare_S_S …) #IH normalize @IH] qed. ntheorem pos_compare_elim : theorem pos_compare_elim : ∀n,m:Pos. ∀P:compare → Prop. (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (pos_compare n m). #n;#m;#P;#Hlt;#Heq;#Hgt; ncut (match (pos_compare n m) with #n #m #P #Hlt #Heq #Hgt cut (match (pos_compare n m) with [ LT ⇒ n < m | EQ ⇒ n=m | GT ⇒ m < n] → P (pos_compare n m)) ##[ncases (pos_compare n m); ##[napply Hlt ##|napply Heq ##|napply Hgt] ##|#Hcut;napply Hcut;//; nqed. ninductive cmp_cases (n,m:Pos) : CProp[0] ≝ [cases (pos_compare n m); [@Hlt |@Heq |@Hgt] |#Hcut @Hcut //; qed. inductive cmp_cases (n,m:Pos) : CProp[0] ≝ | cmp_le : n ≤ m → cmp_cases n m | cmp_gt : m < n → cmp_cases n m. ntheorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m. theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m. (* sic #n;#m;#H;nelim H ##[// ##|/2/] *) /2/; nqed. nlemma cmp_nat: ∀n,m:Pos.cmp_cases n m. #n;#m; nlapply (pos_compare_to_Prop n m); ncases (pos_compare n m);nnormalize; /3/; nqed. nlet rec two_power_nat (n:nat) : Pos ≝ #n #m #H elim H [// |/2/] *) /2/; qed. lemma cmp_nat: ∀n,m:Pos.cmp_cases n m. #n #m lapply (pos_compare_to_Prop n m) cases (pos_compare n m);normalize; /3/; qed. let rec two_power_nat (n:nat) : Pos ≝ match n with [ O ⇒ one ]. ndefinition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p). definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p).
Note: See TracChangeset for help on using the changeset viewer.