--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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
--- /dev/null
+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)
+
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
projects / helm.git / commitdiff