From: matitaweb Date: Wed, 22 Feb 2012 12:31:42 +0000 (+0000) Subject: Integrations X-Git-Tag: make_still_working~1943 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f1ef0a9e283af00cace679efd5775062c2a8f05c;p=helm.git Integrations --- diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma index adbfd9cab..6bc18e055 100644 --- a/weblib/basics/bool.ma +++ b/weblib/basics/bool.ma @@ -38,6 +38,14 @@ theorem notb_notb: ∀b:bool. notb (notb b) = b. theorem injective_notb: injective bool bool notb. #b1 #b2 #H // qed. +theorem noteq_to_eqnot: ∀b1,b2. b1 ≠ b2 → b1 = notb b2. +* * // #H @False_ind /2/ +qed. + +theorem eqnot_to_noteq: ∀b1,b2. b1 = notb b2 → b1 ≠ b2. +* * normalize // #H @(not_to_not … not_eq_true_false) // +qed. + definition andb : bool → bool → bool ≝ λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ]. @@ -53,6 +61,9 @@ theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true. theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true. #b1 #b2 (cases b1) normalize // (cases b2) // qed. +theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true. +/3/ qed. + definition orb : bool → bool → bool ≝ λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2]. @@ -62,8 +73,28 @@ theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop. match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2). #b1 #b2 #P (elim b1) normalize // qed. -definition if_then_else: ∀A:Type[0]. bool → A → A → A ≝ -λA.λb.λ P,Q:A. match b with [ true ⇒ P | false ⇒ Q]. +lemma orb_true_r1: ∀b1,b2:bool. + b1 = true → (b1 ∨ b2) = true. +#b1 #b2 #H >H // qed. + +lemma orb_true_r2: ∀b1,b2:bool. + b2 = true → (b1 ∨ b2) = true. +#b1 #b2 #H >H cases b1 // qed. + +lemma orb_true_l: ∀b1,b2:bool. + (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true). +* normalize /2/ qed. + +definition xorb : bool → bool → bool ≝ +λb1,b2:bool. + match b1 with + [ true ⇒ match b2 with [ true ⇒ false | false ⇒ true ] + | false ⇒ match b2 with [ true ⇒ true | false ⇒ false ]]. + +notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46 + for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f] }. +notation < "hvbox('if' \nbsp term 46 e \nbsp break 'then' \nbsp term 46 t \nbsp break 'else' \nbsp term 49 f \nbsp)" non associative with precedence 46 + for @{ match $e with [ true ⇒ $t | false ⇒ $f] }. theorem bool_to_decidable_eq: ∀b1,b2:bool. decidable (b1=b2). 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.