Require Export Reals.
Open Scope R_scope.

Print derivable_pt_lim.

Inductive fonction : Set :=
| Id : fonction
| Const : R -> fonction
| Exp : fonction
| Sin : fonction
| Cos : fonction
| Plus : fonction -> fonction -> fonction
| Moins : fonction -> fonction -> fonction
| Fois : fonction -> fonction -> fonction
| Compo : fonction -> fonction -> fonction
| Puiss : fonction -> nat -> fonction
.

(* La notion de puissance est ambigue.
La puissance f^g de deux fonctions n'est pas toujours definie,
en revanche f^n l'est pour n entier naturel et dans les deux sens
d'itération et de puissance pour le produit. *)

Fixpoint interp (f : fonction) : R -> R :=
match f with
| Id => fun x => x
| Const k => fun _ => k
| Exp => exp
| Sin => sin
| Cos => cos
| Plus g h => fun x => interp g x + interp h x
| Moins g h => fun x => interp g x - interp h x
| Fois g h => fun x => interp g x * interp h x
| Compo g h => fun x => interp g (interp h x)
| Puiss f n => fun x => pow (interp f x) n
end.

Fixpoint deriv (f : fonction) : fonction :=
match f with
| Id => Const 1
| Const _ => Const 0
| Exp => Exp
| Sin => Cos
| Cos => Moins (Const 0) Sin
| Plus g h => Plus (deriv g) (deriv h)
| Moins g h => Moins (deriv g) (deriv h)
| Fois g h => Plus (Fois (deriv g) h) (Fois g (deriv h))
| Compo g h => Fois (Compo (deriv g) h) (deriv h)
| Puiss f O => Const 0
| Puiss f (S n) => Fois (Fois (Const (INR (S n))) (deriv f)) (Puiss f n)
end.

Theorem deriv_correcte : forall (f : fonction) (x : R),
derivable_pt_lim (interp f) x (interp (deriv f) x).
Proof.
induction f.

(* Cas de l'identite. *)
compute.
intros.
exists (mkposreal eps H).
intros.
rewrite (Rplus_comm (x + h)).
rewrite <- Rplus_assoc.
rewrite Rplus_opp_l.
rewrite Rplus_0_l.
rewrite Rinv_r.
rewrite Rplus_opp_r.
rewrite Ropp_0.
elim Rcase_abs.
trivial.
trivial.
trivial.

(* Cas de la constante. *)
compute.
intros.
exists (mkposreal eps H).
intros.
rewrite Rplus_opp_r.
rewrite Ropp_0.
rewrite Rplus_0_r.
rewrite Rmult_0_l.
rewrite Ropp_0.
elim Rcase_abs.
trivial.
trivial.

(* Cas de l'exponentielle, du sinus. *)
apply derivable_pt_lim_exp.
apply derivable_pt_lim_sin.

(* Cas du cosinus. *)
unfold deriv.
unfold interp.
intros.
rewrite Rminus_0_l.
apply derivable_pt_lim_cos.

(* Cas de la somme. *)
unfold deriv.
fold deriv.
unfold interp.
fold interp.
intros.
assert
(plus_fct (interp f1) (interp f2) = fun x0 => interp f1 x0 + interp f2 x0).
(unfold plus_fct;reflexivity).
rewrite <- H.
apply derivable_pt_lim_plus.
apply IHf1.
apply IHf2.

(* Cas soustraction. *)
unfold deriv.
fold deriv.
unfold interp.
fold interp.
intros.
assert
(minus_fct (interp f1) (interp f2) = fun x0 : R => interp f1 x0 - interp f2 x0).
unfold minus_fct.
reflexivity.
rewrite <- H.
apply derivable_pt_lim_minus.
apply IHf1.
apply IHf2.

(* Cas du fois. *)
unfold deriv.
fold deriv.
unfold interp.
fold interp.
intros.
assert
(mult_fct (interp f1) (interp f2) = fun x0 : R => interp f1 x0 * interp f2 x0).
unfold mult_fct.
reflexivity.
rewrite <- H.
apply derivable_pt_lim_mult.
apply IHf1.
apply IHf2.

(* Cas de  la composee. *)
unfold deriv.
fold deriv.
unfold interp.
fold interp.
intros.
assert
(comp (interp f1) (interp f2) = fun x0 : R => interp f1 (interp f2 x0)).
unfold comp.
reflexivity.
rewrite <- H.
apply derivable_pt_lim_comp.
apply IHf2.
apply IHf1.

(* Cas de la puissance : le faire a la main. En fait, on dit que f^n,
c'est la composée f suivie de .^n (càd. .^n o f)  *)
assert (forall n : nat, 
 interp (Puiss f n) = comp (fun x => pow x n) (interp f)).
induction n0.
compute.
reflexivity.
simpl.
unfold comp.
reflexivity.
(* Du coup, on raisonne non pas par induction sur la puissance n,
mais simplement par cas. *)
case n.
simpl.
assert ((fun _ => 1) = fct_cte 1).
compute.
reflexivity.
rewrite H0.
apply derivable_pt_lim_const.
intros.
unfold deriv.
fold deriv.
rewrite H.
unfold interp.
fold interp.
rewrite (Rmult_comm (INR (S n0) * interp (deriv f) x)).
rewrite <- Rmult_assoc.
apply derivable_pt_lim_comp.
apply IHf.
rewrite Rmult_comm.
apply (derivable_pt_lim_pow (interp f x) (S n0)).
Qed.

Hint Resolve deriv_correcte.

Ltac inversion_fonction f :=
 match constr:f with
  | (comp ?f1 ?f2) =>
     let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Compo g1 g2)
  | (plus_fct ?f1 ?f2) => 
     let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Plus g1 g2)
  | (minus_fct ?f1 ?f2) => 
     let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Moins g1 g2)
  | (mult_fct ?f1 ?f2) => 
     let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Fois g1 g2)
  | (pow_fct ?f ?m) =>
     let g := inversion_fonction f in constr:(Puiss g m)
  | exp => constr:Exp
  | sin => constr:Sin
  | cos => constr:Cos
  | id => constr:Id
  | (fun x => x) => constr:Id 
  | (fun _ => ?y) => constr:(Const y)
  | fct_cte ?x => constr:(Const x)
  | (fun x => ?f x) => inversion_fonction f
end.

Ltac derive f :=
  let f0 := inversion_fonction f in
  let h := fresh "h" in (
  assert (h: forall y, derivable_pt_lim f y (interp (deriv f0) y));
  [ apply (deriv_correcte f0) | simpl in h ]
).