* Almost ready for release 0.99.1.

[helm.git] / matita / matita / lib / basics / logic.ma

diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma
index 1b801a14bf8f339ef9fd20ff57072edd1022d595..1fdd851e09608171a58ba2a0c5f5f072b5444ba7 100644 (file)
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/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.                     
@@ -14,31 +14,47 @@ 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. eq ? x a → Type[2]. P a (refl A a) → P x p.
+ ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl 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.
 
+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 #H #x #p (generalize {match H}) (generalize {match P})
+  cases p; //; qed.
+
+lemma eq_rect_Type1_r:
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[1]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p (generalize {match H}) (generalize {match 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 #H #x #p (generalize {match H}) (generalize {match P})
+  cases p; //; qed.
+
+lemma eq_rect_Type3_r:
+  ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[3]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
+  #A #a #P #H #x #p (generalize {match H}) (generalize {match 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 = 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.
+#A #x #y #Heq @(rewrite_l A x (λz.z=x)) // qed.
 
-theorem rewrite_r: ∀A:Type[1].∀x.∀P:A → Type[1]. P x → ∀y. y = x → P y.
+theorem rewrite_r: ∀A:Type[2].∀x.∀P:A → Type[2]. P x → ∀y. y = x → P y.
 #A #x #P #Hx #y #Heq (cases (sym_eq ? ? ? Heq)); //; qed.
 
 theorem eq_coerc: ∀A,B:Type[0].A→(A=B)→B.
@@ -55,6 +71,10 @@ 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.
 #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. x1=x2 → y1=y2 → z1=z2 → f x1 y1 z1 = 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.
@@ -141,7 +161,7 @@ definition R0 ≝ λT:Type[0].λt:T.t.
   
 definition R1 ≝ eq_rect_Type0.
 
-(* useless stuff
+(* used for lambda-delta *)
 definition R2 :
   ∀T0:Type[0].
   ∀a0:T0.
@@ -216,7 +236,16 @@ definition R4 :
 @(eq_rect_Type0 ????? e3) 
 @(R3 ????????? e0 ? e1 ? e2) 
 @a4 
-qed. *)
+qed.
+
+definition eqProp ≝ λA:Prop.eq A.
 
-(* 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.
+(* Example to avoid indexing and the consequential creation of ill typed
+   terms during paramodulation *)
+example lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
+#A #x #h @(refl ? h: eqProp ? ? ?).
+qed.
+
+theorem streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[3].P (refl ? t) → ∀p.P p.
+ #T #t #P #H #p >(lemmaK T t p) @H
+qed.