(**************************************************************************) (* ___ *) (* ||M|| *) (* ||A|| A project by Andrea Asperti *) (* ||T|| *) (* ||I|| Developers: *) (* ||T|| The HELM team. *) (* ||A|| http://helm.cs.unibo.it *) (* \ / *) (* \ / This file is distributed under the terms of the *) (* v GNU General Public License Version 2 *) (* *) (**************************************************************************) (* This includes a lot of copied code from arithmetics/Z.ma, so some of the comments may no longer be applicable. *) (*include "arithmetics/compare.ma".*) include "utilities/binary/positive.ma". inductive Z : Type[0] ≝ OZ : Z | pos : Pos → Z | neg : Pos → Z. (*interpretation "Integers" 'D = Z.*) definition Z_of_nat ≝ λn. match n with [ O ⇒ OZ | S n ⇒ pos (succ_pos_of_nat n)]. 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)]. definition abs ≝ λz.match z with [ OZ ⇒ O | pos n ⇒ nat_of_pos n | neg n ⇒ nat_of_pos n]. definition OZ_test ≝ λz.match z with [ OZ ⇒ true | pos _ ⇒ false | neg _ ⇒ false]. theorem OZ_test_to_Prop : ∀z:Z. match OZ_test z with [true ⇒ z=OZ |false ⇒ z ≠ OZ]. #z cases z [ @refl |*:#z1 @nmk #H destruct] qed. (* discrimination *) 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. *) 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. *) 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 | pos n ⇒ pos (succ n) | neg n ⇒ match n with [ one ⇒ OZ | _ ⇒ neg (pred n)]]. definition Zpred ≝ λz. match z with [ OZ ⇒ neg one | pos n ⇒ match n with [ one ⇒ OZ | _ ⇒ pos (pred n)] | neg n ⇒ neg (succ n)]. 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 ⇒ match y with [ OZ ⇒ True | pos m ⇒ True | neg m ⇒ False ] | pos n ⇒ match y with [ OZ ⇒ False | pos m ⇒ n ≤ m | neg m ⇒ False ] | neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ True | neg m ⇒ m ≤ n ]]. interpretation "integer 'less or equal to'" 'leq x y = (Zle x y). interpretation "integer 'neither less nor equal to'" 'nleq x y = (Not (Zle x y)). let rec Zlt (x:Z) (y:Z) on x : Prop ≝ match x with [ OZ ⇒ match y with [ OZ ⇒ False | pos m ⇒ True | neg m ⇒ False ] | pos n ⇒ match y with [ OZ ⇒ False | pos m ⇒ n(Zsucc_neg_succ m) @le_S_S_to_le (* XXX: auto? *) ] ] ] qed. (*** COMPARE ***) (* boolean equality *) let rec eqZb (x:Z) (y:Z) on x : bool ≝ match x with [ OZ ⇒ match y with [ OZ ⇒ true | pos q ⇒ false | neg q ⇒ false] | pos p ⇒ match y with [ OZ ⇒ false | pos q ⇒ eqb p q | neg q ⇒ false] | neg p ⇒ match y with [ OZ ⇒ false | pos q ⇒ false | neg q ⇒ eqb p q]]. theorem eqZb_to_Prop: ∀x,y:Z. match eqZb x y with [ true ⇒ x=y | false ⇒ x ≠ y]. #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 normalize @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 normalize @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 cut (match (eqZb x y) with [ true ⇒ x=y | false ⇒ x ≠ y] → P (eqZb x y)) [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 ⇒ match y with [ OZ ⇒ EQ | pos m ⇒ LT | neg m ⇒ GT ] | pos n ⇒ match y with [ OZ ⇒ GT | pos m ⇒ pos_compare n m | neg m ⇒ GT] | neg n ⇒ match y with [ OZ ⇒ LT | pos m ⇒ LT | neg m ⇒ pos_compare m n ]]. 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 elim x [elim y;//; |elim y [1,3:// |#n #m normalize; cut (match (pos_compare m n) with [ LT ⇒ m < n | EQ ⇒ m = n | GT ⇒ n < m ] → match (pos_compare m n) with [ LT ⇒ (succ m) ≤ n | EQ ⇒ pos m = pos n | GT ⇒ (succ n) ≤ m]) [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 | GT ⇒ m < n] → match (pos_compare n m) with [ LT ⇒ (succ n) ≤ m | EQ ⇒ neg m = neg n | GT ⇒ (succ m) ≤ n]) [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 | pos m ⇒ match y with [ OZ ⇒ x | pos n ⇒ (pos (m + n)) | neg n ⇒ match pos_compare m n with [ LT ⇒ (neg (n-m)) | EQ ⇒ OZ | GT ⇒ (pos (m-n))] ] | neg m ⇒ match y with [ OZ ⇒ x | pos n ⇒ match pos_compare m n with [ LT ⇒ (pos (n-m)) | EQ ⇒ OZ | GT ⇒ (neg (m-n))] | neg n ⇒ (neg (m + n))] ]. interpretation "integer plus" 'plus x y = (Zplus x y). 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 // |#p cases y [// |// |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n cases (pos_compare q p);//] |#p cases y [//; |#q whd in ⊢ (??%%) >pos_compare_n_m_m_n 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 @(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 whd in ⊢ (??%%) <(pos_compare_S_S …) >(minus_S_S …) >(minus_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 @(pos_cases … n) @(pos_cases … m) [ //; | #m' >Zpred_pos_succ change in ⊢ (??(??%)?) with (Zsucc (pos m')) Zpred_Zsucc @refl | #m' whd in ⊢ (??%%) >pos_compare_S_one normalize; >partial_minus_S_one normalize; >pos_nonzero minus_S_S >minus_S_S normalize >pos_nonzero >pos_nonzero (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 >(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 @(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 @(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 whd in ⊢ (??%%) minus_S_S >minus_S_S //; qed. theorem Zplus_Zsucc_neg_pos: ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)). #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 @(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 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) \def associative_Zplus. *) (* Zopp *) definition Zopp : Z → Z ≝ λx:Z. match x with [ OZ ⇒ OZ | pos n ⇒ neg n | neg n ⇒ pos n ]. interpretation "integer unary minus" 'uminus x = (Zopp x). theorem eq_OZ_Zopp_OZ : OZ = (- OZ). //; qed. theorem Zopp_Zplus: ∀x,y:Z. -(x+y) = -x + -y. #x #y cases x [cases y;// |*:#n cases y;//;#m whd in ⊢ (??(?%)%) @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 whd in ⊢ (??%?) >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 ???) //; qed. theorem injective_Zplus_r: ∀x:Z.injective Z Z (λy.x+y). #x #z #y #H @(injective_Zplus_l x) <(sym_Zplus ??) //; qed. (* minus *) definition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y). interpretation "integer minus" 'minus x y = (Zminus x y). 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 | pos p ⇒ pos (two_power_pos p) | neg _ ⇒ OZ (* same fib as Coq *) ].