X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Flogic.ma;h=aeee17a7323f3f4abda175fde73c01229d6a0866;hb=f1ef0a9e283af00cace679efd5775062c2a8f05c;hp=c64f887c6fe0f6b36d90dfebb5a7f2c61897f59e;hpb=df8e8b840c36a1a789ec7bebc47c3cc8aca4f663;p=helm.git diff --git a/weblib/basics/logic.ma b/weblib/basics/logic.ma index c64f887c6..aeee17a73 100644 --- 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) a title="logical and" href="cic:/fakeuri.def(1)"∧/a (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.