From edccb29109d07b54b48230a280f4351ed042dd9f Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 2 Mar 2010 16:19:18 +0000 Subject: [PATCH] Some integrations to the ng library. --- .../software/matita/nlibrary/arithmetics/Z.ma | 631 ++++++++++++++++++ .../matita/nlibrary/arithmetics/nat.ma | 96 +++ .../matita/nlibrary/datatypes/list.ma | 333 +++++++++ .../matita/nlibrary/datatypes/pairs.ma | 13 +- .../matita/nlibrary/datatypes/sums.ma | 29 + .../matita/nlibrary/logic/equality.ma | 92 ++- helm/software/matita/nlibrary/sets/sets.ma | 6 +- 7 files changed, 1195 insertions(+), 5 deletions(-) create mode 100644 helm/software/matita/nlibrary/arithmetics/Z.ma create mode 100644 helm/software/matita/nlibrary/datatypes/list.ma create mode 100644 helm/software/matita/nlibrary/datatypes/sums.ma diff --git a/helm/software/matita/nlibrary/arithmetics/Z.ma b/helm/software/matita/nlibrary/arithmetics/Z.ma new file mode 100644 index 000000000..7a0f7f080 --- /dev/null +++ b/helm/software/matita/nlibrary/arithmetics/Z.ma @@ -0,0 +1,631 @@ +(**************************************************************************) +(* ___ *) +(* ||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 Z : Type ≝ + OZ : Z +| pos : nat → Z +| neg : nat → Z. + +interpretation "Integers" 'Z = Z. + +ndefinition Z_of_nat ≝ +λn. match n with +[ O ⇒ OZ +| S n ⇒ pos n]. + +ncoercion Z_of_nat : ∀n:nat.Z ≝ Z_of_nat on _n:nat to Z. + +ndefinition neg_Z_of_nat \def +λn. match n with +[ O ⇒ OZ +| S n ⇒ neg n]. + +nlemma pos_n_eq_S_n : ∀n : nat.pos n = S n. +//. +nqed. + +ndefinition abs ≝ +λz.match z with +[ OZ ⇒ O +| pos n ⇒ S n +| neg n ⇒ S n]. + +ndefinition OZ_test ≝ +λz.match z with +[ OZ ⇒ true +| pos _ ⇒ false +| neg _ ⇒ false]. + +ntheorem OZ_test_to_Prop : ∀z:Z. + match OZ_test z with + [true ⇒ z=OZ + |false ⇒ z ≠ OZ]. +#z;ncases z +##[napply refl +##|##*:#z1;#H;ndestruct] +nqed. + +(* discrimination *) +ntheorem injective_pos: injective nat Z pos. +#n;#m;#H;ndestruct;//; +nqed. + +(* variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m +\def injective_pos. *) + +ntheorem injective_neg: injective nat Z neg. +#n;#m;#H;ndestruct;//; +nqed. + +(* variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m +\def injective_neg. *) + +ntheorem not_eq_OZ_pos: ∀n:nat. OZ ≠ pos n. +#n;#H;ndestruct; +nqed. + +ntheorem not_eq_OZ_neg :∀n:nat. OZ ≠ neg n. +#n;#H;ndestruct; +nqed. + +ntheorem not_eq_pos_neg : ∀n,m:nat. pos n ≠ neg m. +#n;#m;#H;ndestruct; +nqed. + +ntheorem decidable_eq_Z : ∀x,y:Z. decidable (x=y). +#x;#y;ncases x; +##[ncases y; + ##[@;// + ##|##*:#n;@2;#H;ndestruct] +##|#n;ncases y; + ##[@2;#H;ndestruct; + ##|#m;ncases (decidable_eq_nat n m);#H; + ##[nrewrite > H;@;// + ##|@2;#H2;napply H;ndestruct;//] + ##|#m;@2;#H;ndestruct] +##|#n;ncases y; + ##[@2;#H;ndestruct; + ##|#m;@2;#H;ndestruct + ##|#m;ncases (decidable_eq_nat n m);#H; + ##[nrewrite > H;@;// + ##|@2;#H2;napply H;ndestruct;//]##]##] +nqed. + +ndefinition Zsucc ≝ +λz. match z with +[ OZ ⇒ pos O +| pos n ⇒ pos (S n) +| neg n ⇒ + match n with + [ O ⇒ OZ + | S p ⇒ neg p]]. + +ndefinition Zpred ≝ +λz. match z with +[ OZ ⇒ neg O +| pos n ⇒ + match n with + [ O ⇒ OZ + | S p ⇒ pos p] +| neg n ⇒ neg (S n)]. + +ntheorem Zpred_Zsucc: ∀z:Z. Zpred (Zsucc z) = z. +#z;ncases z; +##[##1,2:// +##|#n;ncases n;//] +nqed. + +ntheorem Zsucc_Zpred: ∀z:Z. Zsucc (Zpred z) = z. +#z;ncases z +##[##2:#n;ncases n;// +##|##*://] +nqed. + +ndefinition Zle : Z → Z → Prop ≝ +λx,y:Z. + 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)). + +ndefinition Zlt : Z → Z → Prop ≝ +λx,y:Z. + 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 (Zplus_z_OZ ?) (*XXX*);// +##|#p;ncases y + ##[// + ##|nnormalize;// + ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*); + ncases (nat_compare q p);//] +##|#p;ncases y + ##[//; + ##|#q;nnormalize;nrewrite > (nat_compare_n_m_m_n ??) (*XXX*); + ncases (nat_compare q p);// + ##|nnormalize;//] +##] +nqed. + +ntheorem Zpred_Zplus_neg_O : ∀z. Zpred z = (neg O)+z. +#z;ncases z +##[// +##|##*:#n;ncases n;//] +nqed. + +ntheorem Zsucc_Zplus_pos_O : ∀z. Zsucc z = (pos O)+z. +#z;ncases z +##[// +##|##*:#n;ncases n;//] +nqed. + +ntheorem Zplus_pos_pos: + ∀n,m. (pos n)+(pos m) = (Zsucc (pos n))+(Zpred (pos m)). +#n;#m;ncases n +##[ncases m;// +##|#p;ncases m + ##[nnormalize; + nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_O ?); (* XXX yet again *) + // + ##|#q;nnormalize;nrewrite < (plus_n_Sm ??);nrewrite < (plus_n_Sm ??);//] +##] +nqed. + +ntheorem Zplus_pos_neg: + ∀n,m. (pos n)+(neg m) = (Zsucc (pos n))+(Zpred (neg m)). +//; +nqed. + +ntheorem Zplus_neg_pos : + ∀n,m. (neg n)+(pos m) = (Zsucc (neg n))+(Zpred (pos m)). +#n;#m;ncases n;ncases m;//; +nqed. + +ntheorem Zplus_neg_neg: + ∀n,m. (neg n)+(neg m) = (Zsucc (neg n))+(Zpred (neg m)). +#n;#m;ncases n +##[ncases m;// +##|#p;ncases m;nnormalize; + ##[nrewrite > (plus_n_Sm ??);// + ##|#q;nrewrite > (plus_n_Sm ??);//] +##] +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 ?);// + ##|//] +##|ncases y;// +##|ncases y + ##[#n;nrewrite < (sym_Zplus ??);nrewrite < (sym_Zplus (Zpred OZ) ?); + nrewrite < (Zpred_Zplus_neg_O ?);nrewrite > (Zpred_Zsucc ?);// + ##|##*://] +nqed. + +ntheorem Zplus_Zsucc_pos_pos : + ∀n,m. (Zsucc (pos n))+(pos m) = Zsucc ((pos n)+(pos m)). +//; +nqed. + +ntheorem Zplus_Zsucc_pos_neg: + ∀n,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))). +#n;#m; +napply (nat_elim2 (λn,m. (Zsucc (pos n))+(neg m) = (Zsucc ((pos n)+(neg m))))) +##[#n1;nelim n1 + ##[// + ##|#n2;#IH;nelim n2;//] +##|// +##|#n1;#m1;#IH;nrewrite < (Zplus_pos_neg ? m1);nelim IH;//] +nqed. + +ntheorem Zplus_Zsucc_neg_neg : + ∀n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m). +#n;#m; +napply (nat_elim2 (λ n,m. Zsucc (neg n) + neg m = Zsucc (neg n + neg m))) +##[#n1;nelim n1 + ##[// + ##|#n2;#IH;nelim n2;//] +##|##*://] +nqed. + +ntheorem Zplus_Zsucc_neg_pos: + ∀n,m. Zsucc (neg n)+(pos m) = Zsucc ((neg n)+(pos m)). +#n;#m; +napply (nat_elim2 (λn,m. Zsucc (neg n) + (pos m) = Zsucc (neg n + pos m))) +##[#n1;nelim n1 + ##[// + ##|#n2;#IH;nelim n2;//] +##|// +##|#n1;#m1;#IH;nrewrite < IH;nrewrite < (Zplus_neg_pos ? (S m1));//] +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;//] +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. + +ntheorem associative_Zplus: associative Z Zplus. +(* nchange with (\forall x,y,z:Z. (x + y) + z = x + (y + z));*) +#x;#y;#z;ncases x +##[// +##|#n;nelim n + ##[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) ?);//] +##|#n;nelim n + ##[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. + +(* variant assoc_Zplus : \forall x,y,z:Z. (x+y)+z = x+(y+z) +\def associative_Zplus. *) + +(* Zopp *) +ndefinition 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). + +ntheorem 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 nat_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 > (nat_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 ???); +//; +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 ??); +//; +nqed. + +(* minus *) +ndefinition Zminus : Z → Z → Z ≝ λx,y:Z. x + (-y). + +interpretation "integer minus" 'minus x y = (Zminus x y). \ No newline at end of file diff --git a/helm/software/matita/nlibrary/arithmetics/nat.ma b/helm/software/matita/nlibrary/arithmetics/nat.ma index 120a0bb16..25745e370 100644 --- a/helm/software/matita/nlibrary/arithmetics/nat.ma +++ b/helm/software/matita/nlibrary/arithmetics/nat.ma @@ -1135,3 +1135,99 @@ nqed. 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. diff --git a/helm/software/matita/nlibrary/datatypes/list.ma b/helm/software/matita/nlibrary/datatypes/list.ma new file mode 100644 index 000000000..0e1337725 --- /dev/null +++ b/helm/software/matita/nlibrary/datatypes/list.ma @@ -0,0 +1,333 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "arithmetics/nat.ma". + +ninductive list (A:Type[0]) : Type[0] ≝ + | nil: list A + | cons: A -> list A -> list A. + +notation "hvbox(hd break :: tl)" + right associative with precedence 47 + for @{'cons $hd $tl}. + +notation "[ list0 x sep ; ]" + non associative with precedence 90 + for ${fold right @'nil rec acc @{'cons $x $acc}}. + +notation "hvbox(l1 break @ l2)" + right associative with precedence 47 + for @{'append $l1 $l2 }. + +interpretation "nil" 'nil = (nil ?). +interpretation "cons" 'cons hd tl = (cons ? hd tl). + +ntheorem nil_cons: + ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ []. +#A;#l;#a;#H;ndestruct; +nqed. + +nlet rec id_list A (l: list A) on l ≝ + match l with + [ nil ⇒ [] + | cons hd tl ⇒ hd :: id_list A tl ]. + +nlet rec append A (l1: list A) l2 on l1 ≝ + match l1 with + [ nil ⇒ l2 + | cons hd tl ⇒ hd :: append A tl l2 ]. + +ndefinition tail ≝ λA:Type[0].λl:list A. + match l with + [ nil ⇒ [] + | cons hd tl ⇒ tl]. + +interpretation "append" 'append l1 l2 = (append ? l1 l2). + +ntheorem append_nil: ∀A:Type.∀l:list A.l @ [] = l. +#A;#l;nelim l;//; +#a;#l1;#IH;nnormalize;//; +nqed. + +ntheorem associative_append: ∀A:Type[0].associative (list A) (append A). +#A;#x;#y;#z;nelim x +##[// +##|#a;#x1;#H;nnormalize;//] +nqed. + +ntheorem cons_append_commute: + ∀A:Type[0].∀l1,l2:list A.∀a:A. + a :: (l1 @ l2) = (a :: l1) @ l2. +//; +nqed. + +nlemma append_cons: ∀A.∀a:A.∀l,l1. l@(a::l1)=(l@[a])@l1. +#A;#a;#l;#l1;nrewrite > (associative_append ????);//; +nqed. + +(*ninductive permutation (A:Type) : list A -> list A -> Prop \def + | refl : \forall l:list A. permutation ? l l + | swap : \forall l:list A. \forall x,y:A. + permutation ? (x :: y :: l) (y :: x :: l) + | trans : \forall l1,l2,l3:list A. + permutation ? l1 l2 -> permut1 ? l2 l3 -> permutation ? l1 l3 +with permut1 : list A -> list A -> Prop \def + | step : \forall l1,l2:list A. \forall x,y:A. + permut1 ? (l1 @ (x :: y :: l2)) (l1 @ (y :: x :: l2)).*) + +(* + +definition x1 \def S O. +definition x2 \def S x1. +definition x3 \def S x2. + +theorem tmp : permutation nat (x1 :: x2 :: x3 :: []) (x1 :: x3 :: x2 :: []). + apply (trans ? (x1 :: x2 :: x3 :: []) (x1 :: x2 :: x3 :: []) ?). + apply refl. + apply (step ? (x1::[]) [] x2 x3). + qed. + +theorem nil_append_nil_both: + \forall A:Type.\forall l1,l2:list A. + l1 @ l2 = [] \to l1 = [] \land l2 = []. + +theorem test_notation: [O; S O; S (S O)] = O :: S O :: S (S O) :: []. +reflexivity. +qed. + +theorem test_append: [O;O;O;O;O;O] = [O;O;O] @ [O;O] @ [O]. +simplify. +reflexivity. +qed. + +*) + +nlet rec nth A l d n on n ≝ + match n with + [ O ⇒ match l with + [ nil ⇒ d + | cons (x : A) _ ⇒ x ] + | S n' ⇒ nth A (tail ? l) d n']. + +nlet rec map A B f l on l ≝ + match l with [ nil ⇒ nil B | cons (x:A) tl ⇒ f x :: map A B f tl ]. + +nlet rec foldr (A,B:Type[0]) (f : A → B → B) (b:B) l on l ≝ + match l with [ nil ⇒ b | cons (a:A) tl ⇒ f a (foldr A B f b tl) ]. + +ndefinition length ≝ λT:Type[0].λl:list T.foldr T nat (λx,c.S c) O l. + +ndefinition filter ≝ + λT:Type[0].λl:list T.λp:T → bool. + foldr T (list T) + (λx,l0.match (p x) with [ true => x::l0 | false => l0]) [] l. + +ndefinition iota : nat → nat → list nat ≝ + λn,m. nat_rect_Type0 (λ_.list ?) (nil ?) (λx,acc.cons ? (n+x) acc) m. + +(* ### induction principle for functions visiting 2 lists in parallel *) +nlemma list_ind2 : + ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop. + length ? l1 = length ? l2 → + (P (nil ?) (nil ?)) → + (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) → + P l1 l2. +#T1;#T2;#l1;#l2;#P;#Hl;#Pnil;#Pcons; +ngeneralize in match Hl; ngeneralize in match l2; +nelim l1 +##[#l2;ncases l2;//; + nnormalize;#t2;#tl2;#H;ndestruct; +##|#t1;#tl1;#IH;#l2;ncases l2 + ##[nnormalize;#H;ndestruct + ##|#t2;#tl2;#H;napply Pcons;napply IH;nnormalize in H;ndestruct;//] +##] +nqed. + +nlemma eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l. +#A;#B;#f;#g;#l;#Efg; +nelim l; nnormalize;//; +nqed. + +nlemma le_length_filter : ∀A,l,p.length A (filter A l p) ≤ length A l. +#A;#l;#p;nelim l;nnormalize +##[// +##|#a;#tl;#IH;ncases (p a);nnormalize; + ##[napply le_S_S;//; + ##|@2;//] +##] +nqed. + +nlemma length_append : ∀A,l,m.length A (l@m) = length A l + length A m. +#A;#l;#m;nelim l; +##[// +##|#H;#tl;#IH;nnormalize;nrewrite < IH;//] +nqed. + +ninductive in_list (A:Type): A → (list A) → Prop ≝ +| in_list_head : ∀ x,l.(in_list A x (x::l)) +| in_list_cons : ∀ x,y,l.(in_list A x l) → (in_list A x (y::l)). + +ndefinition incl : \forall A.(list A) \to (list A) \to Prop \def + \lambda A,l,m.\forall x.in_list A x l \to in_list A x m. + +notation "hvbox(a break ∉ b)" non associative with precedence 45 +for @{ 'notmem $a $b }. + +interpretation "list member" 'mem x l = (in_list ? x l). +interpretation "list not member" 'notmem x l = (Not (in_list ? x l)). +interpretation "list inclusion" 'subseteq l1 l2 = (incl ? l1 l2). + +naxiom not_in_list_nil : \forall A,x.\lnot in_list A x []. +(*intros.unfold.intro.inversion H + [intros;lapply (sym_eq ? ? ? H2);destruct Hletin + |intros;destruct H4] +qed.*) + +naxiom in_list_cons_case : \forall A,x,a,l.in_list A x (a::l) \to + x = a \lor in_list A x l. +(*intros;inversion H;intros + [destruct H2;left;reflexivity + |destruct H4;right;assumption] +qed.*) + +naxiom in_list_tail : \forall l,x,y. + in_list nat x (y::l) \to x \neq y \to in_list nat x l. +(*intros 4;elim (in_list_cons_case ? ? ? ? H) + [elim (H2 H1) + |assumption] +qed.*) + +naxiom in_list_singleton_to_eq : \forall A,x,y.in_list A x [y] \to x = y. +(*intros;elim (in_list_cons_case ? ? ? ? H) + [assumption + |elim (not_in_list_nil ? ? H1)] +qed.*) + +naxiom in_list_to_in_list_append_l: \forall A.\forall x:A. +\forall l1,l2.in_list ? x l1 \to in_list ? x (l1@l2). +(*intros. +elim H;simplify + [apply in_list_head + |apply in_list_cons;assumption + ] +qed.*) + +naxiom in_list_to_in_list_append_r: \forall A.\forall x:A. +\forall l1,l2. in_list ? x l2 \to in_list ? x (l1@l2). +(*intros 3. +elim l1;simplify + [assumption + |apply in_list_cons;apply H;assumption + ] +qed.*) + +naxiom in_list_append_to_or_in_list: \forall A:Type.\forall x:A. +\forall l,l1. in_list ? x (l@l1) \to in_list ? x l \lor in_list ? x l1. +(*intros 3. +elim l + [right.apply H + |simplify in H1.inversion H1;intros; destruct; + [left.apply in_list_head + | elim (H l2) + [left.apply in_list_cons. assumption + |right.assumption + |assumption + ] + ] + ] +qed.*) + +nlet rec mem (A:Type) (eq: A → A → bool) x (l: list A) on l ≝ + match l with + [ nil ⇒ false + | (cons a l') ⇒ + match eq x a with + [ true ⇒ true + | false ⇒ mem A eq x l' + ] + ]. + +naxiom mem_true_to_in_list : + \forall A,equ. + (\forall x,y.equ x y = true \to x = y) \to + \forall x,l.mem A equ x l = true \to in_list A x l. +(* intros 5.elim l + [simplify in H1;destruct H1 + |simplify in H2;apply (bool_elim ? (equ x a)) + [intro;rewrite > (H ? ? H3);apply in_list_head + |intro;rewrite > H3 in H2;simplify in H2; + apply in_list_cons;apply H1;assumption]] +qed.*) + +naxiom in_list_to_mem_true : + \forall A,equ. + (\forall x.equ x x = true) \to + \forall x,l.in_list A x l \to mem A equ x l = true. +(*intros 5.elim l + [elim (not_in_list_nil ? ? H1) + |elim H2 + [simplify;rewrite > H;reflexivity + |simplify;rewrite > H4;apply (bool_elim ? (equ a1 a2));intro;reflexivity]]. +qed.*) + +naxiom in_list_filter_to_p_true : \forall A,l,x,p. +in_list A x (filter A l p) \to p x = true. +(* intros 4;elim l + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; + simplify in H1 + [elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H3;assumption + |apply (H H3)] + |apply (H H1)]] +qed.*) + +naxiom in_list_filter : \forall A,l,p,x.in_list A x (filter A l p) \to in_list A x l. +(*intros 4;elim l + [simplify in H;elim (not_in_list_nil ? ? H) + |simplify in H1;apply (bool_elim ? (p a));intro;rewrite > H2 in H1; + simplify in H1 + [elim (in_list_cons_case ? ? ? ? H1) + [rewrite > H3;apply in_list_head + |apply in_list_cons;apply H;assumption] + |apply in_list_cons;apply H;assumption]] +qed.*) + +naxiom in_list_filter_r : \forall A,l,p,x. + in_list A x l \to p x = true \to in_list A x (filter A l p). +(* intros 4;elim l + [elim (not_in_list_nil ? ? H) + |elim (in_list_cons_case ? ? ? ? H1) + [rewrite < H3;simplify;rewrite > H2;simplify;apply in_list_head + |simplify;apply (bool_elim ? (p a));intro;simplify; + [apply in_list_cons;apply H;assumption + |apply H;assumption]]] +qed.*) + +naxiom incl_A_A: ∀T,A.incl T A A. +(*intros.unfold incl.intros.assumption. +qed.*) + +naxiom incl_append_l : ∀T,A,B.incl T A (A @ B). +(*unfold incl; intros;autobatch. +qed.*) + +naxiom incl_append_r : ∀T,A,B.incl T B (A @ B). +(*unfold incl; intros;autobatch. +qed.*) + +naxiom incl_cons : ∀T,A,B,x.incl T A B → incl T (x::A) (x::B). +(*unfold incl; intros;elim (in_list_cons_case ? ? ? ? H1);autobatch. +qed.*) + diff --git a/helm/software/matita/nlibrary/datatypes/pairs.ma b/helm/software/matita/nlibrary/datatypes/pairs.ma index dfff0c3f8..2165accbb 100644 --- a/helm/software/matita/nlibrary/datatypes/pairs.ma +++ b/helm/software/matita/nlibrary/datatypes/pairs.ma @@ -17,4 +17,15 @@ include "logic/pts.ma". nrecord pair (A,B: Type[0]) : Type[0] ≝ { fst: A; snd: B - }. \ No newline at end of file + }. + +interpretation "Pair construction" 'pair x y = (mk_pair ? ? x y). + +interpretation "Product" 'product x y = (pair x y). + +interpretation "pair pi1" 'pi1 = (fst ? ?). +interpretation "pair pi2" 'pi2 = (snd ? ?). +interpretation "pair pi1" 'pi1a x = (fst ? ? x). +interpretation "pair pi2" 'pi2a x = (snd ? ? x). +interpretation "pair pi1" 'pi1b x y = (fst ? ? x y). +interpretation "pair pi2" 'pi2b x y = (snd ? ? x y). diff --git a/helm/software/matita/nlibrary/datatypes/sums.ma b/helm/software/matita/nlibrary/datatypes/sums.ma new file mode 100644 index 000000000..c5a73b4b5 --- /dev/null +++ b/helm/software/matita/nlibrary/datatypes/sums.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "datatypes/pairs.ma". + +ninductive void : Type[0] ≝. + +ninductive unit : Type[0] ≝ something: unit. + +ninductive Sum (A,B:Type[0]) : Type[0] ≝ +| inl : A → Sum A B +| inr : B → Sum A B. + +interpretation "Disjoint union" 'plus A B = (Sum A B). + +ninductive option (A:Type[0]) : Type[0] ≝ + | None : option A + | Some : A → option A. \ No newline at end of file diff --git a/helm/software/matita/nlibrary/logic/equality.ma b/helm/software/matita/nlibrary/logic/equality.ma index 8ae1bcde4..f1a679c7d 100644 --- a/helm/software/matita/nlibrary/logic/equality.ma +++ b/helm/software/matita/nlibrary/logic/equality.ma @@ -125,4 +125,94 @@ ndefinition EQ: ∀A:Type[0]. equivalence_relation A. | napply refl | #x; #y; #H; nrewrite < H; napply refl | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption] -nqed. \ No newline at end of file +nqed. + +naxiom T1 : Type[0]. +naxiom T2 : T1 → Type[0]. +naxiom t1 : T1. +naxiom t2 : ∀x:T1. T2 x. + +ninductive I2 : ∀r1:T1.T2 r1 → Type[0] ≝ +| i2c1 : ∀x1:T1.∀x2:T2 x1. I2 x1 x2 +| i2c2 : I2 t1 (t2 t1). + +(* nlemma i2d : ∀a,b.∀x,y:I2 a b. + ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b. + ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y. + Type[2]. +#a;#b;#x;#y; +napply ( +match x return (λr1,r2,r. + ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b. + ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with + [ i2c1 x1 x2 ⇒ ? + | i2c2 ⇒ ?] +) +[napply (match y return (λr1,r2,r. + ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2. + ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with + [ i2c1 y1 y2 ⇒ ? + | i2c2 ⇒ ? ]) + [#e1; #e2; #e; + napply (∀P:Type[1]. + (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2. + ∀f: R2 T1 x1 (λz,p.T2 z) x2 + (λz1,p1,z2,p2.eq ? + (i2c1 (R1 ??? z1 ? (R1 ?? (λm,n.m = y1) f1 ? p1)) ?) + (* (R2 ???? (λm1,n1,m2,n2.R1 ?? (λm,n.T2 m) ? ? f1 = y2) f2 ? + p1 ? p2)))*) +(* (R2 ???? (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2) + ? (R1 ?? (λw,q.w = y1) e1 z1 p1) + ? (R2 ???? + (λw1,q1,w2,q2.R1 ?? (λm,n.T2 m) w2 ? q1 = y2) + e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2)) + *) (i2c1 y1 y2)) + ? y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P) + → P); + napply (∀P:Type[1]. + (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2. + ∀f: R2 T1 x1 (λz,p.T2 z) x2 + (λz1,p1,z2,p2.eq (I2 y1 y2) + (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2) + y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) + y2 (R2 T1 x1 (λw,q.w = y1) e1 + (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2)) + (i2c1 y1 y2)) + e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P) + → P); + + +ndefinition i2d : ∀a,b.∀x,y:I2 a b. + ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b. + ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.Type[2] ≝ +λa,b,x,y. +match x return (λr1,r2,r. + ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b. + ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with + [ i2c1 x1 x2 ⇒ + match y return (λr1,r2,r. + ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2. + ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with + [ i2c1 y1 y2 ⇒ λe1,e2,e.∀P:Type[1]. + (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2. + ∀f: R2 T1 x1 (λz,p.T2 z) x2 + (λz1,p1,z2,p2.eq (I2 y1 y2) + (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2) + y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) + y2 (R2 T1 x1 (λw,q.w = y1) e1 + (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2)) + (i2c1 y1 y2)) + e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P) + → P + | i2c2 ⇒ λe1,e2,e.∀P:Type[1].P ] + | i2c2 ⇒ + match y return (λr1,r2,r. + ∀e1: x1 = r1. ∀e2: R1 ?? (λz,p. T2 z) x2 ? e1 = r2. + ∀e : R2 ???? (λz1,p1,z2,p2. I2 z1 z2) i2c2 ? e1 ? e2 = r. Type[2]) with + [ i2c1 _ _ ⇒ λe1,e2,e.∀P:Type[1].P + | i2c2 ⇒ λe1,e2,e.∀P:Type[1]. + (∀f: R2 ???? + (λz1,p1,z2,p2.eq ? i2c2 i2c2) + e ? e1 ? e2 = refl ? i2c2.P) → P ] ]. + +*) \ No newline at end of file diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma index 780dc2b4c..d4a13507c 100644 --- a/helm/software/matita/nlibrary/sets/sets.ma +++ b/helm/software/matita/nlibrary/sets/sets.ma @@ -52,8 +52,8 @@ ndefinition seteq: ∀A. equivalence_relation1 (Ω^A). #A; @ [ napply (λS,S'. S ⊆ S' ∧ S' ⊆ S) | /2/ - | #S; #S'; *; /2/ - | #S; #T; #U; *; #H1; #H2; *; /3/] + | #S; #S'; *; /3/ + | #S; #T; #U; *; #H1; #H2; *; /4/] nqed. include "sets/setoids1.ma". @@ -140,7 +140,7 @@ unification hint 0 ≔ A:setoid, x, S; nlemma subseteq_is_morph: ∀A. unary_morphism1 (ext_powerclass_setoid A) (unary_morphism1_setoid1 (ext_powerclass_setoid A) CPROP). #A; napply (mk_binary_morphism1 … (λS,S':𝛀^A. S ⊆ S')); - #a; #a'; #b; #b'; *; #H1; #H2; *; /4/. + #a; #a'; #b; #b'; *; #H1; #H2; *; /5/. nqed. unification hint 0 ≔ A,a,a' -- 2.39.2