]> matita.cs.unibo.it Git - helm.git/commitdiff
Very incomplete example of simple calculus exercises in Matita.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 21 Nov 2007 16:16:58 +0000 (16:16 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 21 Nov 2007 16:16:58 +0000 (16:16 +0000)
helm/software/matita/dama_didactic/bottom.ma [new file with mode: 0644]
helm/software/matita/dama_didactic/deriv.ma [new file with mode: 0644]
helm/software/matita/dama_didactic/ex_deriv.ma [new file with mode: 0644]
helm/software/matita/dama_didactic/ex_seq.ma [new file with mode: 0644]
helm/software/matita/dama_didactic/makefile [new file with mode: 0644]
helm/software/matita/dama_didactic/reals.ma [new file with mode: 0644]
helm/software/matita/dama_didactic/sequences.ma [new file with mode: 0644]

diff --git a/helm/software/matita/dama_didactic/bottom.ma b/helm/software/matita/dama_didactic/bottom.ma
new file mode 100644 (file)
index 0000000..bed8ec6
--- /dev/null
@@ -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 (file)
index 0000000..f4de775
--- /dev/null
@@ -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 (file)
index 0000000..32e1ee8
--- /dev/null
@@ -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 (file)
index 0000000..61952d1
--- /dev/null
@@ -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 (file)
index 0000000..ce86d13
--- /dev/null
@@ -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 (file)
index 0000000..966747c
--- /dev/null
@@ -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 (file)
index 0000000..66b64e5
--- /dev/null
@@ -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.