Require Export Reals.
Open Scope R_scope.

Print derivable_pt_lim.

Inductive fonction : Set :=
(* Fonctions de base *)
| Const : R -> fonction
| Id : fonction
| Exp : fonction
| Sin : fonction
| Cos : fonction
| Log : fonction
| Valeur_absolue : fonction
| Racine : fonction
(* Opérations sur les fonctions. *)
| Oppose : fonction -> fonction
| Inverse : fonction -> fonction
| Plus : fonction -> fonction -> fonction
| Fois : fonction -> fonction -> fonction
| Compo : fonction -> fonction -> fonction
| Puiss : fonction -> nat -> fonction
.

(* Moins et Sur, c'est du sucre syntaxique pour
Plus Oppose et  Fois Inverse *)
Definition Moins f g := Plus f (Oppose g).
Definition Sur f g := Fois f (Inverse g).

(* 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. Choisissons le sens
du produit *)

Print pow.
Print opp_fct.
Print inv_fct.

Fixpoint interp (f : fonction) : R -> R :=
match f with
| Id => id
| Const k => fct_cte k
| Exp => exp
| Sin => sin
| Cos => cos
| Racine => sqrt
| Valeur_absolue => Rabs
| Log => ln
| Oppose f => opp_fct (interp f)
| Inverse f => inv_fct (interp f)
| Plus g h =>  plus_fct  (interp g) (interp h)
| Fois g h => mult_fct (interp g) (interp h)
| Compo g h => comp (interp g) (interp h)
| Puiss g n => fun x => pow (interp g x) n
end.

Theorem interp_moins : forall f g,
interp (Moins f g) = minus_fct (interp f) (interp g).
auto with real.
Qed.

Theorem interp_sur : forall f g,
interp (Sur f g) = div_fct (interp f) (interp g).
auto with real.
Qed.

