Integrations

[helm.git] / weblib / basics / logic.ma

diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma
index 5e97f9b5c1bdd4b27da7613edad60fa8c644b917..aeee17a7323f3f4abda175fde73c01229d6a0866 100644 (file)
--- a/weblib/basics/logic.ma
+++ b/weblib/basics/logic.ma
@@ -137,8 +137,28 @@ inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝
 definition iff :=
  λ A,B. (A → B) \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 (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 *) 
 
 definition R0 ≝ λT:Type[0].λt:T.t.
@@ -223,5 +243,4 @@ definition R4 :
 qed.
 
 (* TODO concrete definition by means of proof irrelevance *)
-axiom streicherK : ∀T:Type[1].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[2].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
-
+axiom streicherK : ∀T:Type[1].∀t:T.∀P:t \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 t → Type[2].P (\ 5a href="cic:/matita/basics/logic/eq.con(0,1,2)"\ 6refl\ 5/a\ 6 ? t) → ∀p.P p.
\ No newline at end of file