From: Andrea Asperti Date: Tue, 23 Mar 2010 07:31:12 +0000 (+0000) Subject: Moved compare in a different file. X-Git-Tag: make_still_working~2985 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=81e3d11cbb2a7a6498b4b19876bbb5ababc8942b;p=helm.git Moved compare in a different file. From: asperti --- diff --git a/helm/software/matita/nlibrary/arithmetics/compare.ma b/helm/software/matita/nlibrary/arithmetics/compare.ma new file mode 100644 index 000000000..68e141155 --- /dev/null +++ b/helm/software/matita/nlibrary/arithmetics/compare.ma @@ -0,0 +1,109 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| A.Asperti, C.Sacerdoti Coen, *) +(* ||A|| E.Tassi, S.Zacchiroli *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU Lesser General Public License Version 2.1 *) +(* *) +(**************************************************************************) + +include "arithmetics/nat.ma". + +ninductive compare : Type[0] ≝ +| LT : compare +| EQ : compare +| GT : compare. + +ndefinition compare_invert: compare → compare ≝ + λc.match c with + [ LT ⇒ GT + | EQ ⇒ EQ + | GT ⇒ LT ]. + +nlet rec nat_compare n m: compare ≝ +match n with +[ O ⇒ match m with + [ O ⇒ EQ + | (S q) ⇒ LT ] +| S p ⇒ match m with + [ O ⇒ GT + | S q ⇒ nat_compare p q]]. + +ntheorem nat_compare_n_n: ∀n. nat_compare n n = EQ. +#n;nelim n +##[// +##|#m;#IH;nnormalize;//] +nqed. + +ntheorem nat_compare_S_S: ∀n,m:nat.nat_compare n m = nat_compare (S n) (S m). +//; +nqed. + +ntheorem nat_compare_pred_pred: + ∀n,m.O < n → O < m → nat_compare n m = nat_compare (pred n) (pred m). +#n;#m;#Hn;#Hm; +napply (lt_O_n_elim n Hn); +napply (lt_O_n_elim m Hm); +#p;#q;//; +nqed. + +ntheorem nat_compare_to_Prop: + ∀n,m.match (nat_compare n m) with + [ LT ⇒ n < m + | EQ ⇒ n = m + | GT ⇒ m < n ]. +#n;#m; +napply (nat_elim2 (λn,m.match (nat_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:#n1;ncases n1;//; +##|#n1;#m1;nnormalize;ncases (nat_compare n1 m1); + ##[##1,3:nnormalize;#IH;napply le_S_S;//; + ##|nnormalize;#IH;nrewrite > IH;//] +nqed. + +ntheorem nat_compare_n_m_m_n: + ∀n,m:nat.nat_compare n m = compare_invert (nat_compare m n). +#n;#m; +napply (nat_elim2 (λn,m. nat_compare n m = compare_invert (nat_compare m n))) +##[##1,2:#n1;ncases n1;//; +##|#n1;#m1;#IH;nnormalize;napply IH] +nqed. + +ntheorem nat_compare_elim : + ∀n,m. ∀P:compare → Prop. + (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (nat_compare n m). +#n;#m;#P;#Hlt;#Heq;#Hgt; +ncut (match (nat_compare n m) with + [ LT ⇒ n < m + | EQ ⇒ n=m + | GT ⇒ m < n] → + P (nat_compare n m)) +##[ncases (nat_compare n m); + ##[napply Hlt + ##|napply Heq + ##|napply Hgt] +##|#Hcut;napply Hcut;//; +nqed. + +ninductive cmp_cases (n,m:nat) : CProp[0] ≝ + | cmp_le : n ≤ m → cmp_cases n m + | cmp_gt : m < n → cmp_cases n m. + +ntheorem lt_to_le : ∀n,m:nat. n < m → n ≤ m. +(* sic +#n;#m;#H;nelim H +##[// +##|/2/] *) +/2/; nqed. + +nlemma cmp_nat: ∀n,m.cmp_cases n m. +#n;#m; nlapply (nat_compare_to_Prop n m); +ncases (nat_compare n m);nnormalize; /3/; +nqed. diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma index fe9ef8267..54ff253c2 100644 --- a/helm/software/matita/nlibrary/arithmetics/nat.ma +++ b/helm/software/matita/nlibrary/arithmetics/nat.ma @@ -17,11 +17,7 @@ include "hints_declaration.ma". include "basics/functions.ma". include "basics/eq.ma". -ntheorem foo: ∀A:Type.∀a,b:A.∀f:A→A.∀g:A→A→A. -(∀x,y.f (g x y) = x) → ∀x. g (f a) x = b → f a = f b. -//; nqed. - -ninductive nat : Type[0] ≝ +ninductive nat : Type ≝ | O : nat | S : nat → nat. @@ -40,7 +36,7 @@ ncoercion nat_to_pos: ∀n:nat. n ≠0 →pos ≝ mk_pos on *) ndefinition pred ≝ - λn. match n with [ O ⇒ O | (S p) ⇒ p]. + λn. match n with [ O ⇒ O | S p ⇒ p]. ntheorem pred_Sn : ∀n. n = pred (S n). //; nqed. @@ -278,6 +274,7 @@ ntheorem monotonic_pred: monotonic ? le pred. ntheorem le_S_S_to_le: ∀n,m:nat. S n ≤ S m → n ≤ m. (* XXX *) nletin hint ≝ monotonic. +#a; #b; #H; napplyS monotonic_pred; /2/; nqed. (* this are instances of the le versions @@ -566,7 +563,6 @@ ntheorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m ntheorem monotonic_le_plus_l: ∀m:nat.monotonic nat le (λn.n + m). -#m; #x; #y; #H; napplyS monotonic_le_plus_r; /2/; nqed. (* @@ -1156,98 +1152,3 @@ ntheorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false. #n; #m; #Hltb; napply lt_to_leb_false; /2/; nqed. *) -ninductive compare : Type[0] ≝ -| LT : compare -| EQ : compare -| GT : compare. - -ndefinition compare_invert: compare → compare ≝ - λc.match c with - [ LT ⇒ GT - | EQ ⇒ EQ - | GT ⇒ LT ]. - -nlet rec nat_compare n m: compare ≝ -match n with -[ O ⇒ match m with - [ O ⇒ EQ - | (S q) ⇒ LT ] -| S p ⇒ match m with - [ O ⇒ GT - | S q ⇒ nat_compare p q]]. - -ntheorem nat_compare_n_n: ∀n. nat_compare n n = EQ. -#n;nelim n -##[// -##|#m;#IH;nnormalize;//] -nqed. - -ntheorem nat_compare_S_S: ∀n,m:nat.nat_compare n m = nat_compare (S n) (S m). -//; -nqed. - -ntheorem nat_compare_pred_pred: - ∀n,m.O < n → O < m → nat_compare n m = nat_compare (pred n) (pred m). -#n;#m;#Hn;#Hm; -napply (lt_O_n_elim n Hn); -napply (lt_O_n_elim m Hm); -#p;#q;//; -nqed. - -ntheorem nat_compare_to_Prop: - ∀n,m.match (nat_compare n m) with - [ LT ⇒ n < m - | EQ ⇒ n = m - | GT ⇒ m < n ]. -#n;#m; -napply (nat_elim2 (λn,m.match (nat_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:#n1;ncases n1;//; -##|#n1;#m1;nnormalize;ncases (nat_compare n1 m1); - ##[##1,3:nnormalize;#IH;napply le_S_S;//; - ##|nnormalize;#IH;nrewrite > IH;//] -nqed. - -ntheorem nat_compare_n_m_m_n: - ∀n,m:nat.nat_compare n m = compare_invert (nat_compare m n). -#n;#m; -napply (nat_elim2 (λn,m. nat_compare n m = compare_invert (nat_compare m n))) -##[##1,2:#n1;ncases n1;//; -##|#n1;#m1;#IH;nnormalize;napply IH] -nqed. - -ntheorem nat_compare_elim : - ∀n,m. ∀P:compare → Prop. - (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (nat_compare n m). -#n;#m;#P;#Hlt;#Heq;#Hgt; -ncut (match (nat_compare n m) with - [ LT ⇒ n < m - | EQ ⇒ n=m - | GT ⇒ m < n] → - P (nat_compare n m)) -##[ncases (nat_compare n m); - ##[napply Hlt - ##|napply Heq - ##|napply Hgt] -##|#Hcut;napply Hcut;//; -nqed. - -ninductive cmp_cases (n,m:nat) : CProp[0] ≝ - | cmp_le : n ≤ m → cmp_cases n m - | cmp_gt : m < n → cmp_cases n m. - -ntheorem lt_to_le : ∀n,m:nat. n < m → n ≤ m. -#n;#m;#H;nelim H -##[// -##|/2/] -nqed. - -nlemma cmp_nat: ∀n,m.cmp_cases n m. -#n;#m; nlapply (nat_compare_to_Prop n m); -ncases (nat_compare n m);#H -##[@;napply lt_to_le;// -##|@;// -##|@2;//] -nqed.