Require Export Reals.
Require Export Quote.

Print varmap.
Print index.

Open Scope R_scope.

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
(* La variable *)
| Var : index -> 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).

Hint Unfold Moins.
Hint Unfold Sur.

(* 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.

(* L'interprétation d'une fonction est soumise à une varmap.
Le problème, c'est qu'une variable ne fait pas toujours référence à une fonction.

Nous aurions pu aussi définir varmap_find2 à valeur dans un type somme comme
(fonction | index) permettant d'indiquer quelle variable n'est pas instanciée dans la fonction.
Mais cette option a posé des problèmes très tôt dans les théorèmes : deux fonctions donnant la même interprétation
dans une varmap fixée où elles sont interprétables (i.e. où toutes les variables sont instanciées) donnent
des interprétations différentes dans une varmap vide par exemple.

Nous aurions pu utiliser une autre fonction que varmap_find, renvoyant une donnée de type
option fonction. Mais c'est impossible à manipuler en pratique dans les grosses preuves. En effet, 
il faut relier le fait qu'une fonction soit interprétable (i.e. que toutes ses variables soient instanciées)
et son interprétation effective.

Tant pis, si une fonction n'est pas trouvée, elle est par défaut instanciée en 0.
(C'est le choix de langages de programmation comme Basic, d'instancier en 0
toute variable non déclarée.)
Ce choix est judicieux en ce sens qu'il reste cohérent si une variable non instanciée
est dérivée, en supposant que sa dérivée ne soit pas instanciée non plus
dans la varmap des dérivées.

*)

Print index.
Print varmap.

Fixpoint interp (v : varmap (R -> R)) (f : fonction) {struct f} : (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 g => opp_fct (interp v g)
| Inverse g => inv_fct( interp v g )
| Plus g h => plus_fct (interp v g) (interp v h)
| Fois g h => mult_fct (interp v g) (interp v h)
| Compo g h => comp (interp v g) (interp v h)
| Puiss g n => fun x => pow (interp v g x) n
| Var x => varmap_find (fct_cte 0) x v
end.

Theorem interp_moins : forall v f g,
interp v (Moins f g) = minus_fct (interp v f) (interp v g).
auto.
Defined.

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

(* On va définir une fonction dérivée telle que, si f est une fonction interprétable
sur une varmap v, alors f' est interprétable sur (Node_vm v v'), avec v' telle que
si i est le chemin d'une fonction de la varmap v, alors i est aussi celui de sa dérivée
dans la varmap v'.
Du coup, le principe est d'ajouter à chaque variable de f un pas vers la gauche,
pour interpréter la fonction obtenue dans la même varmap que sa dérivée.
On définira alors la fonction de dérivation uniquement sur de telles fonctions : pour
dériver une variable, on changera tout simplement son premier pas en un pas vers la droite.
 *)

Fixpoint gauchir (f : fonction) : fonction := match f with
| Var v => Var (Left_idx v)
| Oppose g => Oppose (gauchir g)
| Inverse g => Inverse (gauchir g)
| Plus g h => Plus (gauchir g) (gauchir h)
| Fois g h => Fois (gauchir g) (gauchir h)
| Compo g h => Compo (gauchir g) (gauchir h)
| Puiss g n => Puiss (gauchir g) n
| e => e
end.

(* gauchir ajoute en tête de chaque chemin (représentant une variable) un
pas vers la gauche. *)

(* On voudrait démontrer que :

Theorem gauchir_correcte : forall f v bidon_f bidon_v,
interp v f = interp (Node_vm bidon_f v bidon_v) (gauchir f).

 Problème : si un chemin est inexistant dans la varmap v, et si on transportait dans
les évaluations la variable non trouvée, alors le théorème serait faux.

*)

Theorem gauchir_correcte : forall f v bidon_f bidon_v,
interp v f = interp (Node_vm bidon_f v bidon_v) (gauchir f).
induction f ; trivial.

(* oppose *)
intros.
simpl.
rewrite (IHf v bidon_f bidon_v).
trivial.

(* inverse *)
intros.
simpl.
rewrite (IHf v bidon_f bidon_v).
trivial.

(* plus *)
intros.
simpl.
rewrite (IHf1 v bidon_f bidon_v).
rewrite (IHf2 v bidon_f bidon_v).
trivial.

(* fois *)
intros.
simpl.
rewrite (IHf1 v bidon_f bidon_v).
rewrite (IHf2 v bidon_f bidon_v).
trivial.

(* compo *)
intros.
simpl.
rewrite (IHf1 v bidon_f bidon_v).
rewrite (IHf2 v bidon_f bidon_v).
trivial.

(* puiss *)
intros.
simpl.
rewrite (IHf v bidon_f bidon_v).
trivial.

Qed.


Fixpoint derivg  (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 (derivg g)
| Inverse g => Oppose (Sur (derivg g) (Fois g g))
| Plus g h => Plus (derivg g) (derivg h)
| Fois g h => Plus (Fois (derivg g) h) (Fois g (derivg h))
| Compo g h => Fois (Compo (derivg g) h) (derivg h)
| Puiss _ O => Const 0
| Puiss g (S n) => Fois (Fois (Const (INR (S n))) (derivg g)) (Puiss g n)
| Var (Left_idx i) => Var (Right_idx i)
| Var v => Var v
end.
(* La fonction n'est pas spécifiée pour des fonctions contenant des variables
de chemin vide ou dont le premier pas est à droite. *)

Print derivg.

Definition deriv f := derivg (gauchir f).

Hint Unfold gauchir.
Hint Unfold derivg.
Hint Unfold deriv.


(* Et voilà l'algorithme de dérivation formelle. *)


(* Et maintenant, voilà la dérivabilité formelle. On a donc besoin d'une varmap qui pour chaque fonction
associe son domaine de dérivabilité.

Si une variable ne correspond à aucun prédicat de dérivabilité, on
considère que c'est False. En effet, il s'agit de la plus faible condition
suffisante de dérivabilité dont on dispose a priori.
 *)

(* La dérivabilité dépend d'une interprétation w des variables. Exemple :
h/h est dérivable, mais si h s'annule... *)

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

Hint Constructors derivable.

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

Theorem derivable_sur : forall (v : varmap (R->Prop)) (f g : fonction) (w : varmap (R->R)) (x : R),
  derivable v w f x -> derivable v w g x -> interp w g x <> 0 ->
  derivable v w (Sur f g) x.
intros.
unfold Sur.
eauto.
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
 | |- context k [fct_cte ?c ?x] =>
   change (fct_cte c x) with c ; unfold_fct
 | |- context k [id ?x] =>
   change (id x) with x ; unfold_fct 
 | _ => idtac
end.

(* Voici le théorème de dérivation.*)

Theorem deriv_correcte : forall (f : fonction) (w w' : varmap (R -> R))  (v : varmap (R -> Prop)) (x : R) ,
derivable v w f x ->
(forall (i:index), forall x : R, varmap_find (fun _=>False) i v x -> derivable_pt_lim (interp w (Var i)) x (interp w' (Var i) x)) ->
forall (bidon_fonct : R -> R),
derivable_pt_lim (interp w f) x (interp (Node_vm bidon_fonct w w') (deriv f) x).
Proof.
intros f w w' v.
generalize f ; clear f.
generalize w ; clear w.
generalize w' ; clear w'.
induction f.

(* Constante *)
simpl.
intros.
intros eps Heps.
exists (mkposreal eps Heps).
intros.
unfold_fct.
rewrite Rminus_0_r.
rewrite Rminus_diag_eq.
unfold Rdiv.
rewrite Rmult_0_l.
rewrite Rabs_R0.
assumption.
reflexivity.

(* Cas de l'identite. *)
simpl.
intros.
intros eps Heps.
exists (mkposreal eps Heps).
intros.
unfold_fct.
unfold Rminus.
rewrite (Rplus_comm (x + h)).
rewrite <- Rplus_assoc.
rewrite Rplus_opp_l.
rewrite Rplus_0_l.
unfold Rdiv.
rewrite Rinv_r.
rewrite Rplus_opp_r.
rewrite Rabs_R0.
assumption.
assumption.

(* Cas de l'exponentielle, du sinus, du cosinus. *)
intros ; apply derivable_pt_lim_exp.
intros ; apply derivable_pt_lim_sin.
intros ; simpl ; unfold_fct ; apply derivable_pt_lim_cos.

(* Cas du logarithme *)
intros.
simpl.
unfold_fct.
apply derivable_pt_lim_ln.
inversion H.
apply H1.

(* Cas de la valeur absolue *)
intros.
inversion H.
subst.
unfold_fct.
simpl.
unfold_fct.
destruct (Rdichotomy _ _ H1).
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.
simpl.
unfold_fct.
apply derivable_pt_lim_sqrt.
inversion H.
auto.

(* Cas de l'opposé *)

intros.
unfold deriv ; unfold gauchir ; fold gauchir ; unfold derivg ; fold derivg.
change (derivg  (gauchir f)) with  (deriv f).
unfold interp ; fold interp.
unfold opp_fct at 2.
apply derivable_pt_lim_opp.
apply IHf.
inversion H.
assumption.
assumption.

(* Cas de l'inverse *)
intros.
unfold deriv ; unfold gauchir ; fold gauchir ; unfold derivg ; fold derivg.
change (derivg (gauchir f)) with (deriv f).
unfold interp ; fold interp.
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 w f) x 0 (interp (Node_vm bidon_fonct w w') (deriv f) x)
(derivable_pt_lim_const 1 x)
).
intro Hinv.
generalize (IHf _ H2 H0 bidon_fonct).
intro Hf.
generalize (Hinv Hf H3).
unfold derivable_pt_lim.
intros.
destruct (H1 eps).
assumption.
exists x0.
intros.
unfold Sur ; unfold interp ; fold interp.
rewrite <- gauchir_correcte.
generalize (H5 _ H6 H7).
unfold_fct.
rewrite <- (Rmult_1_l (/ interp w f (x+h))).
rewrite <- (Rmult_1_l (/ interp w 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. *)
intros.
unfold deriv ; unfold gauchir ; fold gauchir ; unfold derivg ; fold derivg.
change (derivg  (gauchir f1)) with  (deriv f1).
change (derivg  (gauchir f2)) with  (deriv f2).
unfold interp ; fold interp.
unfold_fct.
inversion H.
subst.
apply derivable_pt_lim_plus ; auto.

(* Cas du fois. *)
intros.
unfold deriv ; unfold gauchir ; fold gauchir ; unfold derivg ; fold derivg.
change (derivg  (gauchir f1)) with  (deriv f1).
change (derivg  (gauchir f2)) with  (deriv f2).
unfold interp ; fold interp.
unfold_fct.
inversion H.
subst.
rewrite <- gauchir_correcte.
rewrite <- gauchir_correcte.
apply derivable_pt_lim_mult ; auto.

(* Cas de  la composee. *)
intros.
unfold deriv ; unfold gauchir ; fold gauchir ; unfold derivg ; fold derivg.
change (derivg  (gauchir f1)) with  (deriv f1).
change (derivg  (gauchir f2)) with  (deriv f2).
unfold interp ; fold interp.
unfold_fct.
inversion H.
subst.
rewrite <- gauchir_correcte.
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)  *)
intros.
assert (forall n : nat, 
 interp w (Puiss f n) = comp (fun x => pow x n) (interp w 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. *)
generalize H.
case n.
simpl.
intros.
change (fun _:R => 1) with (fct_cte 1).
unfold_fct.
apply derivable_pt_lim_const.
intros.
unfold deriv ; unfold gauchir ; fold gauchir ; unfold derivg ; fold derivg.
change (derivg (gauchir f)) with (deriv f).
rewrite H1.
unfold interp.
fold interp.
unfold_fct.
unfold fct_cte.
rewrite <- gauchir_correcte.
rewrite (Rmult_comm (INR (S n0) * interp (Node_vm bidon_fonct w w') (deriv f) x)).
rewrite <- Rmult_assoc.
inversion_clear H2.
apply derivable_pt_lim_comp ; auto.
rewrite Rmult_comm.
apply (derivable_pt_lim_pow (interp w f x) (S n0)).

(* Cas de la variable. *)
unfold deriv ; unfold gauchir ; unfold derivg.
intros.
unfold interp at 2.
change (varmap_find (fct_cte 0) (Right_idx i) (Node_vm bidon_fonct w w'))
with (varmap_find (fct_cte 0) i w').
change (varmap_find (fct_cte 0) i w')
with (interp w' (Var i)).
apply H0.
inversion H.
assumption.
Qed.

Hint Resolve deriv_correcte.

(* LTAC *)


(* Ajout d'un objet à une varmap. *)

(*
Fixpoint gauche_plus_grand (U : Type) (g d : varmap U) {struct g} : bool :=
match g with
| Empty_vm => false
| Node_vm _ g2 _ =>
match d with
| Empty_vm => true
| Node_vm _ d2 _ => gauche_plus_grand U g2 d2
end end.
Implicit Arguments gauche_plus_grand.

Fixpoint complet (U : Type) (v : varmap U) {struct v} : bool :=
match v with
| Empty_vm => true
| Node_vm _ g d => if complet U g then complet U d else false
end.
Implicit Arguments complet.

Print complet.
Print gauche_plus_grand.

Fixpoint ajouter (U : Type) (o : U) (v : varmap U) {struct v} : varmap U :=
match v with
| Empty_vm => Node_vm o (Empty_vm _) (Empty_vm _)
| Node_vm r g d =>
if complet g
then
 if complet d 
 then
  if gauche_plus_grand g d 
  then Node_vm r g (ajouter U o d)
  else Node_vm r (ajouter U o g) d
 else Node_vm r g (ajouter U o d)
else Node_vm r (ajouter U o g) d
end.
Implicit Arguments ajouter.

Eval compute in 
ajouter True (ajouter False (Node_vm True (Empty_vm _) (Empty_vm _))).
*)

Ltac gauche_plus_grand g d :=
match constr:g with
| Empty_vm _ => constr:False
| Node_vm _ ?g2 _ =>
match constr:d with
| Empty_vm _ => constr:True
| Node_vm _ ?d2 _ => gauche_plus_grand g2 d2
end end.

Ltac complet v :=
match constr:v with
| Empty_vm _ => constr:True
| Node_vm _ ?g ?d => 
match complet g with
| True => complet d
| False => constr:False
end end.

Ltac ajouter o v :=
match constr:v with
| Empty_vm _ => constr:(Node_vm o (Empty_vm _) (Empty_vm _))
| Node_vm ?r ?g ?d =>
match complet g with
| True => 
match complet d  with
| True =>
match gauche_plus_grand g d with
| True => let d' := ajouter o d in constr:(Node_vm r g d')
| False => let g' := ajouter o g in constr:(Node_vm r g' d)
end
| False => let d' := ajouter o d in constr:(Node_vm r g d')
end 
| False => let g' := ajouter o g in constr:(Node_vm r g' d)
end
end.

Ltac essai_ajouter o v :=
let w := ajouter o v in
generalize (refl_equal w). (* en gros, c'est un "print" *)

(* ça marche : 
Theorem bidon : False.
essai_ajouter True (Node_vm True (Node_vm False (Empty_vm _) (Empty_vm _)) (Empty_vm _)).
*)

(* Ajout sans doublon *)
Ltac ajouter_sans_doublon o v :=
match constr:v with
| Empty_vm _ => constr:(Node_vm o (Empty_vm _) (Empty_vm _))
| Node_vm o _ _ => constr:v
| Node_vm ?r ?g ?d =>
match complet g with
| True => 
match complet d  with
| True =>
match gauche_plus_grand g d with
| True => let d' := ajouter_sans_doublon o d in constr:(Node_vm r g d')
| False => let g' := ajouter_sans_doublon o g in constr:(Node_vm r g' d)
end
| False => let d' := ajouter_sans_doublon o d in constr:(Node_vm r g d')
end 
| False => let g' := ajouter_sans_doublon o g in constr:(Node_vm r g' d)
end
end.

Ltac essai_ajout_sans_doublon o1 o2 o3 v :=
let w := ajouter_sans_doublon o1 v in
let x := ajouter_sans_doublon o2 w in
let y := ajouter_sans_doublon o3 x in
generalize (refl_equal y).

(* ça marche :
Theorem bidon : False.
essai_ajout_sans_doublon True False True (Empty_vm Prop).
*)

(* Complétion de la varmap v suivant la fonction f, sans doublons. *)

Ltac completer v f :=
match constr:f with
| (comp ?f1 ?f2) => let w := completer v f1 in  completer w f2
| (plus_fct ?f1 ?f2) => let w := completer v f1 in  completer w f2
| (minus_fct ?f1 ?f2) => let w := completer v f1 in  completer w f2
| (mult_fct ?f1 ?f2) => let w := completer v f1 in  completer w f2
| (pow_fct ?f ?m) => completer v f
| (div_fct ?f1 ?f2) => let w := completer v f1 in  completer w f2
| (inv_fct ?f) => completer v f
| (opp_fct ?f) => completer v f
| exp => constr:v
| sin => constr:v
| cos => constr:v
| ln => constr:v
| Rabs => constr:v
| sqrt => constr:v
| (fun x => x) => constr:v
| id => constr:v
| (fun _ => ?x) => constr:v
| fct_cte ?x => constr:v
| (fun x => ?f (?g x)) => let w := completer v f in completer w g (* eta-conversion avec composition *)
| (fun x => ?f x) => completer v f (* eta-conversion simple *)
| _ => ajouter_sans_doublon f v (* autres cas *)
end.

Ltac essai_completion v f :=
let w := completer v f in
generalize (refl_equal w).

(* ça marche :
Theorem bidon : False.
essai_completion (Empty_vm (R->R)) (plus_fct (fun x=>x) (minus_fct (fun x=>cos x) (fun x=>x+0))).
*)

(* Inversion de la fonction à varmap fixée. *)

(* Recherche d'une fonction à partir d'une varmap et construction du chemin. *)

Ltac trouver f v := 
match constr:v with
| Node_vm f _ _ => constr:End_idx
| Node_vm _ ?g _ => let i := trouver f g in constr:(Left_idx i)
| Node_vm _ _ ?d => let i := trouver f d in constr:(Right_idx i)
| _ => fail "Une fonction n'a pu être trouvée dans la varmap. Complétez d'abord
la varmap avant d'inverser la fonction."
end.

Ltac essai_trouver f v :=
let i := trouver f v in
generalize (refl_equal i).

(* ça marche :
Theorem bidon : False.
essai_trouver False (Node_vm True (Empty_vm _) (Node_vm False (Empty_vm _) (Empty_vm _))).
*)

(* Inversion d'une fonction suivant une varmap fixée : *)

Ltac inversion_fonction v f :=
 match constr:f with
  | (comp ?f1 ?f2) => 
     let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Compo g1 g2)
  | (plus_fct ?f1 ?f2) => 
     let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Plus g1 g2)
  | (minus_fct ?f1 ?f2) => 
     let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Moins g1 g2)
  | (mult_fct ?f1 ?f2) => 
     let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Fois g1 g2)
  | (pow_fct ?f ?m) =>
     let g := inversion_fonction v f in constr:(Puiss g m)
  | (div_fct ?f1 ?f2) => 
     let g1 := inversion_fonction v f1 with g2 := inversion_fonction v f2 in constr:(Sur g1 g2)
  | (inv_fct ?f) =>
     let g := inversion_fonction v f in constr:(Inverse g)    
  | (opp_fct ?f) => let g := inversion_fonction v 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 (?g x)) => 
let k := constr:(comp f g) in inversion_fonction v k (* eta-conversion avec composition *)
  | (fun x => ?f x) => inversion_fonction v f (* eta-conversion simple *)
  | _ => let i := trouver f v in constr:(Var i) (* autres cas *)
  | _ => fail "Une fonction n'a pu être trouvée dans la varmap. Complétez d'abord
la varmap avant d'inverser la fonction."
end.

Ltac essai_inversion  v f := 
let h := inversion_fonction v f in
generalize (refl_equal h).

(* L'enchaînement.
(remarque : on aurait pu aussi écrire une tactique qui ferait les deux à la fois au lieu
d'enchaîner les appels completer et inversion_fonction. Cf infra) *)

Print pair.

(* On a besoin d'un produit dans Type *)
Inductive prod2 (A B : Type) : Type :=
| pair2 : A -> B -> prod2 A B.
Implicit Arguments pair2.

Ltac enchainer v f :=
let w := completer v f in
let h := inversion_fonction w f in
constr:(pair2 w h).

Ltac essai_enchainer v f :=
let k := enchainer v f in
generalize (refl_equal k).

(* ça marche :
Theorem bidon : False.
essai_enchainer (Empty_vm (R->R)) (plus_fct (fun x => x) (fun x => x+0)).
*)

(* en revanche, l'eta-conversion ne marche pas toujours : *)
Ltac eta_contraction f := match f with
| (fun x => ?g x) => eta_contraction g
| _ => constr:f
end.

Ltac essai_eta f :=
let h := eta_contraction f in
generalize (refl_equal h).

(* en effet, ça ne marche pas toujours :
Theorem bidon : False.
essai_eta (fun x => cos x).
essai_eta (fun x => (plus_fct cos sin) x).
*)

Print pair2.

(* Donc, voici une tactique qui fait les deux choses en même temps : *)

Ltac deux_en_un v f :=
 match constr:f with
  | (comp ?f1 ?f2) => 
     let k1 := deux_en_un v f1 in
     match constr:k1 with
     | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in
     match constr:k2 with
     | pair2 ?x ?g2 => constr:(pair2 x (Compo g1 g2))
    end end
  | (plus_fct ?f1 ?f2) =>   
     let k1 := deux_en_un v f1 in
     match constr:k1 with
     | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in
     match constr:k2 with
     | pair2 ?x ?g2 => constr:(pair2 x (Plus g1 g2))
    end end
  | (minus_fct ?f1 ?f2) => 
     let k1 := deux_en_un v f1 in
     match constr:k1 with
     | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in
     match constr:k2 with
     | pair2 ?x ?g2 => constr:(pair2 x (Moins g1 g2))
    end end
  | (mult_fct ?f1 ?f2) => 
     let k1 := deux_en_un v f1 in
     match constr:k1 with
     | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in
     match constr:k2 with
     | pair2 ?x ?g2 => constr:(pair2 x (Fois g1 g2))
    end end
  | (pow_fct ?f1 ?m) =>
     let k1 := deux_en_un v f1 in
     match constr:k1 with
     | pair2 ?w ?g1 => constr:(pair2 w (Puiss g1 m))
    end
  | (div_fct ?f1 ?f2) => 
     let k1 := deux_en_un v f1 in
     match constr:k1 with
     | pair2 ?w ?g1 => let k2 := deux_en_un w f2 in
     match constr:k2 with
     | pair2 ?x ?g2 => constr:(pair2 x (Sur g1 g2))
    end end
  | (inv_fct ?f1) =>
     let k1 := deux_en_un v f1 in
     match constr:k1 with
     | pair2 ?w ?g1 => constr:(pair2 w (Inverse g1))
    end
  | (opp_fct ?f1) => 
     let k1 := deux_en_un v f1 in
     match constr:k1 with
     | pair2 ?w ?g1 => constr:(pair2 w (Oppose g1))
    end
  | exp => constr:(pair2 v Exp)
  | sin => constr:(pair2 v Sin)
  | cos => constr:(pair2 v Cos)
  | ln => constr:(pair2 v Log)
  | Rabs => constr:(pair2 v Valeur_absolue)
  | sqrt => constr:(pair2 v Racine)
  | (fun x => x) => constr:(pair2 v Id)
  | id => constr:(pair2 v Id)
  | (fun _ => ?x) => constr:(pair2 v (Const x))
  | fct_cte ?x => constr:(pair2 v (Const x))
  | (fun x => ?f (?g x)) =>
let k := constr:(comp f g) in deux_en_un v k (* eta-conversion avec composition *)
  | (fun x => ?f x) => deux_en_un v f (* eta-conversion simple *)
  | _ => (* sous-optimal : tenter d'ajouter f sans doublon puis séparément trouver son index
dans la varmap obtenue *)
let w := ajouter_sans_doublon f v in
let i := trouver f w in constr:(pair2 w (Var i))
end.

Ltac essai_deux_en_un v f :=
let k := deux_en_un v f in
generalize (refl_equal k).

(* ça marche :
Theorem bidon : False.
essai_deux_en_un (Empty_vm (R->R)) (plus_fct (fun x => x) (fun x => x + 0)).
*)

(* Maintenant, le plus dur. Heureusement, mon théorème de correction introduit les variables 
universellement quantifiées dans le bon ordre : varmap initiale, puis fonction. *)

Ltac derive v f :=
  let f1 := eta_contraction f in
  let w := completer v f in
  let f0 := inversion_fonction w f1 in (
  generalize (deriv_correcte f0 w) ;
  unfold Moins ; unfold Sur ; simpl interp ; unfold_fct
).

(* les résultats sont non négligeables, mais ça ne va pas très loin non plus.
Theorem bidon : False.
derive (Empty_vm (R->R)) (plus_fct (minus_fct (fun x => x) (fun x => cos x)) (plus_fct (fun x => x+0) (fun x => cos (x + 0)))).
*)