From: Claudio Sacerdoti Coen Date: Wed, 21 Nov 2007 16:16:58 +0000 (+0000) Subject: Very incomplete example of simple calculus exercises in Matita. X-Git-Tag: make_still_working~5798 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fd4d7813792de2cd5999d444c14f7cd72e2f3ce9;p=helm.git Very incomplete example of simple calculus exercises in Matita. --- diff --git a/helm/software/matita/dama_didactic/bottom.ma b/helm/software/matita/dama_didactic/bottom.ma new file mode 100644 index 000000000..bed8ec6b1 --- /dev/null +++ b/helm/software/matita/dama_didactic/bottom.ma @@ -0,0 +1,117 @@ +(**************************************************************************) +(* ___ *) +(* ||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/test/decl". + +include "nat/times.ma". +include "nat/orders.ma". + +inductive L (T:Type):Type:= + bottom: L T + |j: T → L T. + +inductive eq (T:Type) : L T → L T → Prop := + eq_refl:∀x:T. eq T (j ? x) (j ? x). + +notation "hvbox(a break ≡ b)" + non associative with precedence 45 +for @{ 'equiv $a $b }. + +interpretation "uguaglianza parziale" 'equiv x y = + (cic:/matita/test/decl/eq.ind#xpointer(1/1) _ x y). + +coercion cic:/matita/test/decl/L.ind#xpointer(1/1/2). + +lemma sim: ∀T:Type. ∀x,y:T. (j ? x) ≡ (j ? y) → (j ? y) ≡ (j ? x). + intros. + inversion H. + intros. + apply eq_refl. +qed. + +lemma trans: ∀T:Type. ∀x,y,z:T. + (j ? x) ≡ (j ? y) → (j ? y) ≡ (j ? z) → (j ? x) ≡ (j ? z). + intros. + inversion H1. + intros. + rewrite > H2 in H. + assumption. +qed. + +axiom R:Type. +axiom R0:R. +axiom R1:R. +axiom Rplus: L R→L R→L R. +axiom Rmult: L R→L R→L R.(* +axiom Rdiv: L R→L R→L R.*) +axiom Rinv: L R→L R. +axiom Relev: L R→L R→L R. +axiom Rle: L R→L R→Prop. +axiom Rge: L R→L R→Prop. + +interpretation "real plus" 'plus x y = + (cic:/matita/test/decl/Rplus.con x y). + +interpretation "real leq" 'leq x y = + (cic:/matita/test/decl/Rle.con x y). + +interpretation "real geq" 'geq x y = + (cic:/matita/test/decl/Rge.con x y). + +let rec elev (x:L R) (n:nat) on n: L R ≝ + match n with + [O ⇒ match x with [bottom ⇒ bottom ? | j y ⇒ (j ? R1)] + | S n ⇒ Rmult x (elev x n) + ]. + +let rec real_of_nat (n:nat) : L R ≝ + match n with + [ O ⇒ (j ? R0) + | S n ⇒ real_of_nat n + (j ? R1) + ]. + +coercion cic:/matita/test/decl/real_of_nat.con. + +axiom Rplus_commutative: ∀x,y:R. (j ? x) + (j ? y) ≡ (j ? y) + (j ? x). +axiom R0_neutral: ∀x:R. (j ? x) + (j ? R0) ≡ (j ? x). +axiom Rmult_commutative: ∀x,y:R. Rmult (j ? x) (j ? y) ≡ Rmult (j ? y) (j ? x). +axiom R1_neutral: ∀x:R. Rmult (j ? x) (j ? R1) ≡ (j ? x). + +axiom Rinv_ok: + ∀x:R. ¬((j ? x) ≡ (j ? R0)) → Rmult (Rinv (j ? x)) (j ? x) ≡ (j ? R1). +definition is_defined := + λ T:Type. λ x:L T. ∃y:T. x = (j ? y). +axiom Rinv_ok2: ∀x:L R. ¬(x = bottom ?) → ¬(x ≡ (j ? R0)) → is_defined ? (Rinv x). + +definition Rdiv := + λ x,y:L R. Rmult x (Rinv y). + +(* +lemma pippo: ∀x:R. ¬((j ? x) ≡ (j ? R0)) → Rdiv (j ? R1) (j ? x) ≡ Rinv (j ? x). + intros. + unfold Rdiv. + elim (Rinv_ok2 ? ? H). + rewrite > H1. + rewrite > Rmult_commutative. + apply R1_neutral. +*) + +axiom Rdiv_le: ∀x,y:R. (j ? R1) ≤ (j ? y) → Rdiv (j ? x) (j ? y) ≤ (j ? x). +axiom R2_1: (j ? R1) ≤ S (S O). + + +axiom Rdiv_pos: ∀ x,y:R. + (j ? R0) ≤ (j ? x) → (j ? R1) ≤ (j ? y) → (j ? R0) ≤ Rdiv (j ? x) (j ? y). +axiom Rle_R0_R1: (j ? R0) ≤ (j ? R1). +axiom div: ∀x:R. (j ? x) = Rdiv (j ? x) (S (S O)) → (j ? x) = O. \ No newline at end of file diff --git a/helm/software/matita/dama_didactic/deriv.ma b/helm/software/matita/dama_didactic/deriv.ma new file mode 100644 index 000000000..f4de77580 --- /dev/null +++ b/helm/software/matita/dama_didactic/deriv.ma @@ -0,0 +1,112 @@ +(**************************************************************************) +(* ___ *) +(* ||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/didactic/deriv". + +include "reals.ma". + +axiom F:Type.(*F=funzioni regolari*) +axiom fplus:F→F→F. +axiom fmult:F→F→F. +axiom fcomp:F→F→F. + +axiom De: F→F. (*funzione derivata*) +notation "a '" + non associative with precedence 80 +for @{ 'deriv $a }. +interpretation "function derivative" 'deriv x = + (cic:/matita/didactic/deriv/De.con x). +interpretation "function mult" 'mult x y = + (cic:/matita/didactic/deriv/fmult.con x y). +interpretation "function compositon" 'compose x y = + (cic:/matita/didactic/deriv/fcomp.con x y). + +notation "hvbox(a break ⊕ b)" + right associative with precedence 45 +for @{ 'oplus $a $b }. + +interpretation "function plus" 'oplus 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_mult: ∀x,y:R. (i (Rmult x y)) = (i x) · (i y). + +axiom freflex:F. +notation "ρ" + non associative with precedence 100 +for @{ 'rho }. +interpretation "function flip" 'rho = + cic:/matita/didactic/deriv/freflex.con. +axiom reflex_ok: ∀f:F. ρ ∘ f = (i (-R1)) · f. +axiom dereflex: ρ ' = i (-R1). (*Togliere*) + +axiom id:F. (* Funzione identita' *) +axiom fcomp_id_neutral: ∀f:F. f ∘ id = f. +axiom fcomp_id_commutative: ∀f:F. f ∘ id = id ∘ f. +axiom deid: id ' = i R1. +axiom rho_id: ρ ∘ ρ = id. + +lemma rho_disp: ρ = ρ ∘ (ρ ∘ ρ). + we need to prove (ρ = ρ ∘ (ρ ∘ ρ)). + by _ done. +qed. + +lemma id_disp: id = ρ ∘ (id ∘ ρ). + we need to prove (id = ρ ∘ (id ∘ ρ)). + by _ done. +qed. + +let rec felev (f:F) (n:nat) on n: F ≝ + match n with + [ O ⇒ i R1 + | S n ⇒ f · (felev f n) + ]. + +(* 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 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 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_distr2: ∀ f,g,h:F. (f · g) ∘ h = (f ∘ h) · (g ∘ h). + +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 cost_assorb: ∀x:R. ∀f:F. (i x) ∘ f = i x. +axiom cost_deriv: ∀x:R. (i x) ' = i R0. + + +definition fpari ≝ λ f:F. f = f ∘ ρ. +definition fdispari ≝ λ f:F. f = ρ ∘ (f ∘ ρ). +axiom cost_pari: ∀ x:R. fpari (i x). + +axiom meno_piu_i: (i (-R1)) · (i (-R1)) = i R1. + +notation "hvbox(a break ^ b)" + right associative with precedence 75 +for @{ 'elev $a $b }. + +interpretation "function power" 'elev x y = + (cic:/matita/didactic/deriv/felev.con x y). diff --git a/helm/software/matita/dama_didactic/ex_deriv.ma b/helm/software/matita/dama_didactic/ex_deriv.ma new file mode 100644 index 000000000..32e1ee8a5 --- /dev/null +++ b/helm/software/matita/dama_didactic/ex_deriv.ma @@ -0,0 +1,252 @@ +(**************************************************************************) +(* ___ *) +(* ||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/didactic/ex_deriv". + +include "deriv.ma". + +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) ∘ ρ). + conclude + (f ⊕ g) + = (f ⊕ (g ∘ ρ)) by _. + = ((f ∘ ρ) ⊕ (g ∘ ρ)) by _. + = ((f ⊕ g) ∘ ρ) by _ + done. +qed. + +theorem p_mult_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) ∘ ρ). + conclude + (f · g) + = (f · (g ∘ ρ)) by _. + = ((f ∘ ρ) · (g ∘ ρ)) by _. + = ((f · g) ∘ ρ) by _ + done. +qed. + +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) ∘ ρ))). + 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 _ + done. +qed. + +theorem d_mult_d_p: ∀f:F. ∀g:F. (fdispari f ∧ fdispari g) → fpari (f · g). + assume f:F. + assume g:F. + suppose (fdispari f ∧ fdispari g) (h). + by h we have (fdispari f) (h1) and (fdispari g) (h2). + we need to prove (fpari (f · g)) + or equivalently ((f · g) = (f · g) ∘ ρ). + conclude + (f · g) + = (f · (ρ ∘ (g ∘ ρ))) by _. + = ((ρ ∘ (f ∘ ρ)) · (ρ ∘ (g ∘ ρ))) by _. + = (((-R1) · (f ∘ ρ)) · (ρ ∘ (g ∘ ρ))) by _. + = (((-R1) · (f ∘ ρ)) · ((-R1) · (g ∘ ρ))) by _. + = ((-R1) · (f ∘ ρ) · (-R1) · (g ∘ ρ)) by _. + = ((-R1) · ((f ∘ ρ) · (-R1)) · (g ∘ ρ)) by _. + = ((-R1) · (-R1) · (f ∘ ρ) · (g ∘ ρ)) by _. + = (R1 · ((f ∘ ρ) · (g ∘ ρ))) by _. + = (((f ∘ ρ) · (g ∘ ρ))) by _. + = ((f · g) ∘ ρ) by _ + done. +qed. + +theorem p_mult_d_p: ∀f:F. ∀g:F. (fpari f ∧ fdispari g) → fdispari (f · g). + assume f:F. + assume g:F. + suppose (fpari f ∧ fdispari g) (h). + by h we have (fpari f) (h1) and (fdispari g) (h2). + we need to prove (fdispari (f · g)) + or equivalently ((f · g) = ρ ∘ ((f · g) ∘ ρ)). + conclude + (f · g) + = (f · (ρ ∘ (g ∘ ρ))) by _. + = ((f ∘ ρ) · (ρ ∘ (g ∘ ρ))) by _. + = ((f ∘ ρ) · ((-R1) · (g ∘ ρ))) by _. + = ((-R1) · ((f ∘ ρ) · (g ∘ ρ))) by _. + = ((-R1) · ((f · g) ∘ ρ)) by _. + = (ρ ∘ ((f · g) ∘ ρ)) by _ + done. +qed. + +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)) ∘ ρ). + by _ done. +qed. + +theorem p_mult_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)) ∘ ρ). + by _ done. +qed. + +theorem d_mult_c_d: ∀f:F. ∀x:R. fdispari f → fdispari (f · (i x)). + assume f:F. + assume x:R. + suppose (fdispari f) (h). + rewrite < fmult_commutative. + by _ done. +qed. + +theorem d_comp_d_d: ∀f,g:F. fdispari f → fdispari g → fdispari (f ∘ g). + assume f:F. + assume g:F. + suppose (fdispari f) (h1). + suppose (fdispari g) (h2). + we need to prove (fdispari (f ∘ g)) + or equivalently (f ∘ g = ρ ∘ ((f ∘ g) ∘ ρ)). + conclude + (f ∘ g) + = (ρ ∘ (f ∘ ρ) ∘ g) by _. + = (ρ ∘ (f ∘ ρ) ∘ ρ ∘ (g ∘ ρ)) by _. + = (ρ ∘ f ∘ (ρ ∘ ρ) ∘ (g ∘ ρ)) by _. + = (ρ ∘ f ∘ id ∘ (g ∘ ρ)) by _. + = (ρ ∘ ((f ∘ g) ∘ ρ)) by _ + done. +qed. + +theorem pari_in_dispari: ∀ f:F. fpari f → fdispari f '. + assume f:F. + suppose (fpari f) (h1). + we need to prove (fdispari f ') + or equivalently (f ' = ρ ∘ (f ' ∘ ρ)). + conclude + (f ') + = ((f ∘ ρ) ') by _. (*h1*) + = ((f ' ∘ ρ) · ρ ') by _. (*demult*) + = ((f ' ∘ ρ) · -R1) by _. (*deinv*) + = ((-R1) · (f ' ∘ ρ)) by _. (*fmult_commutative*) + = (ρ ∘ (f ' ∘ ρ)) (*reflex_ok*) by _ + done. +qed. + +theorem dispari_in_pari: ∀ f:F. fdispari f → fpari f '. + assume f:F. + suppose (fdispari f) (h1). + we need to prove (fpari f ') + or equivalently (f ' = f ' ∘ ρ). + conclude + (f ') + = ((ρ ∘ (f ∘ ρ)) ') by _. + = ((ρ ' ∘ (f ∘ ρ)) · ((f ∘ ρ) ')) by _. + = (((-R1) ∘ (f ∘ ρ)) · ((f ∘ ρ) ')) by _. + = (((-R1) ∘ (f ∘ ρ)) · ((f ' ∘ ρ) · (-R1))) by _. + = ((-R1) · ((f ' ∘ ρ) · (-R1))) by _. + = (((f ' ∘ ρ) · (-R1)) · (-R1)) by _. + = ((f ' ∘ ρ) · ((-R1) · (-R1))) by _. + = ((f ' ∘ ρ) · R1) by _. + = (f ' ∘ ρ) by _ + done. +qed. + +(* +alias id "plus" = "cic:/matita/nat/plus/plus.con". +theorem de_prodotto_funzioni: + ∀ n:nat. (id ^ (plus n (S O))) ' = (i (n + (S O))) · (id ^ n). + assume n:nat. + we proceed by induction on n to prove + ((id ^ (plus n (S O))) ' = (i (n + (S O))) · (id ^ n)). + case O. + we need to prove ((id ^ (plus O (S O))) ' = (i (S O)) · (id ^ O)). + conclude + ((id ^ (plus O (S O))) ') + = ((id ^ (S O)) ') by _. + = ((id · (id ^ O)) ') by _. + = ((id · (i R1)) ') by _. + = (id ') by _. + = (i R1) by _. + = (i R1 · i R1) by _. + = (i (R0 + R1) · R1) by _. + = ((i (S O)) · (id ^ O)) by _ + done. + case S (n:nat). + by induction hypothesis we know + ((id ^ (plus n (S O))) ' = (i (n + (S O))) · (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)))). + 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 _ + done. +qed. +*) + +let rec times (n:nat) (x:R) on n: R ≝ + match n with + [ O ⇒ R0 + | S n ⇒ Rplus x (times n x) + ]. + +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 e:F. +axiom deriv_e: e ' = e. +axiom e1: e · (e ∘ ρ) = R1. + +(* +theorem decosh_senh: + (invS (S O) · (e ⊕ (e ∘ ρ)))' = (invS (S O) · (e ⊕ (ρ ∘ (e ∘ ρ)))). +*) \ No newline at end of file diff --git a/helm/software/matita/dama_didactic/ex_seq.ma b/helm/software/matita/dama_didactic/ex_seq.ma new file mode 100644 index 000000000..61952d1b0 --- /dev/null +++ b/helm/software/matita/dama_didactic/ex_seq.ma @@ -0,0 +1,201 @@ +(**************************************************************************) +(* ___ *) +(* ||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/didactic/ex_seq". + +include "sequences.ma". + +(* +ESERCIZI SULLE SUCCESSIONI + +Dimostrare che la successione alpha converge a 0 +*) + +definition F ≝ λ x:R.Rdiv x (S (S O)). + +definition alpha ≝ successione F R1. + +axiom cont: continuo F. + +lemma l1: monotone_not_increasing alpha. + we need to prove (monotone_not_increasing alpha) + or equivalently (∀n:nat. alpha (S n) ≤ alpha n). + assume n:nat. + we need to prove (alpha (S n) ≤ alpha n) + or equivalently (Rdiv (alpha n) (S (S O)) ≤ alpha n). + by _ done. +qed. + +lemma l2: inf_bounded alpha. + we need to prove (inf_bounded alpha) + or equivalently (∃m. ∀n:nat. m ≤ alpha n). + (* da trovare il modo giusto *) + cut (∀n:nat.R0 ≤ alpha n).by (ex_intro ? ? R0 Hcut) done. + (* fatto *) + we need to prove (∀n:nat. R0 ≤ alpha n). + assume n:nat. + we proceed by induction on n to prove (R0 ≤ alpha n). + case O. + (* manca il comando + the thesis becomes (R0 ≤ alpha O) + or equivalently (R0 ≤ R1). + by _ done. *) + (* approssimiamo con questo *) + we need to prove (R0 ≤ alpha O) + or equivalently (R0 ≤ R1). + by _ done. + case S (m:nat). + by induction hypothesis we know (R0 ≤ alpha m) (H). + we need to prove (R0 ≤ alpha (S m)) + or equivalently (R0 ≤ Rdiv (alpha m) (S (S O))). + by _ done. +qed. + +axiom xxx': +∀ F: R → R. ∀b:R. continuo F → + ∀ l. tends_to (successione F b) l → + punto_fisso F l. + +theorem dimostrazione: tends_to alpha O. + by _ let l:R such that (tends_to alpha l) (H). +(* unfold alpha in H. + change in match alpha in H with (successione F O). + check(xxx' F cont l H).*) + by (lim_punto_fisso F R1 cont l H) we proved (punto_fisso F l) (H2) + that is equivalent to (l = (Rdiv l (S (S O)))). + by _ we proved (tends_to alpha l = tends_to alpha O) (H4). + rewrite < H4. + by _ done. +qed. + +(******************************************************************************) + +(* Dimostrare che la successione alpha2 diverge *) + +definition F2 ≝ λ x:R. Rmult x x. + +definition alpha2 ≝ successione F2 (S (S O)). + +lemma uno: ∀n. alpha2 n ≥ R1. + we need to prove (∀n. alpha2 n ≥ R1). + assume n:nat. + we proceed by induction on n to prove (alpha2 n ≥ R1). + case O. + alias num (instance 0) = "natural number". + we need to prove (alpha2 0 ≥ R1) + or equivalently ((S (S O)) ≥ R1). + by _ done. + case S (m:nat). + by induction hypothesis we know (alpha2 m ≥ R1) (H). + we need to prove (alpha2 (S m) ≥ R1) + or equivalently (Rmult (alpha2 m) (alpha2 m) ≥ R1).letin xxx := (n ≤ n); + by _ we proved (R1 · R1 ≤ alpha2 m · alpha2 m) (H1). + by _ we proved (R1 · R1 = R1) (H2). + rewrite < H2. + by _ done. +qed. + +lemma mono1: monotone_not_decreasing alpha2. + we need to prove (monotone_not_decreasing alpha2) + or equivalently (∀n:nat. alpha2 n ≤ alpha2 (S n)). + assume n:nat. + we need to prove (alpha2 n ≤ alpha2 (S n)) + or equivalently (alpha2 n ≤ Rmult (alpha2 n) (alpha2 n)). + by _ done. +qed. + +(* +lemma due: ∀n. Relev (alpha2 0) n ≥ R0. + we need to prove (∀n. Relev (alpha2 0) n ≥ R0) + or equivalently (∀n. Relev (S (S O)) n ≥ R0). + by _ done. +qed. + +lemma tre: ∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n). + we need to prove (∀n. alpha2 (S n) ≥ Relev (alpha2 0) (S n)). + assume n:nat. + we proceed by induction on n to prove (alpha2 (S n) ≥ Relev (alpha2 0) (S n)). + case 0. + we need to prove (alpha2 1 ≥ Relev (alpha2 0) R1) + or equivalently (Rmult R2 R2 ≥ R2). + by _ done. + case S (m:nat). + by induction hypothesis we know (alpha2 (S m) ≥ Relev (alpha2 0) (S m)) (H). + we need to prove (alpha2 (S (S m)) ≥ Relev (alpha2 0) (S (S m))) + or equivalently + (*..TODO..*) + +theorem dim2: tends_to_inf alpha2. +(*..TODO..*) +qed. +*) + +(******************************************************************************) + +(* Dimostrare che la successione alpha3 converge a 0 *) +(* +definition alpha3 ≝ successione F2 (Rdiv (S 0) (S (S 0))). + +lemma quattro: ∀n. alpha3 n ≤ R1. + assume n:nat. + we need to prove (∀n. alpha3 n ≤ R1). + we proceed by induction on n to prove (alpha3 n ≤ R1). + case O. + we need to prove (alpha3 0 ≤ R1). + by _ done. + case S (m:nat). + by induction hypothesis we know (alpha3 m ≤ R1) (H). + we need to prove (alpha3 (S m) ≤ R1) + or equivalently (Rmult (alpha3 m) (alpha3 m) ≤ R1). + by _ done. + qed. + +lemma mono3: monotone_not_increasing alpha3. + we need to prove (monotone_not_increasing alpha3) + or equivalently (∀n:nat. alpha (S n) ≤ alpha n). + assume n:nat. + we need to prove (alpha (S n) ≤ alpha n) + or equivalently (Rmult (alpha3 n) (alpha3 n) ≤ alpha3 n). + by _ done. +qed. + +lemma bound3: inf_bounded alpha3. + we need to prove (inf_bounded alpha3) + or equivalently (∃m. ∀n:nat. m ≤ alpha3 n). + (* da trovare il modo giusto *) + cut (∀n:nat.R0 ≤ alpha3 n).by (ex_intro ? ? R0 Hcut) done. + (* fatto *) + we need to prove (∀n:nat. R0 ≤ alpha3 n). + assume n:nat. + we proceed by induction on n to prove (R0 ≤ alpha3 n). + case O. + (* manca il comando + the thesis becomes (R0 ≤ alpha O) + or equivalently (R0 ≤ R1). + by _ done. *) + (* approssimiamo con questo *) + we need to prove (R0 ≤ alpha3 O) + or equivalently (R0 ≤ Rdiv (S 0) (S (S 0))). + by _ done. + case S (m:nat). + by induction hypothesis we know (R0 ≤ alpha3 m) (H). + we need to prove (R0 ≤ alpha3 (S m)) + or equivalently (R0 ≤ Rmult (alpha3 m) (alpha3 m)). + by _ done. +qed. + +theorem dim3: tends_to alpha3 O. +(*..TODO..*) +qed. +*) \ No newline at end of file diff --git a/helm/software/matita/dama_didactic/makefile b/helm/software/matita/dama_didactic/makefile new file mode 100644 index 000000000..ce86d1360 --- /dev/null +++ b/helm/software/matita/dama_didactic/makefile @@ -0,0 +1,33 @@ +H=@ + +RT_BASEDIR=../ +OPTIONS=-bench +MMAKE=$(RT_BASEDIR)matitamake $(OPTIONS) +CLEAN=$(RT_BASEDIR)matitaclean $(OPTIONS) +MMAKEO=$(RT_BASEDIR)matitamake.opt $(OPTIONS) +CLEANO=$(RT_BASEDIR)matitaclean.opt $(OPTIONS) + +devel:=$(shell basename `pwd`) + +all: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) build $(devel) +clean: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) clean $(devel) +cleanall: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEAN) all + +all.opt opt: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) build $(devel) +clean.opt: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) clean $(devel) +cleanall.opt: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MCLEANO) all + +%.mo: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) $@ +%.mo.opt: preall + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKEO) $(@:.opt=) + +preall: + $(H)MATITA_FLAGS=$(MATITA_FLAGS) $(MMAKE) init $(devel) + diff --git a/helm/software/matita/dama_didactic/reals.ma b/helm/software/matita/dama_didactic/reals.ma new file mode 100644 index 000000000..966747c76 --- /dev/null +++ b/helm/software/matita/dama_didactic/reals.ma @@ -0,0 +1,103 @@ +(**************************************************************************) +(* ___ *) +(* ||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/didactic/reals". + +include "nat/plus.ma". + +axiom R:Type. +axiom R0:R. +axiom R1:R. +axiom Rplus: R→R→R. +axiom Ropp:R→R. (*funzione da x → -x*) +axiom Rmult: R→R→R. +axiom Rdiv: R→R→R. +axiom Relev: R→R→R. +axiom Rle: R→R→Prop. +axiom Rge: R→R→Prop. + +interpretation "real plus" 'plus x y = + (cic:/matita/didactic/reals/Rplus.con x y). + +interpretation "real opp" 'uminus x = + (cic:/matita/didactic/reals/Ropp.con x). + +notation "hvbox(a break · b)" + right associative with precedence 55 +for @{ 'mult $a $b }. + +interpretation "real mult" 'mult x y = + (cic:/matita/didactic/reals/Rmult.con x y). + +interpretation "real leq" 'leq x y = + (cic:/matita/didactic/reals/Rle.con x y). + +interpretation "real geq" 'geq x y = + (cic:/matita/didactic/reals/Rge.con x y). + +let rec elev (x:R) (n:nat) on n: R ≝ + match n with + [O ⇒ R1 + | S n ⇒ Rmult x (elev x n) + ]. + +let rec real_of_nat (n:nat) : R ≝ + match n with + [ O ⇒ R0 + | S n ⇒ + match n with + [ O ⇒ R1 + | _ ⇒ real_of_nat n + R1 + ] + ]. + +coercion cic:/matita/didactic/reals/real_of_nat.con. + +axiom Rplus_commutative: ∀x,y:R. x+y = y+x. +axiom R0_neutral: ∀x:R. x+R0=x. +axiom Rdiv_le: ∀x,y:R. R1 ≤ y → Rdiv x y ≤ x. +axiom R2_1: R1 ≤ S (S O). +(* assioma falso! *) +axiom Rmult_Rle: ∀x,y,z,w. x ≤ y → z ≤ w → Rmult x z ≤ Rmult y w. + +axiom Rdiv_pos: ∀ x,y:R. R0 ≤ x → R1 ≤ y → R0 ≤ Rdiv x y. +axiom Rle_R0_R1: R0 ≤ R1. +axiom div: ∀x:R. x = Rdiv x (S (S O)) → x = O. +(* Proprieta' elevamento a potenza NATURALE *) +axiom elev_incr: ∀x:R.∀n:nat. R1 ≤ x → elev x (S n) ≥ elev x n. +axiom elev_decr: ∀x:R.∀n:nat. R0 ≤ x ∧ x ≤ R1 → elev x (S n) ≤ elev x n. +axiom Rle_to_Rge: ∀x,y:R. x ≤ y → y ≥ x. +axiom Rge_to_Rle: ∀x,y:R. x ≥ y → y ≤ x. + +(* Proprieta' elevamento a potenza TRA REALI *) +(* +axiom Relev_ge: ∀x,y:R. + (x ≥ R1 ∧ y ≥ R1) ∨ (x ≤ R1 ∧ y ≤ R1) → Relev x y ≥ x. +axiom Relev_le: ∀x,y:R. + (x ≥ R1 ∧ y ≤ R1) ∨ (x ≤ R1 ∧ y ≥ R1) → Relev x y ≤ x. +*) + +lemma stupido: ∀x:R.R0+x=x. + assume x:R. + conclude (R0+x) = (x+R0) by _. + = x by _ + done. +qed. + +axiom opposto1: ∀x:R. x + -x = R0. +axiom opposto2: ∀x:R. -x = Rmult x (-R1). +axiom meno_piu: Rmult (-R1) (-R1) = R1. +axiom R1_neutral: ∀x:R.Rmult R1 x = x. +(* assioma falso *) +axiom uffa: ∀x,y:R. R1 ≤ x → y ≤ x · y. diff --git a/helm/software/matita/dama_didactic/sequences.ma b/helm/software/matita/dama_didactic/sequences.ma new file mode 100644 index 000000000..66b64e5bc --- /dev/null +++ b/helm/software/matita/dama_didactic/sequences.ma @@ -0,0 +1,57 @@ +(**************************************************************************) +(* ___ *) +(* ||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/didactic/sequences". + +include "reals.ma". + +axiom continuo: (R → R) → Prop. +axiom tends_to: (nat → R) → R → Prop. +axiom tends_to_inf: (nat → R) → Prop. + +definition monotone_not_increasing ≝ + λ alpha:nat→R. + ∀n:nat.alpha (S n) ≤ alpha n. + +definition inf_bounded ≝ + λ alpha:nat → R. + ∃ m. ∀ n:nat. m ≤ alpha n. + +axiom converge: ∀ alpha. + monotone_not_increasing alpha → + inf_bounded alpha → + ∃ l. tends_to alpha l. + +definition punto_fisso := + λ F:R→R. λ x. x = F x. + +let rec successione F x (n:nat) on n : R ≝ + match n with + [ O ⇒ x + | S n ⇒ F (successione F x n) + ]. + +axiom lim_punto_fisso: +∀ F: R → R. ∀b:R. continuo F → + let alpha := successione F b in + ∀ l. tends_to alpha l → + punto_fisso F l. + +definition monotone_not_decreasing ≝ + λ alpha:nat→R. + ∀n:nat.alpha n ≤ alpha (S n). + +definition sup_bounded ≝ + λ alpha:nat → R. + ∃ m. ∀ n:nat. alpha n ≤ m.