X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Fbasics%2Fbool.ma;h=7762657aec90514366049386a6453b8f275ec1e8;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=adbfd9cab304d0455ac9626ed3203602384b2734;hpb=8f08fac33a366b2267b35af1a50ad3a9df8dbb88;p=helm.git

diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index adbfd9cab..7762657ae 100644
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -12,65 +12,97 @@
 include "basics/relations.ma".
 
 (********** bool **********)
-inductive bool: Type[0] ≝ 
+img class="anchor" src="icons/tick.png" id="bool"inductive bool: Type[0] ≝ 
   | true : bool
   | false : bool.
 
-(* destruct does not work *)
-theorem not_eq_true_false : true ≠ false.
-@nmk #Heq change with match true with [true ⇒ False|false ⇒ True]
+img class="anchor" src="icons/tick.png" id="not_eq_true_false"theorem not_eq_true_false : a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
+@a href="cic:/matita/basics/logic/Not.con(0,1,1)"nmk/a #Heq change with match a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a with [true ⇒ a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a|false ⇒ a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a]
 >Heq // qed.
 
-definition notb : bool → bool ≝
-λ b:bool. match b with [true ⇒ false|false ⇒ true ].
+img class="anchor" src="icons/tick.png" id="notb"definition notb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+λ b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. match b with [true ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a|false ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a ].
 
 interpretation "boolean not" 'not x = (notb x).
 
-theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
+img class="anchor" src="icons/tick.png" id="notb_elim"theorem notb_elim: ∀ b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
 match b with
-[ true ⇒ P false
-| false ⇒ P true] → P (notb b).
+[ true ⇒ P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a
+| false ⇒ P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a] → P (a href="cic:/matita/basics/bool/notb.def(1)"notb/a b).
 #b #P elim b normalize // qed.
 
-theorem notb_notb: ∀b:bool. notb (notb b) = b.
+img class="anchor" src="icons/tick.png" id="notb_notb"theorem notb_notb: ∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. a href="cic:/matita/basics/bool/notb.def(1)"notb/a (a href="cic:/matita/basics/bool/notb.def(1)"notb/a b) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a b.
 #b elim b // qed.
 
-theorem injective_notb: injective bool bool notb.
+img class="anchor" src="icons/tick.png" id="injective_notb"theorem injective_notb: a href="cic:/matita/basics/relations/injective.def(1)"injective/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a a href="cic:/matita/basics/bool/notb.def(1)"notb/a.
 #b1 #b2 #H // qed.
 
-definition andb : bool → bool → bool ≝
-λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
+img class="anchor" src="icons/tick.png" id="noteq_to_eqnot"theorem noteq_to_eqnot: ∀b1,b2. b1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a b2 → b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/notb.def(1)"notb/a b2.
+* * // #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/
+qed.
+
+img class="anchor" src="icons/tick.png" id="eqnot_to_noteq"theorem eqnot_to_noteq: ∀b1,b2. b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/notb.def(1)"notb/a b2 → b1 a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"≠/a b2.
+* * normalize // #H @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … a href="cic:/matita/basics/bool/not_eq_true_false.def(3)"not_eq_true_false/a) //
+qed.
+
+img class="anchor" src="icons/tick.png" id="andb"definition andb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+λb1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. match b1 with [ true ⇒ b2 | false ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ].
 
 interpretation "boolean and" 'and x y = (andb x y).
 
-theorem andb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
-match b1 with [ true ⇒ P b2 | false ⇒ P false] → P (b1 ∧ b2).
+img class="anchor" src="icons/tick.png" id="andb_elim"theorem andb_elim: ∀ b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. ∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
+match b1 with [ true ⇒ P b2 | false ⇒ P a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a] → P (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2).
 #b1 #b2 #P (elim b1) normalize // qed.
 
-theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
+img class="anchor" src="icons/tick.png" id="true_to_andb_true"theorem true_to_andb_true: ∀b1,b2. b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#b1 cases b1 normalize //
+qed.
+
+img class="anchor" src="icons/tick.png" id="andb_true_l"theorem andb_true_l: ∀ b1,b2. (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #b1 (cases b1) normalize // qed.
 
-theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
+img class="anchor" src="icons/tick.png" id="andb_true_r"theorem andb_true_r: ∀b1,b2. (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
 #b1 #b2 (cases b1) normalize // (cases b2) // qed.
 
-definition orb : bool → bool → bool ≝
-λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
+img class="anchor" src="icons/tick.png" id="andb_true"theorem andb_true: ∀b1,b2. (b1 a title="boolean and" href="cic:/fakeuri.def(1)"∧/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+/span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/logic/And.con(0,1,2)"conj/a, a href="cic:/matita/basics/bool/andb_true_r.def(4)"andb_true_r/a, a href="cic:/matita/basics/bool/andb_true_l.def(4)"andb_true_l/a/span/span/ qed.
+
+img class="anchor" src="icons/tick.png" id="orb"definition orb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+λb1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.match b1 with [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | false ⇒ b2].
  
 interpretation "boolean or" 'or x y = (orb x y).
 
-theorem orb_elim: ∀ b1,b2:bool. ∀ P:bool → Prop.
-match b1 with [ true ⇒ P true | false ⇒ P b2] → P (orb b1 b2).
+img class="anchor" src="icons/tick.png" id="orb_elim"theorem orb_elim: ∀ b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. ∀ P:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → Prop.
+match b1 with [ true ⇒ P a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | false ⇒ P b2] → P (a href="cic:/matita/basics/bool/orb.def(1)"orb/a 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].
+img class="anchor" src="icons/tick.png" id="orb_true_r1"lemma orb_true_r1: ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. 
+  b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → (b1 a title="boolean or" href="cic:/fakeuri.def(1)"∨/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#b1 #b2 #H >H // qed.
+
+img class="anchor" src="icons/tick.png" id="orb_true_r2"lemma orb_true_r2: ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. 
+  b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → (b1 a title="boolean or" href="cic:/fakeuri.def(1)"∨/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a.
+#b1 #b2 #H >H cases b1 // qed.
+
+img class="anchor" src="icons/tick.png" id="orb_true_l"lemma orb_true_l: ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. 
+  (b1 a title="boolean or" href="cic:/fakeuri.def(1)"∨/a b2) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a → (b1 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a) a title="logical or" href="cic:/fakeuri.def(1)"∨/a (b2 a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a).
+* normalize /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.
 
-theorem bool_to_decidable_eq: 
-  ∀b1,b2:bool. decidable (b1=b2).
-#b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
+img class="anchor" src="icons/tick.png" id="xorb"definition xorb : a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a → a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a ≝
+λb1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a.
+ match b1 with
+  [ true ⇒  match b2 with [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a | false ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a ]
+  | false ⇒  match b2 with [ true ⇒ a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a | false ⇒ a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a ]].
 
-theorem true_or_false:
-∀b:bool. b = true ∨ b = false.
-#b (cases b) /2/ qed.
+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]  }.
 
+img class="anchor" src="icons/tick.png" id="bool_to_decidable_eq"theorem bool_to_decidable_eq: 
+  ∀b1,b2:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (b1a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ab2).
+#b1 #b2 (cases b1) (cases b2) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ %2 /span class="autotactic"3span class="autotrace" trace a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"eqnot_to_noteq/a/span/span/ qed.
 
+img class="anchor" src="icons/tick.png" id="true_or_false"theorem true_or_false:
+∀b:a href="cic:/matita/basics/bool/bool.ind(1,0,0)"bool/a. b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,1,0)"true/a a title="logical or" href="cic:/fakeuri.def(1)"∨/a b a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/basics/bool/bool.con(0,2,0)"false/a.
+#b (cases b) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/Or.con(0,1,2)"or_introl/a, a href="cic:/matita/basics/logic/Or.con(0,2,2)"or_intror/a/span/span/ qed.
\ No newline at end of file