commit by user utente

diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma
index 2260506329463e418b25706942c942bd3cf1c481..a592b1377dfc9815c0d4f706193bab46e1218a4f 100644 (file)
--- a/weblib/arithmetics/nat.ma
+++ b/weblib/arithmetics/nat.ma
@@ -687,14 +687,14 @@ theorem monotonic_lt_times_r:
   ∀c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → \ 5a href="cic:/matita/basics/relations/monotonic.def(1)"\ 6monotonic\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"\ 6lt\ 5/a\ 6 (λt.(c\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6t)).
 #c #posc #n #m #ltnm
 (elim ltnm) normalize
-  [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"\ 6monotonic_lt_plus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ 
+  [/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(5)"\ 6monotonic_lt_plus_l\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
   |#a #_ #lt1 @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 … lt1) //
   ]
 qed.
 
 theorem monotonic_lt_times_l: 
   ∀c:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6. \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → \ 5a href="cic:/matita/basics/relations/monotonic.def(1)"\ 6monotonic\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/lt.def(1)"\ 6lt\ 5/a\ 6 (λt.(t\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6c)).
-/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"\ 6monotonic_lt_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+/\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(9)"\ 6monotonic_lt_times_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
 theorem lt_to_le_to_lt_times: 
@@ -702,7 +702,7 @@ theorem lt_to_le_to_lt_times:
 #n #m #p #q #ltnm #lepq #posq
 @(\ 5a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"\ 6le_to_lt_to_lt\ 5/a\ 6 ? (n\ 5a title="natural times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6q))
   [@\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"\ 6monotonic_le_times_r\ 5/a\ 6 //
-  |@\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(11)"\ 6monotonic_lt_times_l\ 5/a\ 6 //
+  |@\ 5a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(10)"\ 6monotonic_lt_times_l\ 5/a\ 6 //
   ]
 qed.
 
@@ -911,7 +911,7 @@ qed.
 
 theorem le_minus_to_plus: ∀n,m,p. n\ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6m \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p → n\ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 p\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6m.
 #n #m #p #lep @\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6
-  [|@\ 5a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"\ 6le_plus_minus_m_m\ 5/a\ 6 | @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"\ 6monotonic_le_plus_l\ 5/a\ 6 // ]
+  [|@\ 5a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"\ 6le_plus_minus_m_m\ 5/a\ 6 | @\ 5a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"\ 6monotonic_le_plus_l\ 5/a\ 6 // ]
 qed.
 
 theorem le_minus_to_plus_r: ∀a,b,c. c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b → a \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 c → a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 b.
@@ -927,7 +927,7 @@ qed.
 
 theorem lt_minus_to_plus: ∀a,b,c. a \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 b \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b.
 #a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 
-@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 …H)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"\ 6le_plus_to_minus_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"\ 6lt_to_not_le\ 5/a\ 6 …H)) /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"\ 6le_plus_to_minus_r\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
 qed.
 
 theorem lt_minus_to_plus_r: ∀a,b,c. a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 c → a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 c \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 b.
@@ -940,7 +940,7 @@ theorem lt_plus_to_minus: ∀n,m,p. m \ 5a title="natural 'less or equal to'" href
 qed.
 
 theorem lt_plus_to_minus_r: ∀a,b,c. a \ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 b \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c → a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 c \ 5a title="natural minus" href="cic:/fakeuri.def(1)"\ 6-\ 5/a\ 6 b.
-#a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"\ 6le_plus_to_minus_r\ 5/a\ 6 //
+#a #b #c #H @\ 5a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"\ 6le_plus_to_minus_r\ 5/a\ 6 //
 qed. 
 
 theorem monotonic_le_minus_r: 

diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma
index 6bc18e055f2131d16bb1e7ccc758fbcd65892a79..a32d67a0a6a8ecfb2157748a853b1517258951a4 100644 (file)
--- a/weblib/basics/bool.ma
+++ b/weblib/basics/bool.ma
@@ -17,91 +17,97 @@ inductive bool: Type[0] ≝
   | false : bool.
 
 (* destruct does not work *)
-theorem not_eq_true_false : true ≠ false.
-@nmk #Heq change with match true with [true ⇒ False|false ⇒ True]
+theorem 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 ].
+definition 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.
+theorem 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.
+theorem 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.
+theorem 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.
 
-theorem noteq_to_eqnot: ∀b1,b2. b1 ≠ b2 → b1 = notb b2.
-* * // #H @False_ind /2/
+theorem 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.
 
-theorem eqnot_to_noteq: ∀b1,b2. b1 = notb b2 → b1 ≠ b2.
-* * normalize // #H @(not_to_not … not_eq_true_false) //
+theorem 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.
 