Fixpoint deriv (f : fonction) : fonction :=
match f with
| Id => Const 1
| Const _ => Const 0
| Exp => Exp
| Sin => Cos
| Cos => Oppose Sin
| Racine => Inverse (Fois (Const 2) Racine)
| Log => Inverse Id
| Valeur_absolue => Sur Id Valeur_absolue
| Oppose g => Oppose (deriv g)
| Inverse g => Oppose (Sur (deriv g) (Fois g g))
| Plus g h => Plus (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.

Inductive derivable : fonction -> R -> Prop :=
| derivable_id : forall (x : R), derivable Id x
| derivable_const : forall (x y : R), derivable (Const y) x
| derivable_exp : forall (x : R), derivable Exp x
| derivable_cos: forall (x:R), derivable Cos x
| derivable_sin : forall (x : R), derivable Sin x
| derivable_log : forall (x : R),
  x > 0 -> derivable Log x
| derivable_racine : forall (f : fonction) (x : R),
  x > 0 -> derivable Racine x
| derivable_valeur_absolue : forall (x : R),
  x <> 0 -> derivable Valeur_absolue x
| derivable_oppose : forall (f : fonction) (x: R),
derivable f x -> derivable (Oppose f) x
| derivable_inverse : forall (f : fonction) (x: R),
derivable f x -> interp f x <> 0 -> derivable (Inverse f) x
| derivable_plus : forall (f g : fonction) (x : R),
derivable f x -> derivable g x -> derivable (Plus f g) x
| derivable_fois : forall (f g : fonction) (x : R),
derivable f x -> derivable g x -> derivable (Fois f g) x
| derivable_compo : forall (f g : fonction) (x : R),
  derivable f (interp g x) -> derivable g x -> derivable (Compo f g) x
| derivable_puiss_O : forall (f : fonction) (x : R),
  derivable (Puiss f O) x
| derivable_puiss_S : forall (f : fonction) (x : R) (n : nat),
  derivable f x -> derivable (Puiss f (S n)) x
.

Hint Constructors derivable.

Theorem derivable_moins : forall (f g : fonction) (x : R),
derivable f x -> derivable g x -> derivable (Moins f g) x.
intros.
unfold Moins.
auto.
Qed.

Theorem derivable_sur : forall (f g : fonction) (x : R),
  derivable f x -> derivable g x -> interp g x <> 0 ->
  derivable (Sur f g) x.
intros.
unfold Sur.
auto.
Qed.

Hint Resolve derivable_moins derivable_sur.


Ltac unfold_fct :=
match goal with
 | |- context k [ opp_fct ?f1 ?x ] =>
   change (opp_fct f1 x) with (- (f1 x)) ; unfold_fct
 | |- context k [ inv_fct ?f1 ?x ] =>
   change (inv_fct f1 x) with (/ (f1 x)) ; unfold_fct
 | |- context k [ plus_fct ?f1 ?f2 ?x ] =>
   change (plus_fct f1 f2 x) with (f1 x + f2 x) ; unfold_fct
 | |- context k [ minus_fct ?f1 ?f2 ?x ] =>
   change (minus_fct f1 f2 x) with (f1 x - f2 x) ; unfold_fct
 | |- context k [ mult_fct ?f1 ?f2 ?x ] =>
   change (mult_fct f1 f2 x) with (f1 x * f2 x) ; unfold_fct
 | |- context k [ div_fct ?f1 ?f2 ?x ] =>
   change (div_fct f1 f2 x) with (f1 x / f2 x) ; unfold_fct
 | |- context k [comp ?f1 ?f2 ?x] =>
   change (comp f1 f2 x) with (f1 (f2 x)) ; unfold_fct
 | _ => idtac
end.

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

(* Cas de la constante. *)
compute.
intros.
exists (mkposreal eps H0).
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'identite. *)
compute.
intros.
exists (mkposreal eps H0).
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 l'exponentielle, du sinus, du cosinus. *)
intros.
apply derivable_pt_lim_exp.
intros.
apply derivable_pt_lim_sin.
intros.
unfold deriv.
unfold interp.
unfold_fct.
apply derivable_pt_lim_cos.

(* Cas du logarithme *)
intros.
unfold deriv.
unfold interp.
unfold_fct.
apply derivable_pt_lim_ln.
inversion H.
apply H0.

(* Cas de la valeur absolue *)
intros.
inversion H.
subst.
unfold deriv.
unfold Sur.
unfold interp.
unfold_fct.
destruct (Rdichotomy _ _ H0).
rewrite Rabs_left.
rewrite <- Ropp_inv_permute.
rewrite Ropp_mult_distr_r_reverse.
rewrite Rinv_r.
apply Rabs_derive_2.
assumption.
assumption.
assumption.
assumption.
rewrite Rabs_right.
rewrite Rinv_r.
apply Rabs_derive_1.
assumption.
assumption.
apply Rgt_ge.
assumption.

(* La racine carrée. *)
intros.
unfold deriv.
unfold interp.
unfold_fct.
apply derivable_pt_lim_sqrt.
inversion H.
auto.

(* Cas de l'opposé *)
intros.
unfold deriv.
fold deriv.
unfold interp.
fold interp.
unfold_fct.
apply derivable_pt_lim_opp.
apply IHf.
inversion H.
apply H1.

(* Cas de l'inverse *)
intros.
unfold deriv.
fold deriv.
unfold Sur.
unfold interp.
fold interp.
unfold_fct.
(* apply derivable_pt_lim_inv.
Malheur ! Le théorème n'existe pas. Je dois donc le faire à
la main. *)
unfold_fct.
inversion H.
subst.

(* Je vais utiliser le théorème de correction de la dérivée d'une division g/f, où
g est la constante 1. *)
generalize (
derivable_pt_lim_div (fct_cte 1) (interp f) x 0 (interp (deriv f) x)
(derivable_pt_lim_const 1 x)
(IHf x H1)
H2
).
unfold derivable_pt_lim.
intros.
destruct (H0 eps).
assumption.
exists x0.
intros.
generalize (H4 h H5 H6).
unfold_fct.
rewrite <- (Rmult_1_l (/ interp f (x+h))).
rewrite <- (Rmult_1_l (/ interp f x)).
unfold Rdiv.
unfold fct_cte.
unfold Rsqr.
rewrite Rmult_1_r.
rewrite Rmult_0_l.
rewrite Rminus_0_l.
rewrite Ropp_mult_distr_l_reverse.
trivial.

(* Cas de la somme. *)
unfold deriv.
fold deriv.
unfold interp.
fold interp.
intros.
unfold_fct.
inversion_clear H.
apply derivable_pt_lim_plus ; auto.

(* Cas du fois. *)
unfold deriv.
fold deriv.
unfold interp.
fold interp.
intros.
unfold_fct.
inversion_clear H.
apply derivable_pt_lim_mult ; auto.

(* Cas de  la composee. *)
unfold deriv.
fold deriv.
unfold interp.
fold interp.
intros.
unfold_fct.
inversion_clear H.
apply derivable_pt_lim_comp ; auto.

(* 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.
intros.
apply derivable_pt_lim_const.
intros.
unfold deriv.
fold deriv.
rewrite H.
unfold interp.
fold interp.
unfold_fct.
unfold fct_cte.
rewrite (Rmult_comm (INR (S n0) * interp (deriv f) x)).
rewrite <- Rmult_assoc.
inversion_clear H0.
apply derivable_pt_lim_comp ; auto.
rewrite Rmult_comm.
apply (derivable_pt_lim_pow (interp f x) (S n0)).

Qed.

Hint Resolve deriv_correcte.

(* Si on veut... *)
Ltac inversion_fonction f :=
 match constr:f with
  | (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)
  | (div_fct ?f1 ?f2) => 
     let g1 := inversion_fonction f1 with g2 := inversion_fonction f2 in constr:(Sur g1 g2)
  | (inv_fct ?f) =>
     let g := inversion_fonction f in constr:(Inverse g)    
  | (opp_fct ?f) => let g := inversion_fonction f in constr:(Oppose g)
  | exp => constr:Exp
  | sin => constr:Sin
  | cos => constr:Cos
  | ln => constr:Log
  | Rabs => constr:Valeur_absolue
  | sqrt => constr:Racine
  | (fun x => x) => constr:Id 
  | id => constr:Id
  | (fun _ => ?x) => constr:(Const x)
  | fct_cte ?x => constr:(Const x)
  | (fun x => ?f x) => inversion_fonction f (* eta-conversion *)
end.

Ltac eta_contraction f := match f with
| (fun x => ?g x) => eta_contraction g
| _ => constr:f
end.

Ltac derive f p :=
  let f1 := eta_contraction f in
  let f0 := inversion_fonction f1 in
  let g0 := constr:(interp (deriv f0)) in
  let h := fresh "h" in (
  assert (h: forall x : R, p x -> derivable_pt_lim f1 x (g0 x)) ; [
   intro x ; intro ; apply (deriv_correcte f0 x) ; auto
   | simpl in h]
  ).

Theorem sym_diff : forall (T : Type) (x y : T), x<>y -> y<>x.
intros.
intro.
apply H.
symmetry.
assumption.
Qed.

Hint Resolve sym_diff.

(* Dans cet exemple, la condition de dérivabilité semble triviale, mais
en réalité elle ne l'est pas tant que cela : 2 <> 0. *)
Theorem bidon : False.
derive cos (fun _:R => True).
derive (inv_fct id) (fun x => x<>0).
derive (div_fct (fct_cte 2)  (fct_cte 2)) (fun _:R => True).
apply derivable_sur ;auto.
simpl.
unfold fct_cte.
apply sym_diff ; auto with real.
*)