(* *)
(**************************************************************************)
-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.
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.
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.
done.
qed.
-(*
-alias id "plus" = "cic:/matita/nat/plus/plus.con".
+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
].
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.
(*
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 ∘ ρ)))).
+*)
projects / helm.git / blobdiff