X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Fbasics%2Flogic.ma;h=4b90f75181300bdaced20673e08e5d6420f4fbc1;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=43bbcbc4b2b9cf601cb0cefdd3fbd9c2c671f4f4;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index 43bbcbc4b..4b90f7518 100644 --- 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 lapply H lapply 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 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 #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. +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 lapply H lapply P + cases p; //; qed. + +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. @@ -127,13 +147,40 @@ inductive ex (A:Type[0]) (P:A → Prop) : Prop ≝ interpretation "exists" 'exists x = (ex ? x). inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝ - ex_intro2: ∀ x:A. P x → Q x → ex2 A P Q. + ex2_intro: ∀ x:A. P x → Q x → ex2 A P Q. + +interpretation "exists on two predicates" 'exists2 x1 x2 = (ex2 ? x1 x2). + +lemma ex2_commute: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0. +#A0 #P0 #P1 * /2 width=3/ +qed-. (* iff *) definition iff := λ A,B. (A → B) ∧ (B → A). -interpretation "iff" 'iff a b = (iff a b). +interpretation "iff" 'iff a b = (iff a b). + +lemma iff_sym: ∀A,B. A ↔ B → B ↔ A. +#A #B * /3/ qed. + +lemma iff_trans:∀A,B,C. A ↔ B → B ↔ C → A ↔ C. +#A #B #C * #H1 #H2 * #H3 #H4 % /3/ qed. + +lemma iff_not: ∀A,B. A ↔ B → ¬A ↔ ¬B. +#A #B * #H1 #H2 % /3/ qed. + +lemma iff_and_l: ∀A,B,C. A ↔ B → C ∧ A ↔ C ∧ B. +#A #B #C * #H1 #H2 % * /3/ qed. + +lemma iff_and_r: ∀A,B,C. A ↔ B → A ∧ C ↔ B ∧ C. +#A #B #C * #H1 #H2 % * /3/ qed. + +lemma iff_or_l: ∀A,B,C. A ↔ B → C ∨ A ↔ C ∨ B. +#A #B #C * #H1 #H2 % * /3/ qed. + +lemma iff_or_r: ∀A,B,C. A ↔ B → A ∨ C ↔ B ∨ C. +#A #B #C * #H1 #H2 % * /3/ qed. (* cose per destruct: da rivedere *) @@ -141,7 +188,7 @@ definition R0 ≝ λT:Type[0].λt:T.t. definition R1 ≝ eq_rect_Type0. -(* +(* used for lambda-delta *) definition R2 : ∀T0:Type[0]. ∀a0:T0. @@ -154,13 +201,13 @@ definition R2 : ∀b1: T1 b0 e0. ∀e1:R1 ?? T1 a1 ? e0 = b1. T2 b0 e0 b1 e1. -#T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1; -napply (eq_rect_Type0 ????? e1); -napply (R1 ?? ? ?? e0); -napply a2; -nqed. +#T0 #a0 #T1 #a1 #T2 #a2 #b0 #e0 #b1 #e1 +@(eq_rect_Type0 ????? e1) +@(R1 ?? ? ?? e0) +@a2 +qed. -ndefinition R3 : +definition R3 : ∀T0:Type[0]. ∀a0:T0. ∀T1:∀x0:T0. a0=x0 → Type[0]. @@ -177,13 +224,13 @@ ndefinition R3 : ∀b2: T2 b0 e0 b1 e1. ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2. T3 b0 e0 b1 e1 b2 e2. -#T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2; -napply (eq_rect_Type0 ????? e2); -napply (R2 ?? ? ???? e0 ? e1); -napply a3; -nqed. +#T0 #a0 #T1 #a1 #T2 #a2 #T3 #a3 #b0 #e0 #b1 #e1 #b2 #e2 +@(eq_rect_Type0 ????? e2) +@(R2 ?? ? ???? e0 ? e1) +@a3 +qed. -ndefinition R4 : +definition R4 : ∀T0:Type[0]. ∀a0:T0. ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0]. @@ -212,10 +259,20 @@ ndefinition R4 : ∀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. 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; -napply (eq_rect_Type0 ????? e3); -napply (R3 ????????? e0 ? e1 ? e2); -napply a4; -nqed. - -naxiom streicherK : ∀T:Type[2].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p. *) +#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) +@a4 +qed. + +definition eqProp ≝ λA:Prop.eq A. + +(* Example to avoid indexing and the consequential creation of ill typed + terms during paramodulation *) +lemma 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-.