--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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<m
+ | neg m ⇒ False ]
+ | neg n ⇒
+ match y with
+ [ OZ ⇒ True
+ | pos m ⇒ True
+ | neg m ⇒ m<n ]].
+
+interpretation "integer 'less than'" 'lt x y = (Zlt x y).
+interpretation "integer 'not less than'" 'nless x y = (Not (Zlt x y)).
+
+ntheorem irreflexive_Zlt: irreflexive Z Zlt.
+#x;ncases x
+##[//
+##|##*:#n;napply (not_le_Sn_n n) (* XXX: auto?? *)]
+nqed.
+
+(* 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.
+
+(* 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.
+
+(* variant trans_Zlt: transitive Z Zlt
+\def transitive_Zlt.
+theorem irrefl_Zlt: irreflexive Z Zlt
+\def irreflexive_Zlt.*)
+
+ntheorem Zlt_neg_neg_to_lt:
+ ∀n,m:nat. neg n < neg m → m < n.
+//;
+nqed.
+
+ntheorem lt_to_Zlt_neg_neg: ∀n,m:nat.m < n → neg n < neg m.
+//;
+nqed.
+
+ntheorem Zlt_pos_pos_to_lt:
+ ∀n,m:nat. pos n < pos m → n < m.
+//;
+nqed.
+
+ntheorem lt_to_Zlt_pos_pos: ∀n,m:nat.n < m → pos n < pos m.
+//;
+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;ncases n;nnormalize;
+ ##[napply not_le_Sn_O (* XXX: auto? *)
+ ##|#m;napply le_S_S_to_le (* XXX: auto? *)]
+ ##]
+##]
+nqed.
+
+(*** COMPARE ***)
+
+(* boolean equality *)
+ndefinition eqZb : Z → Z → bool ≝
+λx,y:Z.
+ 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]].
+
+ntheorem 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;
+ ##[#H;napply not_eq_OZ_pos;//;
+ ##|#m;napply eqb_elim;
+ ##[//
+ ##|#H;#H2;napply H;ndestruct;//]
+ ##|#m;napply not_eq_pos_neg]
+##|#n;ncases y
+ ##[#H;napply not_eq_OZ_neg;//;
+ ##|#m;#H;ndestruct
+ ##|#m;napply eqb_elim;
+ ##[//
+ ##|#H;#H2;napply H;ndestruct;//]
+ ##]
+##]
+nqed.
+
+ntheorem 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
+(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.
+
+ndefinition Z_compare : Z → Z → compare ≝
+λx,y:Z.
+ match x with
+ [ OZ ⇒
+ match y with
+ [ OZ ⇒ EQ
+ | pos m ⇒ LT
+ | neg m ⇒ GT ]
+ | pos n ⇒
+ match y with
+ [ OZ ⇒ GT
+ | pos m ⇒ nat_compare n m
+ | neg m ⇒ GT]
+ | neg n ⇒
+ match y with
+ [ OZ ⇒ LT
+ | pos m ⇒ LT
+ | neg m ⇒ nat_compare m n ]].
+
+ntheorem 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 (nat_compare m n) with
+ [ LT ⇒ m < n
+ | EQ ⇒ m = n
+ | GT ⇒ n < m ] →
+ match (nat_compare m n) with
+ [ LT ⇒ S m ≤ n
+ | EQ ⇒ pos m = pos n
+ | GT ⇒ S n ≤ m])
+ ##[ncases (nat_compare m n);//
+ ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
+ ##]
+##|nelim y
+ ##[#n;//
+ ##|nnormalize;//
+ ##|nnormalize;#n;#m;
+ ncut (match (nat_compare n m) with
+ [ LT ⇒ n < m
+ | EQ ⇒ n = m
+ | GT ⇒ m < n] →
+ match (nat_compare n m) with
+ [ LT ⇒ S n ≤ m
+ | EQ ⇒ neg m = neg n
+ | GT ⇒ S m ≤ n])
+ ##[ncases (nat_compare n m);//
+ ##|#Hcut;napply Hcut;napply nat_compare_to_Prop]
+ ##]
+##]
+nqed.
+
+ndefinition Zplus : Z → Z → Z ≝
+ λx,y. match x with
+ [ OZ ⇒ y
+ | pos m ⇒
+ match y with
+ [ OZ ⇒ x
+ | pos n ⇒ (pos (pred ((S m)+(S n))))
+ | neg n ⇒
+ match nat_compare m n with
+ [ LT ⇒ (neg (pred (n-m)))
+ | EQ ⇒ OZ
+ | GT ⇒ (pos (pred (m-n)))] ]
+ | neg m ⇒
+ match y with
+ [ OZ ⇒ x
+ | pos n ⇒
+ match nat_compare m n with
+ [ LT ⇒ (pos (pred (n-m)))
+ | EQ ⇒ OZ
+ | GT ⇒ (neg (pred (m-n)))]
+ | neg n ⇒ (neg (pred ((S m)+(S n))))] ].
+
+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;//
+ ##|//]
+nqed.
+
+ntheorem Zplus_z_OZ: ∀z:Z. z+OZ = z.
+#z;ncases z;//;
+nqed.
+
+(* theorem symmetric_Zplus: symmetric Z Zplus. *)
+
+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 > (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
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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.*)
+
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).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
| 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
#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".
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'
projects / helm.git / commitdiff