update in standard library

[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 d1dbfad775aaebc0d1388255fb32890675c9ac49..4b90f75181300bdaced20673e08e5d6420f4fbc1 100644 (file)
--- a/matita/matita/lib/basics/logic.ma
+++ b/matita/matita/lib/basics/logic.ma
@@ -30,22 +30,22 @@ lemma eq_ind_r :
 
 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 in match H) (generalize in match 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 (generalize in match H) (generalize in match 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.
 
 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 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[2].∀x.∀P:A → Type[2]. P x → ∀y. x = y → P y.
@@ -147,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 *) 
 
@@ -242,10 +269,10 @@ definition eqProp ≝ λA:Prop.eq A.
 
 (* 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).
+lemma lemmaK : ∀A.∀x:A.∀h:x=x. eqProp ? h (refl A x).
 #A #x #h @(refl ? h: eqProp ? ? ?).
-qed.
+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.
+qed-.