From 87bfe7fa6c7b906646a0094180e69c0b0373ce10 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 26 Nov 2007 12:42:51 +0000 Subject: [PATCH] Notation improved. --- helm/software/matita/dama_didactic/deriv.ma | 20 +-- .../software/matita/dama_didactic/ex_deriv.ma | 115 +++++++++--------- 2 files changed, 66 insertions(+), 69 deletions(-) diff --git a/helm/software/matita/dama_didactic/deriv.ma b/helm/software/matita/dama_didactic/deriv.ma index f4de77580..201471c45 100644 --- a/helm/software/matita/dama_didactic/deriv.ma +++ b/helm/software/matita/dama_didactic/deriv.ma @@ -32,16 +32,16 @@ interpretation "function mult" 'mult x y = interpretation "function compositon" 'compose x y = (cic:/matita/didactic/deriv/fcomp.con x y). -notation "hvbox(a break ⊕ b)" +notation "hvbox(a break + b)" right associative with precedence 45 for @{ 'oplus $a $b }. -interpretation "function plus" 'oplus x y = +interpretation "function plus" 'plus x y = (cic:/matita/didactic/deriv/fplus.con x y). axiom i:R→F. (*mappatura R in F*) coercion cic:/matita/didactic/deriv/i.con. -axiom i_comm_plus: ∀x,y:R. (i (x+y)) = (i x) ⊕ (i y). +axiom i_comm_plus: ∀x,y:R. (i (x+y)) = (i x) + (i y). axiom i_comm_mult: ∀x,y:R. (i (Rmult x y)) = (i x) · (i y). axiom freflex:F. @@ -77,22 +77,22 @@ let rec felev (f:F) (n:nat) on n: F ≝ (* Proprietà *) -axiom fplus_commutative: ∀ f,g:F. f ⊕ g = g ⊕ f. -axiom fplus_associative: ∀ f,g,h:F. f ⊕ (g ⊕ h) = (f ⊕ g) ⊕ h. -axiom fplus_neutral: ∀f:F. (i R0) ⊕ f = f. +axiom fplus_commutative: ∀ f,g:F. f + g = g + f. +axiom fplus_associative: ∀ f,g,h:F. f + (g + h) = (f + g) + h. +axiom fplus_neutral: ∀f:F. (i R0) + f = f. axiom fmult_commutative: ∀ f,g:F. f · g = g · f. axiom fmult_associative: ∀ f,g,h:F. f · (g · h) = (f · g) · h. axiom fmult_neutral: ∀f:F. (i R1) · f = f. axiom fmult_assorb: ∀f:F. (i R0) · f = (i R0). -axiom fdistr: ∀ f,g,h:F. (f ⊕ g) · h = (f · h) ⊕ (g · h). +axiom fdistr: ∀ f,g,h:F. (f + g) · h = (f · h) + (g · h). axiom fcomp_associative: ∀ f,g,h:F. f ∘ (g ∘ h) = (f ∘ g) ∘ h. -axiom fcomp_distr1: ∀ f,g,h:F. (f ⊕ g) ∘ h = (f ∘ h) ⊕ (g ∘ h). +axiom fcomp_distr1: ∀ f,g,h:F. (f + g) ∘ h = (f ∘ h) + (g ∘ h). axiom fcomp_distr2: ∀ f,g,h:F. (f · g) ∘ h = (f ∘ h) · (g ∘ h). -axiom demult: ∀ f,g:F. (f · g) ' = (f ' · g) ⊕ (f · g '). +axiom demult: ∀ f,g:F. (f · g) ' = (f ' · g) + (f · g '). axiom decomp: ∀ f,g:F. (f ∘ g) ' = (f ' ∘ g) · g '. -axiom deplus: ∀ f,g:F. (f ⊕ g) ' = (f ') ⊕ (g '). +axiom deplus: ∀ f,g:F. (f + g) ' = (f ') + (g '). axiom cost_assorb: ∀x:R. ∀f:F. (i x) ∘ f = i x. axiom cost_deriv: ∀x:R. (i x) ' = i R0. diff --git a/helm/software/matita/dama_didactic/ex_deriv.ma b/helm/software/matita/dama_didactic/ex_deriv.ma index 32e1ee8a5..59e881592 100644 --- a/helm/software/matita/dama_didactic/ex_deriv.ma +++ b/helm/software/matita/dama_didactic/ex_deriv.ma @@ -16,18 +16,18 @@ set "baseuri" "cic:/matita/didactic/ex_deriv". include "deriv.ma". -theorem p_plus_p_p: ∀f:F. ∀g:F. (fpari f ∧ fpari g) → fpari (f ⊕ g). +theorem p_plus_p_p: ∀f:F. ∀g:F. (fpari f ∧ fpari g) → fpari (f + g). assume f:F. assume g:F. suppose (fpari f ∧ fpari g) (h). by h we have (fpari f) (H) and (fpari g) (K). - we need to prove (fpari (f ⊕ g)) - or equivalently ((f ⊕ g) = (f ⊕ g) ∘ ρ). + we need to prove (fpari (f + g)) + or equivalently ((f + g) = (f + g) ∘ ρ). conclude - (f ⊕ g) - = (f ⊕ (g ∘ ρ)) by _. - = ((f ∘ ρ) ⊕ (g ∘ ρ)) by _. - = ((f ⊕ g) ∘ ρ) by _ + (f + g) + = (f + (g ∘ ρ)) by _. + = ((f ∘ ρ) + (g ∘ ρ)) by _. + = ((f + g) ∘ ρ) by _ done. qed. @@ -46,23 +46,23 @@ theorem p_mult_p_p: ∀f:F. ∀g:F. (fpari f ∧ fpari g) → fpari (f · g). done. qed. -theorem d_plus_d_d: ∀f:F. ∀g:F. (fdispari f ∧ fdispari g) → fdispari (f ⊕ g). +theorem d_plus_d_d: ∀f:F. ∀g:F. (fdispari f ∧ fdispari g) → fdispari (f + g). assume f:F. assume g:F. suppose (fdispari f ∧ fdispari g) (h). by h we have (fdispari f) (H) and (fdispari g) (K). - we need to prove (fdispari (f ⊕ g)) - or equivalently ((f ⊕ g) = (ρ ∘ ((f ⊕ g) ∘ ρ))). + we need to prove (fdispari (f + g)) + or equivalently ((f + g) = (ρ ∘ ((f + g) ∘ ρ))). conclude - (f ⊕ g) - = (f ⊕ (ρ ∘ (g ∘ ρ))) by _. - = ((ρ ∘ (f ∘ ρ)) ⊕ (ρ ∘ (g ∘ ρ))) by _. - = (((-R1) · (f ∘ ρ)) ⊕ (ρ ∘ (g ∘ ρ))) by _. - = (((i (-R1)) · (f ∘ ρ)) ⊕ ((i (-R1)) · (g ∘ ρ))) by _. - = (((f ∘ ρ) · (i (-R1))) ⊕ ((g ∘ ρ) · (i (-R1)))) by _. - = (((f ∘ ρ) ⊕ (g ∘ ρ)) · (i (-R1))) by _. - = ((i (-R1)) · ((f ⊕ g) ∘ ρ)) by _. - = (ρ ∘ ((f ⊕ g) ∘ ρ)) by _ + (f + g) + = (f + (ρ ∘ (g ∘ ρ))) by _. + = ((ρ ∘ (f ∘ ρ)) + (ρ ∘ (g ∘ ρ))) by _. + = (((-R1) · (f ∘ ρ)) + (ρ ∘ (g ∘ ρ))) by _. + = (((i (-R1)) · (f ∘ ρ)) + ((i (-R1)) · (g ∘ ρ))) by _. + = (((f ∘ ρ) · (i (-R1))) + ((g ∘ ρ) · (i (-R1)))) by _. + = (((f ∘ ρ) + (g ∘ ρ)) · (i (-R1))) by _. + = ((i (-R1)) · ((f + g) ∘ ρ)) by _. + = (ρ ∘ ((f + g) ∘ ρ)) by _ done. qed. @@ -106,12 +106,12 @@ theorem p_mult_d_p: ∀f:F. ∀g:F. (fpari f ∧ fdispari g) → fdispari (f · done. qed. -theorem p_plus_c_p: ∀f:F. ∀x:R. fpari f → fpari (f ⊕ (i x)). +theorem p_plus_c_p: ∀f:F. ∀x:R. fpari f → fpari (f + (i x)). assume f:F. assume x:R. suppose (fpari f) (h). - we need to prove (fpari (f ⊕ (i x))) - or equivalently (f ⊕ (i x) = (f ⊕ (i x)) ∘ ρ). + we need to prove (fpari (f + (i x))) + or equivalently (f + (i x) = (f + (i x)) ∘ ρ). by _ done. qed. @@ -183,54 +183,51 @@ theorem dispari_in_pari: ∀ f:F. fdispari f → fpari f '. done. qed. -(* -alias id "plus" = "cic:/matita/nat/plus/plus.con". +axiom tech1: ∀n,m. F_OF_nat n + F_OF_nat m = F_OF_nat (n + m). + +alias symbol "plus" = "natural plus". +alias num (instance 0) = "natural number". theorem de_prodotto_funzioni: - ∀ n:nat. (id ^ (plus n (S O))) ' = (i (n + (S O))) · (id ^ n). + ∀ n:nat. (id ^ (n + 1)) ' = ((n + 1)) · (id ^ n). assume n:nat. we proceed by induction on n to prove - ((id ^ (plus n (S O))) ' = (i (n + (S O))) · (id ^ n)). + ((id ^ (n + 1)) ' = (i (n + 1)) · (id ^ n)). case O. - we need to prove ((id ^ (plus O (S O))) ' = (i (S O)) · (id ^ O)). + we need to prove ((id ^ (0 + 1)) ' = (i 1) · (id ^ 0)). conclude - ((id ^ (plus O (S O))) ') - = ((id ^ (S O)) ') by _. - = ((id · (id ^ O)) ') by _. - = ((id · (i R1)) ') by _. + ((id ^ (0 + 1)) ') + = ((id ^ 1) ') by _. + = ((id · (id ^ 0)) ') by _. + = ((id · R1) ') by _. = (id ') by _. = (i R1) by _. - = (i R1 · i R1) by _. + = (i R1 · R1) by _. = (i (R0 + R1) · R1) by _. - = ((i (S O)) · (id ^ O)) by _ + = (1 · (id ^ 0)) by _ done. case S (n:nat). by induction hypothesis we know - ((id ^ (plus n (S O))) ' = (i (n + (S O))) · (id ^ n)) (H). + ((id ^ (n + 1)) ' = ((n + 1)) · (id ^ n)) (H). we need to prove - ((id ^ (plus (plus n (S O)) (S O))) ' - = (i (plus (plus n (S O)) (S O))) · (id ^ (plus n (S O)))). + ((id ^ ((n + 1)+1)) ' + = (i ((n + 1)+1)) · (id ^ (n+1))). conclude - ((id ^ ((n + (S O)) + (S O))) ') - = ((id ^ ((n + (S (S O))))) ') by _. - = ((id ^ (S (n + S O))) ') by _. - = ((id · (id ^ (n + (S O)))) ') by _. - = ((id ' · (id ^ (n + (S O)))) ⊕ (id · (id ^ (n + (S O))) ')) by _. - alias symbol "plus" (instance 4) = "natural plus". - = ((R1 · (id ^ (n + (S O)))) ⊕ (id · ((i (n + S O)) · (id ^ n)))) by _. - = ((R1 · (id ^ (n + (S O)))) ⊕ (((i (n + S O)) · id · (id ^ n)))) by _. - alias symbol "plus" (instance 8) = "natural plus". - = ((R1 · (id ^ (n + (S O)))) ⊕ ((i (n + S O)) · (id ^ (n + (S O))))) by _. - = ((i R1 · (id ^ (n + (S O)))) ⊕ ((i (n + S O)) · (id ^ (n + (S O))))) by _. - alias symbol "plus" = "natural plus". - cut (((i R1 · (id ^ (n + (S O)))) ⊕ ((i (n + S O)) · (id ^ (n + (S O))))) = - (((i R1 ⊕ (i (plus n (S O)))) · (id ^ (n + (S O))))));[| by _ done;] - unfold F_OF_nat in Hcut; - rewrite > Hcut; - = (((i R1 ⊕ (i (plus n (S O)))) · (id ^ (n + (S O))))) by _. - = ((i (n + S O + S O)) · (id ^ (n + S O))) by _ + ((id ^ ((n + 1) + 1)) ') + = ((id ^ ((n + (S 1)))) ') by _. + = ((id ^ (S (n + 1))) ') by _. + = ((id · (id ^ (n + 1))) ') by _. + = ((id ' · (id ^ (n + 1))) + (id · (id ^ (n + 1)) ')) by _. + alias symbol "plus" (instance 1) = "function plus". + = ((R1 · (id ^ (n + 1))) + (id · (((n + 1)) · (id ^ n)))) by _. + = ((R1 · (id ^ (n + 1))) + (((n + 1) · id · (id ^ n)))) by _. + = ((R1 · (id ^ (n + 1))) + ((n + 1) · (id ^ (1 + n)))) by _. + = ((R1 · (id ^ (n + 1))) + ((n + 1) · (id ^ (n + 1)))) by _. + alias symbol "plus" (instance 2) = "function plus". + = (((R1 + (n + 1))) · (id ^ (n + 1))) by _. + = ((1 + (n + 1)) · (id ^ (n + 1))) by _; + = ((n + 1 + 1) · (id ^ (n + 1))) by _ done. qed. -*) let rec times (n:nat) (x:R) on n: R ≝ match n with @@ -239,8 +236,8 @@ let rec times (n:nat) (x:R) on n: R ≝ ]. axiom invS: nat→R. -axiom invS1: ∀n:nat. Rmult (invS n) (real_of_nat (n + S O)) = R1. -axiom invS2: invS (S O) + invS (S O) = R1. (*forse*) +axiom invS1: ∀n:nat. Rmult (invS n) (real_of_nat (n + 1)) = R1. +axiom invS2: invS 1 + invS 1 = R1. (*forse*) axiom e:F. axiom deriv_e: e ' = e. @@ -248,5 +245,5 @@ axiom e1: e · (e ∘ ρ) = R1. (* theorem decosh_senh: - (invS (S O) · (e ⊕ (e ∘ ρ)))' = (invS (S O) · (e ⊕ (ρ ∘ (e ∘ ρ)))). -*) \ No newline at end of file + (invS 1 · (e + (e ∘ ρ)))' = (invS 1 · (e + (ρ ∘ (e ∘ ρ)))). +*) -- 2.39.2