From: Claudio Sacerdoti Coen Date: Thu, 30 Nov 2006 21:48:29 +0000 (+0000) Subject: Added a demo for Matita: two slightly different proofs in declarative language X-Git-Tag: 0.4.95@7852~757 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=16bd8ab4cb83990229256fb9aa65c94f90f25c5d;p=helm.git Added a demo for Matita: two slightly different proofs in declarative language that the derivative of x^n is n*x^(n-1). The real numbers, the definition of derivative and some basic properties of derivatives are axiomatized. Two alternative notations are proposed for the derivatives. (The somehow nicer one is currently bugged.) --- diff --git a/matita/library/demo/power_derivative.ma b/matita/library/demo/power_derivative.ma new file mode 100644 index 000000000..ce288b731 --- /dev/null +++ b/matita/library/demo/power_derivative.ma @@ -0,0 +1,315 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/demo/power_derivative". + +include "nat/plus.ma". +include "nat/orders.ma". +include "nat/compare.ma". + +axiom R: Type. +axiom R0: R. +axiom R1: R. +axiom Rplus: R→R→R. +axiom Rmult: R→R→R. + +notation "0" with precedence 89 +for @{ 'zero }. +interpretation "Rzero" 'zero = + (cic:/matita/demo/power_derivative/R0.con). +interpretation "Nzero" 'zero = + (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)). + +notation "1" with precedence 89 +for @{ 'one }. +interpretation "Rone" 'one = + (cic:/matita/demo/power_derivative/R1.con). +interpretation "None" 'one = + (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) + cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)). + +interpretation "Rplus" 'plus x y = + (cic:/matita/demo/power_derivative/Rplus.con x y). +interpretation "Rmult" 'times x y = + (cic:/matita/demo/power_derivative/Rmult.con x y). + +definition Fplus ≝ + λf,g:R→R.λx:R.f x + g x. + +definition Fmult ≝ + λf,g:R→R.λx:R.f x * g x. + +interpretation "Fplus" 'plus x y = + (cic:/matita/demo/power_derivative/Fplus.con x y). +interpretation "Fmult" 'times x y = + (cic:/matita/demo/power_derivative/Fmult.con x y). + +notation "2" with precedence 89 +for @{ 'two }. +interpretation "Rtwo" 'two = + (cic:/matita/demo/power_derivative/Rplus.con + cic:/matita/demo/power_derivative/R1.con + cic:/matita/demo/power_derivative/R1.con). +interpretation "Ntwo" 'two = + (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) + (cic:/matita/nat/nat/nat.ind#xpointer(1/1/2) + (cic:/matita/nat/nat/nat.ind#xpointer(1/1/1)))). + +let rec Rpower (x:R) (n:nat) on n ≝ + match n with + [ O ⇒ 1 + | S n ⇒ x * (Rpower x n) + ]. + +interpretation "Rpower" 'exp x n = + (cic:/matita/demo/power_derivative/Rpower.con x n). + +let rec inj (n:nat) on n : R ≝ + match n with + [ O ⇒ 0 + | S n ⇒ + match n with + [ O ⇒ 1 + | S m ⇒ 1 + inj n + ] + ]. + +coercion cic:/matita/demo/power_derivative/inj.con. + +axiom Rplus_Rzero_x: ∀x:R.0+x=x. +axiom Rplus_comm: symmetric ? Rplus. +axiom Rplus_assoc: associative ? Rplus. +axiom Rmult_Rone_x: ∀x:R.1*x=x. +axiom Rmult_Rzero_x: ∀x:R.0*x=0. +axiom Rmult_assoc: associative ? Rmult. +axiom Rmult_comm: symmetric ? Rmult. +axiom Rmult_Rplus_distr: distributive ? Rmult Rplus. + +alias symbol "times" = "Rmult". +alias symbol "plus" = "natural plus". + +definition monomio ≝ + λn.λx:R.x\sup n. + +definition costante : nat → R → R ≝ + λa:nat.λx:R.inj a. + +coercion cic:/matita/demo/power_derivative/costante.con 1. + +axiom f_eq_extensional: + ∀f,g:R→R.(∀x:R.f x = g x) → f=g. + +lemma Fmult_one_f: ∀f:R→R.1*f=f. + intro; + unfold Fmult; + simplify; + apply f_eq_extensional; + intro; + auto. +qed. + +lemma Fmult_zero_f: ∀f:R→R.0*f=0. + intro; + unfold Fmult; + simplify; + apply f_eq_extensional; + intro; + auto. +qed. + +lemma Fmult_commutative: symmetric ? Fmult. + unfold; + intros; + unfold Fmult; + apply f_eq_extensional; + intros; + auto. +qed. + +lemma Fmult_associative: associative ? Fmult. + unfold; + intros; + unfold Fmult; + unfold Fmult; + apply f_eq_extensional; + intros; + auto. +qed. + +lemma Fmult_Fplus_distr: distributive ? Fmult Fplus. + unfold; + intros; + unfold Fmult; + unfold Fplus; + apply f_eq_extensional; + intros; + simplify; + auto. +qed. + +lemma monomio_product: + ∀n,m.monomio (n+m) = monomio n * monomio m. + intros; + unfold monomio; + unfold Fmult; + simplify; + elim n; + [ simplify; + apply f_eq_extensional; + intro; + auto + | simplify; + apply f_eq_extensional; + intro; + cut (x\sup (n1+m) = x \sup n1 * x \sup m); + [ rewrite > Hcut; + auto + | change in ⊢ (? ? % ?) with ((λx:R.(x)\sup(n1+m)) x); + rewrite > H; + reflexivity + ] + ]. +qed. + +lemma costante_sum: + ∀n,m.costante n + costante m = costante (n+m). + intros; + unfold Fplus; + unfold costante; + apply f_eq_extensional; + intros; + elim n; + [ simplify; + auto + | simplify; + clear x; + clear H; + clear n; + elim n1; + [ simplify; + elim m; + [ simplify; + auto + | simplify; + rewrite < H; + auto + ] + | simplify; + rewrite < H; + clear H; + elim n; + [ simplify; + auto + | simplify; + auto + ] + ] + ]. +qed. + +axiom derivative: (R→R) → R → R. + +notation "hvbox('D'[f])" + non associative with precedence 90 +for @{ 'derivative $f }. + +interpretation "Rderivative" 'derivative f = + (cic:/matita/demo/power_derivative/derivative.con f). + +notation "hvbox('x' \sup n)" + non associative with precedence 60 +for @{ 'monomio $n }. + +notation "hvbox('x')" + non associative with precedence 60 +for @{ 'monomio 1 }. + +interpretation "Rmonomio" 'monomio n = + (cic:/matita/demo/power_derivative/monomio.con n). + +axiom derivative_x0: D[x \sup 0] = 0. +axiom derivative_x1: D[x] = 1. +axiom derivative_mult: ∀f,g:R→R. D[f*g] = D[f]*g + f*D[g]. + +alias symbol "times" = "Fmult". + +theorem derivative_power: ∀n:nat. D[x \sup n] = n*x \sup (pred n). + assume n:nat. + we proceed by induction on n to prove + (D[x \sup n] = n*x \sup (pred n)). + case O. + the thesis becomes (D[x \sup 0] = 0*x \sup (pred 0)). + by _ + done. + case S (m:nat). + by induction hypothesis we know + (D[x \sup m] = m*x \sup (pred m)) (H). + the thesis becomes + (D[x \sup (1+m)] = (1+m)*x \sup m). + we need to prove + (m * (x \sup (1+ pred m)) = m * x \sup m) (Ppred). + by _ we proved (0 < m ∨ 0=m) (cases). + we proceed by induction on cases + to prove (m * (x \sup (1+ pred m)) = m * x \sup m). + case left. + suppose (0 < m) (m_pos). + by (S_pred m m_pos) we proved (m = 1 + pred m) (H1). + by _ + done. + case right. + suppose (0=m) (m_zero). by _ done. + conclude + (D[x \sup (1+m)]) + = (D[x * x \sup m]) by _. + = (D[x] * x \sup m + x * D[x \sup m]) by _. + = (x \sup m + x * (m * x \sup (pred m))) by _. +clear H. + = (x \sup m + m * (x \sup (1 + pred m))) by _. + = (x \sup m + m * x \sup m) by _. + = ((1+m)*x \sup m) by _ (timeout=30) + done. +qed. + +notation "hvbox(\frac 'd' ('d' ident i) break p)" + right associative with precedence 90 +for @{ 'derivative ${default + @{\lambda ${ident i} : $ty. $p)} + @{\lambda ${ident i} . $p}}}. + +interpretation "Rderivative" 'derivative \eta.f = + (cic:/matita/demo/power_derivative/derivative.con f). + +theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n)*x \sup n. + assume n:nat. + we proceed by induction on n to prove + (D[x \sup (1+n)] = (1+n)*x \sup n). + case O. + the thesis becomes (D[x \sup 1] = 1*x \sup 0). + by _ + done. + case S (m:nat). + by induction hypothesis we know + (D[x \sup (1+m)] = (1+m)*x \sup m) (H). + the thesis becomes + (D[x \sup (2+m)] = (2+m)*x \sup (1+m)). + conclude + (D[x \sup (2+m)]) + = (D[x \sup 1 * x \sup (1+m)]) by _. + = (D[x \sup 1] * x \sup (1+m) + x * D[x \sup (1+m)]) by _. + = (x \sup (1+m) + x * (costante (1+m) * x \sup m)) by _. +clear H. + = (x \sup (1+m) + costante (1+m) * x \sup (1+m)) by _. + = (x \sup (1+m) * (costante (2 + m))) by _ + done. +qed.