-definition andb : bool → bool → bool ≝
-λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ].
+definition 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).
+theorem 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.
+theorem 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.
+theorem 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.
 
-theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true.
-/3/ qed.
+theorem 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.
 
-definition orb : bool → bool → bool ≝
-λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2].
+definition 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).
+theorem 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.
 
-lemma orb_true_r1: ∀b1,b2:bool. 
-  b1 = true → (b1 ∨ b2) = true.
+lemma 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.
 
-lemma orb_true_r2: ∀b1,b2:bool. 
-  b2 = true → (b1 ∨ b2) = true.
+lemma 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.
 
-lemma orb_true_l: ∀b1,b2:bool. 
-  (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true).
-* normalize /2/ qed.
+lemma 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.
 
-definition xorb : bool → bool → bool ≝
-λb1,b2:bool.
+definition 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 ⇒ false | false ⇒ true ]
-  | false ⇒  match b2 with [ true ⇒ true | false ⇒ false ]].
+  [ 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
- for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
+(* 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]  }.
+ for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }. 
 
-theorem bool_to_decidable_eq: 
-  ∀b1,b2:bool. decidable (b1=b2).
-#b1 #b2 (cases b1) (cases b2) /2/ %2 /3/ qed.
+definition ite ≝ λA:Type[0].λe.λt,f:A.match e with [ true ⇒ t | false ⇒ f ].
 
-theorem true_or_false:
-∀b:bool. b = true ∨ b = false.
-#b (cases b) /2/ qed.
+interpretation "if then else" 'ite e t f = (ite ? e t f).
+
+(* axiom foo : ∀b.\ 5a title="if then else" href="cic:/fakeuri.def(1)"\ 6£\ 5/a\ 6 b &amp; \ 5a href="cic:/matita/basics/logic/True.ind(1,0,0)"\ 6True\ 5/a\ 6 &amp; \ 5a href="cic:/matita/basics/logic/False.ind(1,0,0)"\ 6False\ 5/a\ 6. *)
+axiom foo : ∀b. if b then True else False.
 
+(*theorem 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.
 
+theorem 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.*)
\ No newline at end of file

diff --git a/weblib/ricciott/prova.ma b/weblib/ricciott/prova.ma
new file mode 100644 (file)
index 0000000..cd95fd0
--- /dev/null
+++ b/weblib/ricciott/prova.ma
@@ -0,0 +1,27 @@
+include "basics/pts.ma".
+
+axiom R : Type[0].
+axiom V : Type[0].
+
+axiom f : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+
+axiom rplus : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+axiom rtimes : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+
+axiom vplus : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6.
+axiom stimes : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 → \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6.
+
+interpretation "real plus" 'plus x y = (rplus x y).
+interpretation "real times" 'times x y = (rtimes x y).
+
+interpretation "vector plus" 'plus x y = (vplus x y).
+interpretation "scalar product on vectors" 'times x y = (stimes x y).
+
+axiom a : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6. axiom b : \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+axiom x : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6. axiom y : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6. axiom z : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6.
+
+include "basics/logic.ma".
+
+axiom fa : \ 5a href="cic:/matita/ricciott/prova/V.dec"\ 6V\ 5/a\ 6 -> \ 5a href="cic:/matita/ricciott/prova/R.dec"\ 6R\ 5/a\ 6.
+
+lemma pippo : \ 5a href="cic:/matita/ricciott/prova/f.dec"\ 6f\ 5/a\ 6 (\ 5a href="cic:/matita/ricciott/prova/a.dec"\ 6a\ 5/a\ 6\ 5a title="scalar product on vectors" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a href="cic:/matita/ricciott/prova/x.dec"\ 6x\ 5/a\ 6 \ 5a title="vector plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/b.dec"\ 6b\ 5/a\ 6\ 5a title="scalar product on vectors" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6\ 5a href="cic:/matita/ricciott/prova/y.dec"\ 6y\ 5/a\ 6 \ 5a title="vector plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/z.dec"\ 6z\ 5/a\ 6) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/a.dec"\ 6a\ 5/a\ 6\ 5a title="real times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/ricciott/prova/f.dec"\ 6f\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/x.dec"\ 6x\ 5/a\ 6) \ 5a title="real plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/b.dec"\ 6b\ 5/a\ 6\ 5a title="real times" href="cic:/fakeuri.def(1)"\ 6*\ 5/a\ 6(\ 5a href="cic:/matita/ricciott/prova/fa.dec"\ 6fa\ 5/a\ 6 \ 5a href="cic:/matita/ricciott/prova/y.dec"\ 6y\ 5/a\ 6) + z.
\ No newline at end of file