From 2225846a2ee76026bef7c3e8eacc42e86c3ae6a2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 5 Dec 2011 08:56:30 +0000 Subject: [PATCH] More properties of iff --- matita/matita/lib/basics/logic.ma | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/matita/matita/lib/basics/logic.ma b/matita/matita/lib/basics/logic.ma index c80fa31f5..8f981d469 100644 --- a/matita/matita/lib/basics/logic.ma +++ b/matita/matita/lib/basics/logic.ma @@ -153,7 +153,28 @@ inductive ex2 (A:Type[0]) (P,Q:A →Prop) : Prop ≝ 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 *) -- 2.39.2