X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=weblib%2Fbasics%2Flogic.ma;h=b9dfed28c7d70dc1d39e7ca68fa9b5e533be02de;hb=eb918fc784eacd2094e3986ba321ef47690d9983;hp=34299aff0072b77a9a78c75c23d7ed8e3bccf889;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git
diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index 34299aff0..b9dfed28c 100644
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -1,4 +1,4 @@
-(*
+ (*
||M|| This file is part of HELM, an Hypertextual, Electronic
||A|| Library of Mathematics, developed at the Computer Science
||T|| Department of the University of Bologna, Italy.
@@ -10,54 +10,71 @@
V_______________________________________________________________ *)
include "basics/pts.ma".
-(*include "hints_declaration.ma".*)
+include "hints_declaration.ma".
(* propositional equality *)
-inductive eq (A:Type[1]) (x:A) : A â Prop â
+inductive eq (A:Type[2]) (x:A) : A â Prop â
refl: eq A x x.
-
+
interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
+interpretation "leibniz reflexivity" 'refl = refl.
lemma eq_rect_r:
- âA.âa,x.âp:eq ? x a.âP:
- âx:A. x = a â Type[2]. P a (refl A a) â P x p.
+ âA.âa,x.âp:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.âP: âx:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a â Type[3]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) â P x p.
#A #a #x #p (cases p) // qed.
lemma eq_ind_r :
- âA.âa.âP: âx:A. x = a â Prop. P a (refl A a) â
- âx.âp:eq ? x a.P x p.
- #A #a #P #p #x0 #p0; @(eq_rect_r ? ? ? p0) //; qed.
+ âA.âa.âP: âx:A. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a â Prop. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) â âx.âp:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.P x p.
+ #A #a #P #p #x0 #p0; @(a href="cic:/matita/basics/logic/eq_rect_r.def(1)"eq_rect_r/a ? ? ? p0) //; qed.
+
+lemma eq_rect_Type0_r:
+ âA.âa.âP: âx:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a â Type[0]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) â âx.âp:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
+
+lemma eq_rect_Type1_r:
+ âA.âa.âP: âx:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a â Type[1]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) â âx.âp:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
lemma eq_rect_Type2_r:
- âA.âa.âP: âx:A. eq ? x a â Type[2]. P a (refl A a) â
- âx.âp:eq ? x a.P x p.
- #A #a #P #H #x #p (generalize in match H) (generalize in match P)
+ âA.âa.âP: âx:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a â Type[2]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) â âx.âp:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
+ cases p; //; qed.
+
+lemma eq_rect_Type3_r:
+ âA.âa.âP: âx:A. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a â Type[3]. P a (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A a) â âx.âp:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a ? x a.P x p.
+ #A #a #P #H #x #p lapply H lapply P
cases p; //; qed.
-theorem rewrite_l: âA:Type[1].âx.âP:A â Type[1]. P x â ây. x = y â P y.
+theorem rewrite_l: âA:Type[2].âx.âP:A â Type[2]. P x â ây. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y â P y.
#A #x #P #Hx #y #Heq (cases Heq); //; qed.
-theorem sym_eq: âA.âx,y:A. x = y â y = x.
-#A #x #y #Heq @(rewrite_l A x (λz.z=x)); //; qed.
+theorem sym_eq: âA.âx,y:A. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y â y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x.
+#A #x #y #Heq @(a href="cic:/matita/basics/logic/rewrite_l.def(1)"rewrite_l/a A x (λz.za title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax)) // qed.
-theorem rewrite_r: âA:Type[1].âx.âP:A â Type[1]. P x â ây. y = x â P y.
-#A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
+theorem rewrite_r: âA:Type[2].âx.âP:A â Type[2]. P x â ây. y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x â P y.
+#A #x #P #Hx #y #Heq (cases (a href="cic:/matita/basics/logic/sym_eq.def(2)"sym_eq/a ? ? ? Heq)); //; qed.
-theorem eq_coerc: âA,B:Type[0].Aâ(A=B)âB.
+theorem eq_coerc: âA,B:Type[0].Aâ(Aa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/aB)âB.
#A #B #Ha #Heq (elim Heq); //; qed.
-theorem trans_eq : âA.âx,y,z:A. x = y â y = z â x = z.
+theorem trans_eq : âA.âx,y,z:A. x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a y â y a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a z â x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a z.
#A #x #y #z #H1 #H2 >H1; //; qed.
-theorem eq_f: âA,B.âf:AâB.âx,y:A. x=y â f x = f y.
+theorem eq_f: âA,B.âf:AâB.âx,y:A. xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay â f x a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f y.
#A #B #f #x #y #H >H; //; qed.
(* deleterio per auto? *)
theorem eq_f2: âA,B,C.âf:AâBâC.
-âx1,x2:A.ây1,y2:B. x1=x2 â y1=y2 â f x1 y1 = f x2 y2.
+âx1,x2:A.ây1,y2:B. x1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax2 â y1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay2 â f x1 y1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x2 y2.
#A #B #C #f #x1 #x2 #y1 #y2 #E1 #E2 >E1; >E2; //; qed.
+lemma eq_f3: âA,B,C,D.âf:AâBâC->D.
+âx1,x2:A.ây1,y2:B. âz1,z2:C. x1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax2 â y1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ay2 â z1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/az2 â f x1 y1 z1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a f x2 y2 z2.
+#A #B #C #D #f #x1 #x2 #y1 #y2 #z1 #z2 #E1 #E2 #E3 >E1; >E2; >E3 //; qed.
+
(* hint to genereric equality
definition eq_equality: equality â
mk_equality eq refl rewrite_l rewrite_r.
@@ -80,27 +97,26 @@ inductive False: Prop â .
λA. A â False. *)
inductive Not (A:Prop): Prop â
-nmk: (A â False) â Not A.
-
+nmk: (A â a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a) â Not A.
interpretation "logical not" 'not x = (Not x).
-theorem absurd : âA:Prop. A â ¬A â False.
-#A #H #Hn (elim Hn); /2/; qed.
+theorem absurd : âA:Prop. A â a title="logical not" href="cic:/fakeuri.def(1)"¬/aA â a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a.
+#A #H #Hn (elim Hn); /span class="autotactic"2span class="autotrace" trace /span/span/; qed.
(*
ntheorem absurd : â A,C:Prop. A â ¬A â C.
#A; #C; #H; #Hn; nelim (Hn H).
nqed. *)
-theorem not_to_not : âA,B:Prop. (A â B) â ¬B â¬A.
-/4/; qed.
+theorem not_to_not : âA,B:Prop. (A â B) â a title="logical not" href="cic:/fakeuri.def(1)"¬/aB âa title="logical not" href="cic:/fakeuri.def(1)"¬/aA.
+/span class="autotactic"4span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a, a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/; qed.
(* inequality *)
interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
-theorem sym_not_eq: âA.âx,y:A. x â y â y â x.
-/3/; qed.
+theorem sym_not_eq: âA.âx,y:A. x a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"â /a y â y a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"â /a x.
+/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a, a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a/span/span/; qed.
(* and *)
inductive And (A,B:Prop) : Prop â
@@ -108,10 +124,10 @@ inductive And (A,B:Prop) : Prop â
interpretation "logical and" 'and x y = (And x y).
-theorem proj1: âA,B:Prop. A ⧠B â A.
+theorem proj1: âA,B:Prop. A a title="logical and" href="cic:/fakeuri.def(1)"â§/a B â A.
#A #B #AB (elim AB) //; qed.
-theorem proj2: â A,B:Prop. A ⧠B â B.
+theorem proj2: â A,B:Prop. A a title="logical and" href="cic:/fakeuri.def(1)"â§/a B â B.
#A #B #AB (elim AB) //; qed.
(* or *)
@@ -122,7 +138,7 @@ inductive Or (A,B:Prop) : Prop â
interpretation "logical or" 'or x y = (Or x y).
definition decidable : Prop â Prop â
-λ A:Prop. A ⨠¬ A.
+λ A:Prop. A a title="logical or" href="cic:/fakeuri.def(1)"â¨/a a title="logical not" href="cic:/fakeuri.def(1)"¬/a A.
(* exists *)
inductive ex (A:Type[0]) (P:A â Prop) : Prop â
@@ -135,92 +151,122 @@ inductive ex2 (A:Type[0]) (P,Q:A âProp) : Prop â
(* iff *)
definition iff :=
- λ A,B. (A â B) ⧠(B â A).
+ λ A,B. (A â B) a title="logical and" href="cic:/fakeuri.def(1)"â§/a (B â A).
-interpretation "iff" 'iff a b = (iff a b).
+interpretation "iff" 'iff a b = (iff a b).
+
+lemma iff_sym: âA,B. A a title="iff" href="cic:/fakeuri.def(1)"â/a B â B a title="iff" href="cic:/fakeuri.def(1)"â/a A.
+#A #B * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed.
+
+lemma iff_trans:âA,B,C. A a title="iff" href="cic:/fakeuri.def(1)"â/a B â B a title="iff" href="cic:/fakeuri.def(1)"â/a C â A a title="iff" href="cic:/fakeuri.def(1)"â/a C.
+#A #B #C * #H1 #H2 * #H3 #H4 % /span class="autotactic"3span class="autotrace" trace /span/span/ qed.
+
+lemma iff_not: âA,B. A a title="iff" href="cic:/fakeuri.def(1)"â/a B â a title="logical not" href="cic:/fakeuri.def(1)"¬/aA a title="iff" href="cic:/fakeuri.def(1)"â/a a title="logical not" href="cic:/fakeuri.def(1)"¬/aB.
+#A #B * #H1 #H2 % /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a/span/span/ qed.
+
+lemma iff_and_l: âA,B,C. A a title="iff" href="cic:/fakeuri.def(1)"â/a B â C a title="logical and" href="cic:/fakeuri.def(1)"â§/a A a title="iff" href="cic:/fakeuri.def(1)"â/a C a title="logical and" href="cic:/fakeuri.def(1)"â§/a B.
+#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed.
+
+lemma iff_and_r: âA,B,C. A a title="iff" href="cic:/fakeuri.def(1)"â/a B â A a title="logical and" href="cic:/fakeuri.def(1)"â§/a C a title="iff" href="cic:/fakeuri.def(1)"â/a B a title="logical and" href="cic:/fakeuri.def(1)"â§/a C.
+#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a/span/span/ qed.
+
+lemma iff_or_l: âA,B,C. A a title="iff" href="cic:/fakeuri.def(1)"â/a B â C a title="logical or" href="cic:/fakeuri.def(1)"â¨/a A a title="iff" href="cic:/fakeuri.def(1)"â/a C a title="logical or" href="cic:/fakeuri.def(1)"â¨/a B.
+#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.
+
+lemma iff_or_r: âA,B,C. A a title="iff" href="cic:/fakeuri.def(1)"â/a B â A a title="logical or" href="cic:/fakeuri.def(1)"â¨/a C a title="iff" href="cic:/fakeuri.def(1)"â/a B a title="logical or" href="cic:/fakeuri.def(1)"â¨/a C.
+#A #B #C * #H1 #H2 % * /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.
(* cose per destruct: da rivedere *)
definition R0 â λT:Type[0].λt:T.t.
-definition R1 â eq_rect_Type0.
+definition R1 â a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a.
-(* useless stuff *)
+(* used for lambda-delta *)
definition R2 :
âT0:Type[0].
âa0:T0.
- âT1:âx0:T0. a0=x0 â Type[0].
- âa1:T1 a0 (refl ? a0).
- âT2:âx0:T0. âp0:a0=x0. âx1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 â Type[0].
- âa2:T2 a0 (refl ? a0) a1 (refl ? a1).
+ âT1:âx0:T0. a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0 â Type[0].
+ âa1:T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0).
+ âT2:âx0:T0. âp0:a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0. âx1:T1 x0 p0. a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? p0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x1 â Type[0].
+ âa2:T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a1).
âb0:T0.
- âe0:a0 = b0.
+ âe0:a0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b0.
âb1: T1 b0 e0.
- âe1:R1 ?? T1 a1 ? e0 = b1.
+ âe1:a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? e0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b1.
T2 b0 e0 b1 e1.
#T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1
-@(eq_rect_Type0 ????? e1)
-@(R1 ?? ? ?? e0)
+@(a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a ????? e1)
+@(a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? ? ?? e0)
@a2
qed.
definition R3 :
âT0:Type[0].
âa0:T0.
- âT1:âx0:T0. a0=x0 â Type[0].
- âa1:T1 a0 (refl ? a0).
- âT2:âx0:T0. âp0:a0=x0. âx1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 â Type[0].
- âa2:T2 a0 (refl ? a0) a1 (refl ? a1).
- âT3:âx0:T0. âp0:a0=x0. âx1:T1 x0 p0.âp1:R1 ?? T1 a1 ? p0 = x1.
- âx2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 â Type[0].
- âa3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
+ âT1:âx0:T0. a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0 â Type[0].
+ âa1:T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0).
+ âT2:âx0:T0. âp0:a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0. âx1:T1 x0 p0. a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? p0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x1 â Type[0].
+ âa2:T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a1).
+ âT3:âx0:T0. âp0:a0a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax0. âx1:T1 x0 p0.âp1:a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? p0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x1.
+ âx2:T2 x0 p0 x1 p1.a href="cic:/matita/basics/logic/R2.def(3)"R2/a ???? T2 a2 x0 p0 ? p1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a x2 â Type[0].
+ âa3:T3 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a1) a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? a2).
âb0:T0.
- âe0:a0 = b0.
+ âe0:a0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b0.
âb1: T1 b0 e0.
- âe1:R1 ?? T1 a1 ? e0 = b1.
+ âe1:a href="cic:/matita/basics/logic/R1.def(2)"R1/a ?? T1 a1 ? e0 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b1.
âb2: T2 b0 e0 b1 e1.
- âe2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
+ âe2:a href="cic:/matita/basics/logic/R2.def(3)"R2/a ???? T2 a2 b0 e0 ? e1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b2.
T3 b0 e0 b1 e1 b2 e2.
#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2
-@(eq_rect_Type0 ????? e2)
-@(R2 ?? ? ???? e0 ? e1)
+@(a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a ????? e2)
+@(a href="cic:/matita/basics/logic/R2.def(3)"R2/a ?? ? ???? e0 ? e1)
@a3
qed.
definition R4 :
âT0:Type[0].
âa0:T0.
- âT1:âx0:T0. eq T0 a0 x0 â Type[0].
- âa1:T1 a0 (refl T0 a0).
- âT2:âx0:T0. âp0:eq (T0 â¦) a0 x0. âx1:T1 x0 p0.eq (T1 â¦) (R1 T0 a0 T1 a1 x0 p0) x1 â Type[0].
- âa2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
- âT3:âx0:T0. âp0:eq (T0 â¦) a0 x0. âx1:T1 x0 p0.âp1:eq (T1 â¦) (R1 T0 a0 T1 a1 x0 p0) x1.
- âx2:T2 x0 p0 x1 p1.eq (T2 â¦) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 â Type[0].
- âa3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
- a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
- âT4:âx0:T0. âp0:eq (T0 â¦) a0 x0. âx1:T1 x0 p0.âp1:eq (T1 â¦) (R1 T0 a0 T1 a1 x0 p0) x1.
- âx2:T2 x0 p0 x1 p1.âp2:eq (T2 â¦) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
- âx3:T3 x0 p0 x1 p1 x2 p2.âp3:eq (T3 â¦) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
+ âT1:âx0:T0. a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a T0 a0 x0 â Type[0].
+ âa1:T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0).
+ âT2:âx0:T0. âp0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 â¦) a0 x0. âx1:T1 x0 p0.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 â¦) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 x0 p0) x1 â Type[0].
+ âa2:T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1).
+ âT3:âx0:T0. âp0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 â¦) a0 x0. âx1:T1 x0 p0.âp1:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 â¦) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 x0 p0) x1.
+ âx2:T2 x0 p0 x1 p1.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T2 â¦) (a href="cic:/matita/basics/logic/R2.def(3)"R2/a T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 â Type[0].
+ âa3:T3 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)
+ a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)) a2).
+ âT4:âx0:T0. âp0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 â¦) a0 x0. âx1:T1 x0 p0.âp1:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 â¦) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 x0 p0) x1.
+ âx2:T2 x0 p0 x1 p1.âp2:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T2 â¦) (a href="cic:/matita/basics/logic/R2.def(3)"R2/a T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
+ âx3:T3 x0 p0 x1 p1 x2 p2.âp3:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T3 â¦) (a href="cic:/matita/basics/logic/R3.def(4)"R3/a T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
Type[0].
- âa4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
- a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
- a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
- a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
+ âa4:T4 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)
+ a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)) a2)
+ a3 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T3 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)
+ a2 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T2 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0) a1 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a (T1 a0 (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a T0 a0)) a1)) a2))
a3).
âb0:T0.
- âe0:eq (T0 â¦) a0 b0.
+ âe0:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T0 â¦) a0 b0.
âb1: T1 b0 e0.
- âe1:eq (T1 â¦) (R1 T0 a0 T1 a1 b0 e0) b1.
+ âe1:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T1 â¦) (a href="cic:/matita/basics/logic/R1.def(2)"R1/a T0 a0 T1 a1 b0 e0) b1.
âb2: T2 b0 e0 b1 e1.
- âe2:eq (T2 â¦) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
+ âe2:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T2 â¦) (a href="cic:/matita/basics/logic/R2.def(3)"R2/a T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
âb3: T3 b0 e0 b1 e1 b2 e2.
- âe3:eq (T3 â¦) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
+ âe3:a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a (T3 â¦) (a href="cic:/matita/basics/logic/R3.def(4)"R3/a T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
T4 b0 e0 b1 e1 b2 e2 b3 e3.
#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #T4 #a4 #b0 #e0 #b1 #e1 #b2 #e2 #b3 #e3
-@(eq_rect_Type0 ????? e3)
-@(R3 ????????? e0 ? e1 ? e2)
+@(a href="cic:/matita/basics/logic/eq_rect_Type0.fix(0,5,1)"eq_rect_Type0/a ????? e3)
+@(a href="cic:/matita/basics/logic/R3.def(4)"R3/a ????????? e0 ? e1 ? e2)
@a4
qed.
-(* TODO concrete definition by means of proof irrelevance *)
-axiom streicherK : âT:Type[1].ât:T.âP:t = t â Type[2].P (refl ? t) â âp.P p.
\ No newline at end of file
+definition eqProp â λA:Prop.a href="cic:/matita/basics/logic/eq.ind(1,0,2)"eq/a A.
+
+(* Example to avoid indexing and the consequential creation of ill typed
+ terms during paramodulation *)
+example lemmaK : âA.âx:A.âh:xa title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax. a href="cic:/matita/basics/logic/eqProp.def(1)"eqProp/a ? h (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a A x).
+#A #x #h @(a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? h: a href="cic:/matita/basics/logic/eqProp.def(1)"eqProp/a ? ? ?).
+qed.
+
+theorem streicherK : âT:Type[2].ât:T.âP:t a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a t â Type[3].P (a href="cic:/matita/basics/logic/eq.con(0,1,2)"refl/a ? t) â âp.P p.
+ #T #t #P #H #p >(a href="cic:/matita/basics/logic/lemmaK.def(2)"lemmaK/a T t p) @H
+qed.
\ No newline at end of file