From 8095279ddfb0e36b417115f94c60622caf4bfdab Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 6 Jul 2012 12:03:50 +0000 Subject: [PATCH] commit by user utente --- weblib/arithmetics/nat.ma | 12 ++--- weblib/basics/bool.ma | 94 +++++++++++++++++++++------------------ weblib/ricciott/prova.ma | 27 +++++++++++ 3 files changed, 83 insertions(+), 50 deletions(-) create mode 100644 weblib/ricciott/prova.ma diff --git a/weblib/arithmetics/nat.ma b/weblib/arithmetics/nat.ma index 226050632..a592b1377 100644 --- a/weblib/arithmetics/nat.ma +++ b/weblib/arithmetics/nat.ma @@ -687,14 +687,14 @@ theorem monotonic_lt_times_r: ∀c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a (λt.(ca title="natural times" href="cic:/fakeuri.def(1)"*/at)). #c #posc #n #m #ltnm (elim ltnm) normalize - [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(9)"monotonic_lt_plus_l/a/span/span/ + [/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_plus_l.def(5)"monotonic_lt_plus_l/a/span/span/ |#a #_ #lt1 @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a … lt1) // ] qed. theorem monotonic_lt_times_l: ∀c:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a. a href="cic:/matita/arithmetics/nat/nat.con(0,1,0)"O/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a href="cic:/matita/basics/relations/monotonic.def(1)"monotonic/a a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a a href="cic:/matita/arithmetics/nat/lt.def(1)"lt/a (λt.(ta title="natural times" href="cic:/fakeuri.def(1)"*/ac)). -/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(10)"monotonic_lt_times_r/a/span/span/ +/span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/monotonic_lt_times_r.def(9)"monotonic_lt_times_r/a/span/span/ 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 @(a href="cic:/matita/arithmetics/nat/le_to_lt_to_lt.def(4)"le_to_lt_to_lt/a ? (na title="natural times" href="cic:/fakeuri.def(1)"*/aq)) [@a href="cic:/matita/arithmetics/nat/monotonic_le_times_r.def(8)"monotonic_le_times_r/a // - |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(11)"monotonic_lt_times_l/a // + |@a href="cic:/matita/arithmetics/nat/monotonic_lt_times_l.def(10)"monotonic_lt_times_l/a // ] qed. @@ -911,7 +911,7 @@ qed. theorem le_minus_to_plus: ∀n,m,p. na title="natural minus" href="cic:/fakeuri.def(1)"-/am a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a p → na title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a pa title="natural plus" href="cic:/fakeuri.def(1)"+/am. #n #m #p #lep @a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a - [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(9)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ] + [|@a href="cic:/matita/arithmetics/nat/le_plus_minus_m_m.def(6)"le_plus_minus_m_m/a | @a href="cic:/matita/arithmetics/nat/monotonic_le_plus_l.def(6)"monotonic_le_plus_l/a // ] qed. theorem le_minus_to_plus_r: ∀a,b,c. c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b → a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a b. @@ -927,7 +927,7 @@ qed. theorem lt_minus_to_plus: ∀a,b,c. a a title="natural minus" href="cic:/fakeuri.def(1)"-/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural plus" href="cic:/fakeuri.def(1)"+/a b. #a #b #c #H @a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"not_le_to_lt/a -@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a …H)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"le_plus_to_minus_r/a/span/span/ +@(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … (a href="cic:/matita/arithmetics/nat/lt_to_not_le.def(7)"lt_to_not_le/a …H)) /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"le_plus_to_minus_r/a/span/span/ qed. theorem lt_minus_to_plus_r: ∀a,b,c. a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b a title="natural minus" href="cic:/fakeuri.def(1)"-/a c → a a title="natural plus" href="cic:/fakeuri.def(1)"+/a c a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a b. @@ -940,7 +940,7 @@ theorem lt_plus_to_minus: ∀n,m,p. m a title="natural 'less or equal to'" href qed. theorem lt_plus_to_minus_r: ∀a,b,c. a a title="natural plus" href="cic:/fakeuri.def(1)"+/a b a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c → a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a c a title="natural minus" href="cic:/fakeuri.def(1)"-/a b. -#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(10)"le_plus_to_minus_r/a // +#a #b #c #H @a href="cic:/matita/arithmetics/nat/le_plus_to_minus_r.def(7)"le_plus_to_minus_r/a // qed. theorem monotonic_le_minus_r: diff --git a/weblib/basics/bool.ma b/weblib/basics/bool.ma index 6bc18e055..a32d67a0a 100644 --- 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 : 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 ]. +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. +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. +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. +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. -theorem noteq_to_eqnot: ∀b1,b2. b1 ≠ b2 → b1 = notb b2. -* * // #H @False_ind /2/ +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. -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 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. -definition andb : bool → bool → bool ≝ -λb1,b2:bool. match b1 with [ true ⇒ b2 | false ⇒ false ]. +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). +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. +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. +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. -theorem andb_true: ∀b1,b2. (b1 ∧ b2) = true → b1 = true ∧ b2 = true. -/3/ qed. +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. -definition orb : bool → bool → bool ≝ -λb1,b2:bool.match b1 with [ true ⇒ true | false ⇒ b2]. +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). +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. -lemma orb_true_r1: ∀b1,b2:bool. - b1 = true → (b1 ∨ b2) = true. +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. -lemma orb_true_r2: ∀b1,b2:bool. - b2 = true → (b1 ∨ b2) = true. +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. -lemma orb_true_l: ∀b1,b2:bool. - (b1 ∨ b2) = true → (b1 = true) ∨ (b2 = true). -* normalize /2/ qed. +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. -definition xorb : bool → bool → bool ≝ -λb1,b2:bool. +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 ⇒ false | false ⇒ true ] - | false ⇒ match b2 with [ true ⇒ true | false ⇒ false ]]. + [ 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 ]]. 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.a title="if then else" href="cic:/fakeuri.def(1)"£/a b & a href="cic:/matita/basics/logic/True.ind(1,0,0)"True/a & a href="cic:/matita/basics/logic/False.ind(1,0,0)"False/a. *) +axiom foo : ∀b. if b then True else False. +(*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. +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 diff --git a/weblib/ricciott/prova.ma b/weblib/ricciott/prova.ma new file mode 100644 index 000000000..cd95fd0a0 --- /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 : a href="cic:/matita/ricciott/prova/V.dec"V/a → a href="cic:/matita/ricciott/prova/R.dec"R/a. + +axiom rplus : a href="cic:/matita/ricciott/prova/R.dec"R/a → a href="cic:/matita/ricciott/prova/R.dec"R/a → a href="cic:/matita/ricciott/prova/R.dec"R/a. +axiom rtimes : a href="cic:/matita/ricciott/prova/R.dec"R/a → a href="cic:/matita/ricciott/prova/R.dec"R/a → a href="cic:/matita/ricciott/prova/R.dec"R/a. + +axiom vplus : a href="cic:/matita/ricciott/prova/V.dec"V/a → a href="cic:/matita/ricciott/prova/V.dec"V/a → a href="cic:/matita/ricciott/prova/V.dec"V/a. +axiom stimes : a href="cic:/matita/ricciott/prova/R.dec"R/a → a href="cic:/matita/ricciott/prova/V.dec"V/a → a href="cic:/matita/ricciott/prova/V.dec"V/a. + +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 : a href="cic:/matita/ricciott/prova/R.dec"R/a. axiom b : a href="cic:/matita/ricciott/prova/R.dec"R/a. +axiom x : a href="cic:/matita/ricciott/prova/V.dec"V/a. axiom y : a href="cic:/matita/ricciott/prova/V.dec"V/a. axiom z : a href="cic:/matita/ricciott/prova/V.dec"V/a. + +include "basics/logic.ma". + +axiom fa : a href="cic:/matita/ricciott/prova/V.dec"V/a -> a href="cic:/matita/ricciott/prova/R.dec"R/a. + +lemma pippo : a href="cic:/matita/ricciott/prova/f.dec"f/a (a href="cic:/matita/ricciott/prova/a.dec"a/aa title="scalar product on vectors" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/ricciott/prova/x.dec"x/a a title="vector plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/ricciott/prova/b.dec"b/aa title="scalar product on vectors" href="cic:/fakeuri.def(1)"*/aa href="cic:/matita/ricciott/prova/y.dec"y/a a title="vector plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/ricciott/prova/z.dec"z/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/ricciott/prova/a.dec"a/aa title="real times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/ricciott/prova/f.dec"f/a a href="cic:/matita/ricciott/prova/x.dec"x/a) a title="real plus" href="cic:/fakeuri.def(1)"+/a a href="cic:/matita/ricciott/prova/b.dec"b/aa title="real times" href="cic:/fakeuri.def(1)"*/a(a href="cic:/matita/ricciott/prova/fa.dec"fa/a a href="cic:/matita/ricciott/prova/y.dec"y/a) + z. \ No newline at end of file -- 2.39.2