manual commit after active hyperlinks

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

diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index adbfd9cab304d0455ac9626ed3203602384b2734..d532c3186fdca7ffd11fdd611183db88b228f89e 100644 (file)
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -12,65 +12,96 @@
 include "basics/relations.ma".
 
 (********** bool **********)
-inductive bool: Type[0] ≝ 
+\ 5img class="anchor" src="icons/tick.png" id="bool"\ 6inductive 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]
+\ 5img class="anchor" src="icons/tick.png" id="not_eq_true_false"\ 6theorem not_eq_true_false : \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+@\ 5a href="cic:/matita/basics/logic/Not.con(0,1,1)"\ 6nmk\ 5/a\ 6 #Heq change with match \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 with [true ⇒ \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6|false ⇒ \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6]
 >Heq // qed.
 
-definition notb : bool → bool ≝
-λ b:bool. match b with [true ⇒ false|false ⇒ true ].
+\ 5img class="anchor" src="icons/tick.png" id="notb"\ 6definition notb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+λ b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. match b with [true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6|false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 ].
 
 interpretation "boolean not" 'not x = (notb x).
 
-theorem notb_elim: ∀ b:bool.∀ P:bool → Prop.
+\ 5img class="anchor" src="icons/tick.png" id="notb_elim"\ 6theorem notb_elim: ∀ b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
 match b with
-[ true ⇒ P false
-| false ⇒ P true] → P (notb b).
+[ true ⇒ P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6
+| false ⇒ P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6] → P (\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b).
 #b #P elim b normalize // qed.
 
-theorem notb_notb: ∀b:bool. notb (notb b) = b.
+\ 5img class="anchor" src="icons/tick.png" id="notb_notb"\ 6theorem notb_notb: ∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 (\ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
 #b elim b // qed.
 
-theorem injective_notb: injective bool bool notb.
+\ 5img class="anchor" src="icons/tick.png" id="injective_notb"\ 6theorem injective_notb: \ 5a href="cic:/matita/basics/relations/injective.def(1)"\ 6injective\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6.
 #b1 #b2 #H // qed.
 
-definition andb : bool → bool → bool ≝
-λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
+\ 5img class="anchor" src="icons/tick.png" id="noteq_to_eqnot"\ 6theorem noteq_to_eqnot: ∀b1,b2. b1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 b2 → b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2.
+* * // #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="eqnot_to_noteq"\ 6theorem eqnot_to_noteq: ∀b1,b2. b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/notb.def(1)"\ 6notb\ 5/a\ 6 b2 → b1 \ 5a title="leibnitz's non-equality" href="cic:/fakeuri.def(1)"\ 6≠\ 5/a\ 6 b2.
+* * normalize // #H @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … \ 5a href="cic:/matita/basics/bool/not_eq_true_false.def(3)"\ 6not_eq_true_false\ 5/a\ 6) //
+qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="andb"\ 6definition andb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+λb1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. match b1 with [ true ⇒ b2 | false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 ].
 
 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).
+\ 5img class="anchor" src="icons/tick.png" id="andb_elim"\ 6theorem andb_elim: ∀ b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. ∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
+match b1 with [ true ⇒ P b2 | false ⇒ P \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6] → P (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2).
 #b1 #b2 #P (elim b1) normalize // qed.
 
-theorem andb_true_l: ∀ b1,b2. (b1 ∧ b2) = true → b1 = true.
+\ 5img class="anchor" src="icons/tick.png" id="andb_true_l"\ 6theorem andb_true_l: ∀ b1,b2. (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 #b1 (cases b1) normalize // qed.
 
-theorem andb_true_r: ∀b1,b2. (b1 ∧ b2) = true → b2 = true.
+\ 5img class="anchor" src="icons/tick.png" id="andb_true_r"\ 6theorem andb_true_r: ∀b1,b2. (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
 #b1 #b2 (cases b1) normalize // (cases b2) // qed.
 
-definition orb : bool → bool → bool ≝
-λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
+\ 5img class="anchor" src="icons/tick.png" id="andb_true"\ 6theorem andb_true: ∀b1,b2. (b1 \ 5a title="boolean and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+/\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6, \ 5a href="cic:/matita/basics/bool/andb_true_r.def(4)"\ 6andb_true_r\ 5/a\ 6, \ 5a href="cic:/matita/basics/bool/andb_true_l.def(4)"\ 6andb_true_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="orb"\ 6definition orb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+λb1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.match b1 with [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | 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).
+\ 5img class="anchor" src="icons/tick.png" id="orb_elim"\ 6theorem orb_elim: ∀ b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. ∀ P:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → Prop.
+match b1 with [ true ⇒ P \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | false ⇒ P b2] → P (\ 5a href="cic:/matita/basics/bool/orb.def(1)"\ 6orb\ 5/a\ 6 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].
-
-theorem bool_to_decidable_eq: 
-  ∀b1,b2:bool. decidable (b1=b2).
-#b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
-
-theorem true_or_false:
-∀b:bool. b = true ∨ b = false.
-#b (cases b) /2/ qed.
-
+\ 5img class="anchor" src="icons/tick.png" id="orb_true_r1"\ 6lemma orb_true_r1: ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. 
+  b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → (b1 \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#b1 #b2 #H >H // qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="orb_true_r2"\ 6lemma orb_true_r2: ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. 
+  b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → (b1 \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6.
+#b1 #b2 #H >H cases b1 // qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="orb_true_l"\ 6lemma orb_true_l: ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. 
+  (b1 \ 5a title="boolean or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b2) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 → (b1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 (b2 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6).
+* normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="xorb"\ 6definition xorb : \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 → \ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6 ≝
+λb1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6.
+ match b1 with
+  [ true ⇒  match b2 with [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 | false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 ]
+  | false ⇒  match b2 with [ true ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 | false ⇒ \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 ]].
+
+notation > "'if' term 46 e 'then' term 46 t 'else' term 46 f" non associative with precedence 46
+(* notation > "£ term 46 e & term 46 t & term 46 f" non associative with precedence 46 *)
+ for @{ 'ite $e $t $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]  }. 
+
+\ 5img class="anchor" src="icons/tick.png" id="bool_to_decidable_eq"\ 6theorem bool_to_decidable_eq: 
+  ∀b1,b2:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (b1\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6b2).
+#b1 #b2 (cases b1) (cases b2) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ %2 /\ 5span class="autotactic"\ 63\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.
+
+\ 5img class="anchor" src="icons/tick.png" id="true_or_false"\ 6theorem true_or_false:
+∀b:\ 5a href="cic:/matita/basics/bool/bool.ind(1,0,0)"\ 6bool\ 5/a\ 6. b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6 \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6 b \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6.
+#b (cases b) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6, \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ qed.