Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 755 insertions, 430 deletions

diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v
index 4f944995c..eee3f2daf 100644
--- a/theories/Reals/Ranalysis.v
+++ b/theories/Reals/Ranalysis.v
@@ -8,10 +8,10 @@
  
 (*i $Id$ i*)
 
-Require Rbase.
-Require Rfunctions.
-Require Rtrigo.
-Require SeqSeries.
+Require Import Rbase.
+Require Import Rfunctions.
+Require Import Rtrigo.
+Require Import SeqSeries.
 Require Export Ranalysis1.
 Require Export Ranalysis2.
 Require Export Ranalysis3.
@@ -27,451 +27,776 @@ Require Export Rgeom.
 Require Export RList.
 Require Export Sqrt_reg.
 Require Export Ranalysis4.
-Require Export Rpower.
-V7only [Import R_scope.]. Open Local Scope R_scope.
+Require Export Rpower. Open Local Scope R_scope.
 
 Axiom AppVar : R.
 
 (**********)
-Recursive Tactic Definition IntroHypG trm :=
-Match trm With
-|[(plus_fct ?1 ?2)] -> 
- (Match Context With
- |[|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2
- |[|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2
- | _ -> Idtac)
-|[(minus_fct ?1 ?2)] -> 
- (Match Context With
- |[|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2
- |[|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2
- | _ -> Idtac)
-|[(mult_fct ?1 ?2)] ->
- (Match Context With
- |[|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2
- |[|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2
- | _ -> Idtac)
-|[(div_fct ?1 ?2)] -> Let aux = ?2 In
- (Match Context With
- |[_:(x0:R)``(aux x0)<>0``|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2
- |[_:(x0:R)``(aux x0)<>0``|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2
- |[|-(derivable ?)] -> Cut ((x0:R)``(aux x0)<>0``); [Intro; IntroHypG ?1; IntroHypG ?2 | Try Assumption]
- |[|-(continuity ?)] -> Cut ((x0:R)``(aux x0)<>0``); [Intro; IntroHypG ?1; IntroHypG ?2 | Try Assumption]
- | _ -> Idtac)
-|[(comp ?1 ?2)] -> 
- (Match Context With
- |[|-(derivable ?)] -> IntroHypG ?1; IntroHypG ?2
- |[|-(continuity ?)] -> IntroHypG ?1; IntroHypG ?2
- | _ -> Idtac)
-|[(opp_fct ?1)] -> 
- (Match Context With
- |[|-(derivable ?)] -> IntroHypG ?1
- |[|-(continuity ?)] -> IntroHypG ?1
- | _ -> Idtac)
-|[(inv_fct ?1)] -> Let aux = ?1 In
- (Match Context With
- |[_:(x0:R)``(aux x0)<>0``|-(derivable ?)] -> IntroHypG ?1
- |[_:(x0:R)``(aux x0)<>0``|-(continuity ?)] -> IntroHypG ?1
- |[|-(derivable ?)] -> Cut ((x0:R)``(aux x0)<>0``); [Intro; IntroHypG ?1 | Try Assumption]
- |[|-(continuity ?)] -> Cut ((x0:R)``(aux x0)<>0``); [Intro; IntroHypG ?1| Try Assumption]
- | _ -> Idtac)
-|[cos] -> Idtac
-|[sin] -> Idtac
-|[cosh] -> Idtac
-|[sinh] -> Idtac
-|[exp] -> Idtac
-|[Rsqr] -> Idtac
-|[sqrt] -> Idtac
-|[id] -> Idtac
-|[(fct_cte ?)] -> Idtac
-|[(pow_fct ?)] -> Idtac
-|[Rabsolu] -> Idtac
-|[?1] -> Let p = ?1 In
- (Match Context With
- |[_:(derivable p)|- ?] -> Idtac
- |[|-(derivable p)] -> Idtac
- |[|-(derivable ?)] -> Cut True -> (derivable p); [Intro HYPPD; Cut (derivable p); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac]
- | [_:(continuity p)|- ?] -> Idtac
- |[|-(continuity p)] -> Idtac
- |[|-(continuity ?)] -> Cut True -> (continuity p); [Intro HYPPD; Cut (continuity p); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac]
- | _ -> Idtac).
+Ltac intro_hyp_glob trm :=
+  match constr:trm with
+  | (?X1 + ?X2)%F =>
+      match goal with
+      |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
+      |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
+      | _ => idtac
+      end
+  | (?X1 - ?X2)%F =>
+      match goal with
+      |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
+      |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
+      | _ => idtac
+      end
+  | (?X1 * ?X2)%F =>
+      match goal with
+      |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
+      |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
+      | _ => idtac
+      end
+  | (?X1 / ?X2)%F =>
+      let aux := constr:X2 in
+      match goal with
+      | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
+          intro_hyp_glob X1; intro_hyp_glob X2
+      | _:(forall x0:R, aux x0 <> 0) |- (continuity _) =>
+          intro_hyp_glob X1; intro_hyp_glob X2
+      |  |- (derivable _) =>
+          cut (forall x0:R, aux x0 <> 0);
+           [ intro; intro_hyp_glob X1; intro_hyp_glob X2 | try assumption ]
+      |  |- (continuity _) =>
+          cut (forall x0:R, aux x0 <> 0);
+           [ intro; intro_hyp_glob X1; intro_hyp_glob X2 | try assumption ]
+      | _ => idtac
+      end
+  | (comp ?X1 ?X2) =>
+      match goal with
+      |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
+      |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
+      | _ => idtac
+      end
+  | (- ?X1)%F =>
+      match goal with
+      |  |- (derivable _) => intro_hyp_glob X1
+      |  |- (continuity _) => intro_hyp_glob X1
+      | _ => idtac
+      end
+  | (/ ?X1)%F =>
+      let aux := constr:X1 in
+      match goal with
+      | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
+          intro_hyp_glob X1
+      | _:(forall x0:R, aux x0 <> 0) |- (continuity _) => 
+      intro_hyp_glob X1
+      |  |- (derivable _) =>
+          cut (forall x0:R, aux x0 <> 0);
+           [ intro; intro_hyp_glob X1 | try assumption ]
+      |  |- (continuity _) =>
+          cut (forall x0:R, aux x0 <> 0);
+           [ intro; intro_hyp_glob X1 | try assumption ]
+      | _ => idtac
+      end
+  | cos => idtac
+  | sin => idtac
+  | cosh => idtac
+  | sinh => idtac
+  | exp => idtac
+  | Rsqr => idtac
+  | sqrt => idtac
+  | id => idtac
+  | (fct_cte _) => idtac
+  | (pow_fct _) => idtac
+  | Rabs => idtac
+  | ?X1 =>
+      let p := constr:X1 in
+      match goal with
+      | _:(derivable p) |- _ => idtac
+      |  |- (derivable p) => idtac
+      |  |- (derivable _) =>
+          cut (True -> derivable p);
+           [ intro HYPPD; cut (derivable p);
+              [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
+           | idtac ]
+      | _:(continuity p) |- _ => idtac
+      |  |- (continuity p) => idtac
+      |  |- (continuity _) =>
+          cut (True -> continuity p);
+           [ intro HYPPD; cut (continuity p);
+              [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
+           | idtac ]
+      | _ => idtac
+      end
+  end.
 
 (**********)
-Recursive Tactic Definition IntroHypL trm pt :=
-Match trm With
-|[(plus_fct ?1 ?2)] -> 
- (Match Context With
- |[|-(derivable_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- |[|-(continuity_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- |[|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- | _ -> Idtac)
-|[(minus_fct ?1 ?2)] -> 
- (Match Context With
- |[|-(derivable_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- |[|-(continuity_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- |[|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- | _ -> Idtac)
-|[(mult_fct ?1 ?2)] ->
- (Match Context With
- |[|-(derivable_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- |[|-(continuity_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- |[|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- | _ -> Idtac)
-|[(div_fct ?1 ?2)] -> Let aux = ?2 In
- (Match Context With
- |[_:``(aux pt)<>0``|-(derivable_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- |[_:``(aux pt)<>0``|-(continuity_pt ? ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- |[_:``(aux pt)<>0``|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt; IntroHypL ?2 pt
- |[id:(x0:R)``(aux x0)<>0``|-(derivable_pt ? ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt; IntroHypL ?2 pt
- |[id:(x0:R)``(aux x0)<>0``|-(continuity_pt ? ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt; IntroHypL ?2 pt
- |[id:(x0:R)``(aux x0)<>0``|-(eqT ? (derive_pt ? ? ?) ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt; IntroHypL ?2 pt
- |[|-(derivable_pt ? ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt; IntroHypL ?2 pt | Try Assumption]
- |[|-(continuity_pt ? ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt; IntroHypL ?2 pt | Try Assumption]
- |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt; IntroHypL ?2 pt | Try Assumption]
- | _ -> Idtac)
-|[(comp ?1 ?2)] -> 
- (Match Context With
- |[|-(derivable_pt ? ?)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In IntroHypL ?1 pt_f1; IntroHypL ?2 pt
- |[|-(continuity_pt ? ?)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In IntroHypL ?1 pt_f1; IntroHypL ?2 pt
- |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In IntroHypL ?1 pt_f1; IntroHypL ?2 pt
- | _ -> Idtac)
-|[(opp_fct ?1)] -> 
- (Match Context With
- |[|-(derivable_pt ? ?)] -> IntroHypL ?1 pt
- |[|-(continuity_pt ? ?)] -> IntroHypL ?1 pt
- |[|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt
- | _ -> Idtac)
-|[(inv_fct ?1)] -> Let aux = ?1 In
- (Match Context With
- |[_:``(aux pt)<>0``|-(derivable_pt ? ?)] -> IntroHypL ?1 pt
- |[_:``(aux pt)<>0``|-(continuity_pt ? ?)] -> IntroHypL ?1 pt
- |[_:``(aux pt)<>0``|-(eqT ? (derive_pt ? ? ?) ?)] -> IntroHypL ?1 pt
- |[id:(x0:R)``(aux x0)<>0``|-(derivable_pt ? ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt
- |[id:(x0:R)``(aux x0)<>0``|-(continuity_pt ? ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt
- |[id:(x0:R)``(aux x0)<>0``|-(eqT ? (derive_pt ? ? ?) ?)] -> Generalize (id pt); Intro; IntroHypL ?1 pt
- |[|-(derivable_pt ? ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt | Try Assumption]
- |[|-(continuity_pt ? ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt| Try Assumption]
- |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut ``(aux pt)<>0``; [Intro; IntroHypL ?1 pt | Try Assumption]
- | _ -> Idtac)
-|[cos] -> Idtac
-|[sin] -> Idtac
-|[cosh] -> Idtac
-|[sinh] -> Idtac
-|[exp] -> Idtac
-|[Rsqr] -> Idtac
-|[id] -> Idtac
-|[(fct_cte ?)] -> Idtac
-|[(pow_fct ?)] -> Idtac
-|[sqrt] ->
- (Match Context With
- |[|-(derivable_pt ? ?)] -> Cut ``0<pt``; [Intro | Try Assumption]
- |[|-(continuity_pt ? ?)] -> Cut ``0<=pt``; [Intro | Try Assumption]
- |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut ``0<pt``; [Intro | Try Assumption]
- | _ -> Idtac)
-|[Rabsolu] ->
- (Match Context With
- |[|-(derivable_pt ? ?)] -> Cut ``pt<>0``; [Intro | Try Assumption]
- | _ -> Idtac)
-|[?1] -> Let p = ?1 In
- (Match Context With
- |[_:(derivable_pt p pt)|- ?] -> Idtac
- |[|-(derivable_pt p pt)] -> Idtac
- |[|-(derivable_pt ? ?)] -> Cut True -> (derivable_pt p pt); [Intro HYPPD; Cut (derivable_pt p pt); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac]
- |[_:(continuity_pt p pt)|- ?] -> Idtac
- |[|-(continuity_pt p pt)] -> Idtac
- |[|-(continuity_pt ? ?)] -> Cut True -> (continuity_pt p pt); [Intro HYPPD; Cut (continuity_pt p pt); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac]
- |[|-(eqT ? (derive_pt ? ? ?) ?)] -> Cut True -> (derivable_pt p pt); [Intro HYPPD; Cut (derivable_pt p pt); [Intro; Clear HYPPD | Apply HYPPD; Clear HYPPD; Trivial] | Idtac]
- | _ -> Idtac).
+Ltac intro_hyp_pt trm pt :=
+  match constr:trm with
+  | (?X1 + ?X2)%F =>
+      match goal with
+      |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      |  |- (continuity_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      |  |- (derive_pt _ _ _ = _) =>
+          intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      | _ => idtac
+      end
+  | (?X1 - ?X2)%F =>
+      match goal with
+      |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      |  |- (continuity_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      |  |- (derive_pt _ _ _ = _) =>
+          intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      | _ => idtac
+      end
+  | (?X1 * ?X2)%F =>
+      match goal with
+      |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      |  |- (continuity_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      |  |- (derive_pt _ _ _ = _) =>
+          intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      | _ => idtac
+      end
+  | (?X1 / ?X2)%F =>
+      let aux := constr:X2 in
+      match goal with
+      | _:(aux pt <> 0) |- (derivable_pt _ _) =>
+          intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      | _:(aux pt <> 0) |- (continuity_pt _ _) =>
+          intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      | _:(aux pt <> 0) |- (derive_pt _ _ _ = _) =>
+          intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      | id:(forall x0:R, aux x0 <> 0) |- (derivable_pt _ _) =>
+          generalize (id pt); intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      | id:(forall x0:R, aux x0 <> 0) |- (continuity_pt _ _) =>
+          generalize (id pt); intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      | id:(forall x0:R, aux x0 <> 0) |- (derive_pt _ _ _ = _) =>
+          generalize (id pt); intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
+      |  |- (derivable_pt _ _) =>
+          cut (aux pt <> 0);
+           [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
+      |  |- (continuity_pt _ _) =>
+          cut (aux pt <> 0);
+           [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
+      |  |- (derive_pt _ _ _ = _) =>
+          cut (aux pt <> 0);
+           [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
+      | _ => idtac
+      end
+  | (comp ?X1 ?X2) =>
+      match goal with
+      |  |- (derivable_pt _ _) =>
+          let pt_f1 := eval cbv beta in (X2 pt) in
+          (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt)
+      |  |- (continuity_pt _ _) =>
+          let pt_f1 := eval cbv beta in (X2 pt) in
+          (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt)
+      |  |- (derive_pt _ _ _ = _) =>
+          let pt_f1 := eval cbv beta in (X2 pt) in
+          (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt)
+      | _ => idtac
+      end
+  | (- ?X1)%F =>
+      match goal with
+      |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt
+      |  |- (continuity_pt _ _) => intro_hyp_pt X1 pt
+      |  |- (derive_pt _ _ _ = _) => intro_hyp_pt X1 pt
+      | _ => idtac
+      end
+  | (/ ?X1)%F =>
+      let aux := constr:X1 in
+      match goal with
+      | _:(aux pt <> 0) |- (derivable_pt _ _) =>
+          intro_hyp_pt X1 pt
+      | _:(aux pt <> 0) |- (continuity_pt _ _) =>
+          intro_hyp_pt X1 pt
+      | _:(aux pt <> 0) |- (derive_pt _ _ _ = _) =>
+          intro_hyp_pt X1 pt
+      | id:(forall x0:R, aux x0 <> 0) |- (derivable_pt _ _) =>
+          generalize (id pt); intro; intro_hyp_pt X1 pt
+      | id:(forall x0:R, aux x0 <> 0) |- (continuity_pt _ _) =>
+          generalize (id pt); intro; intro_hyp_pt X1 pt
+      | id:(forall x0:R, aux x0 <> 0) |- (derive_pt _ _ _ = _) =>
+          generalize (id pt); intro; intro_hyp_pt X1 pt
+      |  |- (derivable_pt _ _) =>
+          cut (aux pt <> 0); [ intro; intro_hyp_pt X1 pt | try assumption ]
+      |  |- (continuity_pt _ _) =>
+          cut (aux pt <> 0); [ intro; intro_hyp_pt X1 pt | try assumption ]
+      |  |- (derive_pt _ _ _ = _) =>
+          cut (aux pt <> 0); [ intro; intro_hyp_pt X1 pt | try assumption ]
+      | _ => idtac
+      end
+  | cos => idtac
+  | sin => idtac
+  | cosh => idtac
+  | sinh => idtac
+  | exp => idtac
+  | Rsqr => idtac
+  | id => idtac
+  | (fct_cte _) => idtac
+  | (pow_fct _) => idtac
+  | sqrt =>
+      match goal with
+      |  |- (derivable_pt _ _) => cut (0 < pt); [ intro | try assumption ]
+      |  |- (continuity_pt _ _) =>
+          cut (0 <= pt); [ intro | try assumption ]
+      |  |- (derive_pt _ _ _ = _) =>
+          cut (0 < pt); [ intro | try assumption ]
+      | _ => idtac
+      end
+  | Rabs =>
+      match goal with
+      |  |- (derivable_pt _ _) =>
+          cut (pt <> 0); [ intro | try assumption ]
+      | _ => idtac
+      end
+  | ?X1 =>
+      let p := constr:X1 in
+      match goal with
+      | _:(derivable_pt p pt) |- _ => idtac
+      |  |- (derivable_pt p pt) => idtac
+      |  |- (derivable_pt _ _) =>
+          cut (True -> derivable_pt p pt);
+           [ intro HYPPD; cut (derivable_pt p pt);
+              [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
+           | idtac ]
+      | _:(continuity_pt p pt) |- _ => idtac
+      |  |- (continuity_pt p pt) => idtac
+      |  |- (continuity_pt _ _) =>
+          cut (True -> continuity_pt p pt);
+           [ intro HYPPD; cut (continuity_pt p pt);
+              [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
+           | idtac ]
+      |  |- (derive_pt _ _ _ = _) =>
+          cut (True -> derivable_pt p pt);
+           [ intro HYPPD; cut (derivable_pt p pt);
+              [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
+           | idtac ]
+      | _ => idtac
+      end
+  end.
  
 (**********)
-Recursive Tactic Definition IsDiff_pt :=
-Match Context With
- (* fonctions de base *)
- [|-(derivable_pt Rsqr ?)] -> Apply derivable_pt_Rsqr
-|[|-(derivable_pt id ?1)] -> Apply (derivable_pt_id ?1)
-|[|-(derivable_pt (fct_cte ?) ?)] -> Apply derivable_pt_const
-|[|-(derivable_pt sin ?)] -> Apply derivable_pt_sin
-|[|-(derivable_pt cos ?)] -> Apply derivable_pt_cos
-|[|-(derivable_pt sinh ?)] -> Apply derivable_pt_sinh
-|[|-(derivable_pt cosh ?)] -> Apply derivable_pt_cosh
-|[|-(derivable_pt exp ?)] -> Apply derivable_pt_exp
-|[|-(derivable_pt (pow_fct ?) ?)] -> Unfold pow_fct; Apply derivable_pt_pow
-|[|-(derivable_pt sqrt ?1)] -> Apply (derivable_pt_sqrt ?1); Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte pow_fct
-|[|-(derivable_pt Rabsolu ?1)] -> Apply (derivable_pt_Rabsolu ?1); Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte pow_fct
- (* regles de differentiabilite *)
- (* PLUS *)
-|[|-(derivable_pt (plus_fct ?1 ?2) ?3)] -> Apply (derivable_pt_plus ?1 ?2 ?3); IsDiff_pt
- (* MOINS *)
-|[|-(derivable_pt (minus_fct ?1 ?2) ?3)] -> Apply (derivable_pt_minus ?1 ?2 ?3); IsDiff_pt
- (* OPPOSE *)
-|[|-(derivable_pt (opp_fct ?1) ?2)] -> Apply (derivable_pt_opp ?1 ?2); IsDiff_pt
- (* MULTIPLICATION PAR UN SCALAIRE *)
-|[|-(derivable_pt (mult_real_fct ?1 ?2) ?3)] -> Apply (derivable_pt_scal ?2 ?1 ?3); IsDiff_pt
- (* MULTIPLICATION *)
-|[|-(derivable_pt (mult_fct ?1 ?2) ?3)] -> Apply (derivable_pt_mult ?1 ?2 ?3); IsDiff_pt
-  (* DIVISION *)
- |[|-(derivable_pt (div_fct ?1 ?2) ?3)] -> Apply (derivable_pt_div ?1 ?2 ?3); [IsDiff_pt | IsDiff_pt | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp pow_fct id fct_cte]
-  (* INVERSION *)
- |[|-(derivable_pt (inv_fct ?1) ?2)] -> Apply (derivable_pt_inv ?1 ?2); [Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp pow_fct id fct_cte | IsDiff_pt]
- (* COMPOSITION *)
-|[|-(derivable_pt (comp ?1 ?2) ?3)] -> Apply (derivable_pt_comp ?2 ?1 ?3); IsDiff_pt
-|[_:(derivable_pt ?1 ?2)|-(derivable_pt ?1 ?2)] -> Assumption
-|[_:(derivable ?1) |- (derivable_pt ?1 ?2)] -> Cut (derivable ?1); [Intro HypDDPT; Apply HypDDPT | Assumption]
-|[|-True->(derivable_pt ? ?)] -> Intro HypTruE; Clear HypTruE; IsDiff_pt
-| _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct.
+Ltac is_diff_pt :=
+  match goal with
+  |  |- (derivable_pt Rsqr _) =>
+      
+  (* fonctions de base *)
+  apply derivable_pt_Rsqr
+  |  |- (derivable_pt id ?X1) => apply (derivable_pt_id X1)
+  |  |- (derivable_pt (fct_cte _) _) => apply derivable_pt_const
+  |  |- (derivable_pt sin _) => apply derivable_pt_sin
+  |  |- (derivable_pt cos _) => apply derivable_pt_cos
+  |  |- (derivable_pt sinh _) => apply derivable_pt_sinh
+  |  |- (derivable_pt cosh _) => apply derivable_pt_cosh
+  |  |- (derivable_pt exp _) => apply derivable_pt_exp
+  |  |- (derivable_pt (pow_fct _) _) =>
+      unfold pow_fct in |- *; apply derivable_pt_pow
+  |  |- (derivable_pt sqrt ?X1) =>
+      apply (derivable_pt_sqrt X1);
+       assumption ||
+         unfold plus_fct, minus_fct, opp_fct, mult_fct, div_fct, inv_fct,
+          comp, id, fct_cte, pow_fct in |- *
+  |  |- (derivable_pt Rabs ?X1) =>
+      apply (Rderivable_pt_abs X1);
+       assumption ||
+         unfold plus_fct, minus_fct, opp_fct, mult_fct, div_fct, inv_fct,
+          comp, id, fct_cte, pow_fct in |- *
+        (* regles de differentiabilite *)
+        (* PLUS *)
+  |  |- (derivable_pt (?X1 + ?X2) ?X3) =>
+      apply (derivable_pt_plus X1 X2 X3); is_diff_pt
+       (* MOINS *)
+  |  |- (derivable_pt (?X1 - ?X2) ?X3) =>
+      apply (derivable_pt_minus X1 X2 X3); is_diff_pt
+       (* OPPOSE *)
+  |  |- (derivable_pt (- ?X1) ?X2) =>
+      apply (derivable_pt_opp X1 X2);
+       is_diff_pt
+       (* MULTIPLICATION PAR UN SCALAIRE *)
+  |  |- (derivable_pt (mult_real_fct ?X1 ?X2) ?X3) =>
+      apply (derivable_pt_scal X2 X1 X3); is_diff_pt
+       (* MULTIPLICATION *)
+  |  |- (derivable_pt (?X1 * ?X2) ?X3) =>
+      apply (derivable_pt_mult X1 X2 X3); is_diff_pt
+       (* DIVISION *)
+  |  |- (derivable_pt (?X1 / ?X2) ?X3) =>
+      apply (derivable_pt_div X1 X2 X3);
+       [ is_diff_pt
+       | is_diff_pt
+       | try
+          assumption ||
+            unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
+             comp, pow_fct, id, fct_cte in |- * ]
+  |  |- (derivable_pt (/ ?X1) ?X2) =>
+      
+       (* INVERSION *)
+       apply (derivable_pt_inv X1 X2);
+       [ assumption ||
+           unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
+            comp, pow_fct, id, fct_cte in |- *
+       | is_diff_pt ]
+  |  |- (derivable_pt (comp ?X1 ?X2) ?X3) =>
+      
+       (* COMPOSITION *)
+       apply (derivable_pt_comp X2 X1 X3); is_diff_pt
+  | _:(derivable_pt ?X1 ?X2) |- (derivable_pt ?X1 ?X2) =>
+      assumption
+  | _:(derivable ?X1) |- (derivable_pt ?X1 ?X2) =>
+      cut (derivable X1); [ intro HypDDPT; apply HypDDPT | assumption ]
+  |  |- (True -> derivable_pt _ _) =>
+      intro HypTruE; clear HypTruE; is_diff_pt
+  | _ =>
+      try
+       unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
+        fct_cte, comp, pow_fct in |- *
+  end.
 
 (**********)
-Recursive Tactic Definition IsDiff_glob :=
-Match Context With
- (* fonctions de base *)
-  [|-(derivable Rsqr)] -> Apply derivable_Rsqr
- |[|-(derivable id)] -> Apply derivable_id
- |[|-(derivable (fct_cte ?))] -> Apply derivable_const
- |[|-(derivable sin)] -> Apply derivable_sin
- |[|-(derivable cos)] -> Apply derivable_cos
- |[|-(derivable cosh)] -> Apply derivable_cosh
- |[|-(derivable sinh)] -> Apply derivable_sinh
- |[|-(derivable exp)] -> Apply derivable_exp
- |[|-(derivable (pow_fct ?))] -> Unfold pow_fct; Apply derivable_pow
-  (* regles de differentiabilite *)
-  (* PLUS *)
- |[|-(derivable (plus_fct ?1 ?2))] -> Apply (derivable_plus ?1 ?2); IsDiff_glob
-  (* MOINS *)
- |[|-(derivable (minus_fct ?1 ?2))] -> Apply (derivable_minus ?1 ?2); IsDiff_glob
-  (* OPPOSE *)
- |[|-(derivable (opp_fct ?1))] -> Apply (derivable_opp ?1); IsDiff_glob
-  (* MULTIPLICATION PAR UN SCALAIRE *)
- |[|-(derivable (mult_real_fct ?1 ?2))] -> Apply (derivable_scal ?2 ?1); IsDiff_glob
-  (* MULTIPLICATION *)
- |[|-(derivable (mult_fct ?1 ?2))] -> Apply (derivable_mult ?1 ?2); IsDiff_glob
-  (* DIVISION *)
- |[|-(derivable (div_fct ?1 ?2))] -> Apply (derivable_div ?1 ?2); [IsDiff_glob | IsDiff_glob | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct]
-  (* INVERSION *)
- |[|-(derivable (inv_fct ?1))] -> Apply (derivable_inv ?1); [Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct | IsDiff_glob]
-  (* COMPOSITION *)
- |[|-(derivable (comp sqrt ?))] -> Unfold derivable; Intro; Try IsDiff_pt
- |[|-(derivable (comp Rabsolu ?))] -> Unfold derivable; Intro; Try IsDiff_pt
- |[|-(derivable (comp ?1 ?2))] -> Apply (derivable_comp ?2 ?1); IsDiff_glob
- |[_:(derivable ?1)|-(derivable ?1)] -> Assumption
- |[|-True->(derivable ?)] -> Intro HypTruE; Clear HypTruE; IsDiff_glob
- | _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct.
+Ltac is_diff_glob :=
+  match goal with
+  |  |- (derivable Rsqr) => 
+  (* fonctions de base *)
+  apply derivable_Rsqr
+  |  |- (derivable id) => apply derivable_id
+  |  |- (derivable (fct_cte _)) => apply derivable_const
+  |  |- (derivable sin) => apply derivable_sin
+  |  |- (derivable cos) => apply derivable_cos
+  |  |- (derivable cosh) => apply derivable_cosh
+  |  |- (derivable sinh) => apply derivable_sinh
+  |  |- (derivable exp) => apply derivable_exp
+  |  |- (derivable (pow_fct _)) =>
+      unfold pow_fct in |- *;
+       apply derivable_pow
+        (* regles de differentiabilite *)
+        (* PLUS *)
+  |  |- (derivable (?X1 + ?X2)) =>
+      apply (derivable_plus X1 X2); is_diff_glob
+       (* MOINS *)
+  |  |- (derivable (?X1 - ?X2)) =>
+      apply (derivable_minus X1 X2); is_diff_glob
+       (* OPPOSE *)
+  |  |- (derivable (- ?X1)) =>
+      apply (derivable_opp X1);
+       is_diff_glob
+       (* MULTIPLICATION PAR UN SCALAIRE *)
+  |  |- (derivable (mult_real_fct ?X1 ?X2)) =>
+      apply (derivable_scal X2 X1); is_diff_glob
+       (* MULTIPLICATION *)
+  |  |- (derivable (?X1 * ?X2)) =>
+      apply (derivable_mult X1 X2); is_diff_glob
+       (* DIVISION *)
+  |  |- (derivable (?X1 / ?X2)) =>
+      apply (derivable_div X1 X2);
+       [ is_diff_glob
+       | is_diff_glob
+       | try
+          assumption ||
+            unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
+             id, fct_cte, comp, pow_fct in |- * ]
+  |  |- (derivable (/ ?X1)) =>
+      
+       (* INVERSION *)
+       apply (derivable_inv X1);
+       [ try
+          assumption ||
+            unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
+             id, fct_cte, comp, pow_fct in |- *
+       | is_diff_glob ]
+  |  |- (derivable (comp sqrt _)) =>
+      
+       (* COMPOSITION *)
+       unfold derivable in |- *; intro; try is_diff_pt
+  |  |- (derivable (comp Rabs _)) =>
+      unfold derivable in |- *; intro; try is_diff_pt
+  |  |- (derivable (comp ?X1 ?X2)) =>
+      apply (derivable_comp X2 X1); is_diff_glob
+  | _:(derivable ?X1) |- (derivable ?X1) => assumption
+  |  |- (True -> derivable _) =>
+      intro HypTruE; clear HypTruE; is_diff_glob
+  | _ =>
+      try
+       unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
+        fct_cte, comp, pow_fct in |- *
+  end.
 
 (**********)
-Recursive Tactic Definition IsCont_pt :=
-Match Context With
- (* fonctions de base *)
- [|-(continuity_pt Rsqr ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_Rsqr
-|[|-(continuity_pt id ?1)] -> Apply derivable_continuous_pt; Apply (derivable_pt_id ?1)
-|[|-(continuity_pt (fct_cte ?) ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_const
-|[|-(continuity_pt sin ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_sin
-|[|-(continuity_pt cos ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_cos
-|[|-(continuity_pt sinh ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_sinh
-|[|-(continuity_pt cosh ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_cosh
-|[|-(continuity_pt exp ?)] -> Apply derivable_continuous_pt; Apply derivable_pt_exp
-|[|-(continuity_pt (pow_fct ?) ?)] -> Unfold pow_fct; Apply derivable_continuous_pt; Apply derivable_pt_pow
-|[|-(continuity_pt sqrt ?1)] -> Apply continuity_pt_sqrt; Assumption Orelse Unfold plus_fct minus_fct opp_fct mult_fct div_fct inv_fct comp id fct_cte pow_fct
-|[|-(continuity_pt Rabsolu ?1)] -> Apply (continuity_Rabsolu ?1)
- (* regles de differentiabilite *)
- (* PLUS *)
-|[|-(continuity_pt (plus_fct ?1 ?2) ?3)] -> Apply (continuity_pt_plus ?1 ?2 ?3); IsCont_pt
- (* MOINS *)
-|[|-(continuity_pt (minus_fct ?1 ?2) ?3)] -> Apply (continuity_pt_minus ?1 ?2 ?3); IsCont_pt
- (* OPPOSE *)
-|[|-(continuity_pt (opp_fct ?1) ?2)] -> Apply (continuity_pt_opp ?1 ?2); IsCont_pt
- (* MULTIPLICATION PAR UN SCALAIRE *)
-|[|-(continuity_pt (mult_real_fct ?1 ?2) ?3)] -> Apply (continuity_pt_scal ?2 ?1 ?3); IsCont_pt
- (* MULTIPLICATION *)
-|[|-(continuity_pt (mult_fct ?1 ?2) ?3)] -> Apply (continuity_pt_mult ?1 ?2 ?3); IsCont_pt
-  (* DIVISION *)
- |[|-(continuity_pt (div_fct ?1 ?2) ?3)] -> Apply (continuity_pt_div ?1 ?2 ?3); [IsCont_pt | IsCont_pt | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte pow_fct]
-  (* INVERSION *)
- |[|-(continuity_pt (inv_fct ?1) ?2)] -> Apply (continuity_pt_inv ?1 ?2); [IsCont_pt | Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct comp id fct_cte pow_fct]
- (* COMPOSITION *)
-|[|-(continuity_pt (comp ?1 ?2) ?3)] -> Apply (continuity_pt_comp ?2 ?1 ?3); IsCont_pt
-|[_:(continuity_pt ?1 ?2)|-(continuity_pt ?1 ?2)] -> Assumption
-|[_:(continuity ?1) |- (continuity_pt ?1 ?2)] -> Cut (continuity ?1); [Intro HypDDPT; Apply HypDDPT | Assumption]
-|[_:(derivable_pt ?1 ?2)|-(continuity_pt ?1 ?2)] -> Apply derivable_continuous_pt; Assumption
-|[_:(derivable ?1)|-(continuity_pt ?1 ?2)] -> Cut (continuity ?1); [Intro HypDDPT; Apply HypDDPT | Apply derivable_continuous; Assumption]
-|[|-True->(continuity_pt ? ?)] -> Intro HypTruE; Clear HypTruE; IsCont_pt
-| _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct.
+Ltac is_cont_pt :=
+  match goal with
+  |  |- (continuity_pt Rsqr _) =>
+      
+       (* fonctions de base *)
+       apply derivable_continuous_pt; apply derivable_pt_Rsqr
+  |  |- (continuity_pt id ?X1) =>
+      apply derivable_continuous_pt; apply (derivable_pt_id X1)
+  |  |- (continuity_pt (fct_cte _) _) =>
+      apply derivable_continuous_pt; apply derivable_pt_const
+  |  |- (continuity_pt sin _) =>
+      apply derivable_continuous_pt; apply derivable_pt_sin
+  |  |- (continuity_pt cos _) =>
+      apply derivable_continuous_pt; apply derivable_pt_cos
+  |  |- (continuity_pt sinh _) =>
+      apply derivable_continuous_pt; apply derivable_pt_sinh
+  |  |- (continuity_pt cosh _) =>
+      apply derivable_continuous_pt; apply derivable_pt_cosh
+  |  |- (continuity_pt exp _) =>
+      apply derivable_continuous_pt; apply derivable_pt_exp
+  |  |- (continuity_pt (pow_fct _) _) =>
+      unfold pow_fct in |- *; apply derivable_continuous_pt;
+       apply derivable_pt_pow
+  |  |- (continuity_pt sqrt ?X1) =>
+      apply continuity_pt_sqrt;
+       assumption ||
+         unfold plus_fct, minus_fct, opp_fct, mult_fct, div_fct, inv_fct,
+          comp, id, fct_cte, pow_fct in |- *
+  |  |- (continuity_pt Rabs ?X1) =>
+      apply (Rcontinuity_abs X1)
+       (* regles de differentiabilite *)
+       (* PLUS *)
+  |  |- (continuity_pt (?X1 + ?X2) ?X3) =>
+      apply (continuity_pt_plus X1 X2 X3); is_cont_pt
+       (* MOINS *)
+  |  |- (continuity_pt (?X1 - ?X2) ?X3) =>
+      apply (continuity_pt_minus X1 X2 X3); is_cont_pt
+       (* OPPOSE *)
+  |  |- (continuity_pt (- ?X1) ?X2) =>
+      apply (continuity_pt_opp X1 X2);
+       is_cont_pt
+       (* MULTIPLICATION PAR UN SCALAIRE *)
+  |  |- (continuity_pt (mult_real_fct ?X1 ?X2) ?X3) =>
+      apply (continuity_pt_scal X2 X1 X3); is_cont_pt
+       (* MULTIPLICATION *)
+  |  |- (continuity_pt (?X1 * ?X2) ?X3) =>
+      apply (continuity_pt_mult X1 X2 X3); is_cont_pt
+       (* DIVISION *)
+  |  |- (continuity_pt (?X1 / ?X2) ?X3) =>
+      apply (continuity_pt_div X1 X2 X3);
+       [ is_cont_pt
+       | is_cont_pt
+       | try
+          assumption ||
+            unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
+             comp, id, fct_cte, pow_fct in |- * ]
+  |  |- (continuity_pt (/ ?X1) ?X2) =>
+      
+       (* INVERSION *)
+       apply (continuity_pt_inv X1 X2);
+       [ is_cont_pt
+       | assumption ||
+           unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
+            comp, id, fct_cte, pow_fct in |- * ]
+  |  |- (continuity_pt (comp ?X1 ?X2) ?X3) =>
+      
+       (* COMPOSITION *)
+       apply (continuity_pt_comp X2 X1 X3); is_cont_pt
+  | _:(continuity_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
+      assumption
+  | _:(continuity ?X1) |- (continuity_pt ?X1 ?X2) =>
+      cut (continuity X1); [ intro HypDDPT; apply HypDDPT | assumption ]
+  | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
+      apply derivable_continuous_pt; assumption
+  | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) =>
+      cut (continuity X1);
+       [ intro HypDDPT; apply HypDDPT
+       | apply derivable_continuous; assumption ]
+  |  |- (True -> continuity_pt _ _) =>
+      intro HypTruE; clear HypTruE; is_cont_pt
+  | _ =>
+      try
+       unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
+        fct_cte, comp, pow_fct in |- *
+  end.
 
 (**********)
-Recursive Tactic Definition IsCont_glob :=
-Match Context With
-  (* fonctions de base *)
-  [|-(continuity Rsqr)] -> Apply derivable_continuous; Apply derivable_Rsqr
- |[|-(continuity id)] -> Apply derivable_continuous; Apply derivable_id
- |[|-(continuity (fct_cte ?))] -> Apply derivable_continuous; Apply derivable_const
- |[|-(continuity sin)] -> Apply derivable_continuous; Apply derivable_sin
- |[|-(continuity cos)] -> Apply derivable_continuous; Apply derivable_cos
- |[|-(continuity exp)] -> Apply derivable_continuous; Apply derivable_exp
- |[|-(continuity (pow_fct ?))] -> Unfold pow_fct; Apply derivable_continuous; Apply derivable_pow
- |[|-(continuity sinh)] -> Apply derivable_continuous; Apply derivable_sinh
- |[|-(continuity cosh)] -> Apply derivable_continuous; Apply derivable_cosh
- |[|-(continuity Rabsolu)] -> Apply continuity_Rabsolu
- (* regles de continuite *)
- (* PLUS *)
-|[|-(continuity (plus_fct ?1 ?2))] -> Apply (continuity_plus ?1 ?2); Try IsCont_glob Orelse Assumption
- (* MOINS *)
-|[|-(continuity (minus_fct ?1 ?2))] -> Apply (continuity_minus ?1 ?2); Try IsCont_glob Orelse Assumption
- (* OPPOSE *)
-|[|-(continuity (opp_fct ?1))] -> Apply (continuity_opp ?1); Try IsCont_glob Orelse Assumption
- (* INVERSE *)
-|[|-(continuity (inv_fct ?1))] -> Apply (continuity_inv ?1); Try IsCont_glob Orelse Assumption
- (* MULTIPLICATION PAR UN SCALAIRE *)
-|[|-(continuity (mult_real_fct ?1 ?2))] -> Apply (continuity_scal ?2 ?1); Try IsCont_glob Orelse Assumption
- (* MULTIPLICATION *)
-|[|-(continuity (mult_fct ?1 ?2))] -> Apply (continuity_mult ?1 ?2); Try IsCont_glob Orelse Assumption
-  (* DIVISION *)
- |[|-(continuity (div_fct ?1 ?2))] -> Apply (continuity_div ?1 ?2); [Try IsCont_glob Orelse Assumption | Try IsCont_glob Orelse Assumption | Try Assumption Orelse Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte pow_fct]
-  (* COMPOSITION *)
- |[|-(continuity (comp sqrt ?))] -> Unfold continuity_pt; Intro; Try IsCont_pt
- |[|-(continuity (comp ?1 ?2))] -> Apply (continuity_comp ?2 ?1); Try IsCont_glob Orelse Assumption
- |[_:(continuity ?1)|-(continuity ?1)] -> Assumption
- |[|-True->(continuity ?)] -> Intro HypTruE; Clear HypTruE; IsCont_glob
- |[_:(derivable ?1)|-(continuity ?1)] -> Apply derivable_continuous; Assumption
- | _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct.
+Ltac is_cont_glob :=
+  match goal with
+  |  |- (continuity Rsqr) =>
+      
+       (* fonctions de base *)
+       apply derivable_continuous; apply derivable_Rsqr
+  |  |- (continuity id) => apply derivable_continuous; apply derivable_id
+  |  |- (continuity (fct_cte _)) =>
+      apply derivable_continuous; apply derivable_const
+  |  |- (continuity sin) => apply derivable_continuous; apply derivable_sin
+  |  |- (continuity cos) => apply derivable_continuous; apply derivable_cos
+  |  |- (continuity exp) => apply derivable_continuous; apply derivable_exp
+  |  |- (continuity (pow_fct _)) =>
+      unfold pow_fct in |- *; apply derivable_continuous; apply derivable_pow
+  |  |- (continuity sinh) =>
+      apply derivable_continuous; apply derivable_sinh
+  |  |- (continuity cosh) =>
+      apply derivable_continuous; apply derivable_cosh
+  |  |- (continuity Rabs) =>
+      apply Rcontinuity_abs
+       (* regles de continuite *)
+       (* PLUS *)
+  |  |- (continuity (?X1 + ?X2)) =>
+      apply (continuity_plus X1 X2);
+       try is_cont_glob || assumption
+            (* MOINS *)
+  |  |- (continuity (?X1 - ?X2)) =>
+      apply (continuity_minus X1 X2);
+       try is_cont_glob || assumption
+            (* OPPOSE *)
+  |  |- (continuity (- ?X1)) =>
+      apply (continuity_opp X1); try is_cont_glob || assumption
+                                      (* INVERSE *)
+  |  |- (continuity (/ ?X1)) =>
+      apply (continuity_inv X1);
+       try is_cont_glob || assumption
+            (* MULTIPLICATION PAR UN SCALAIRE *)
+  |  |- (continuity (mult_real_fct ?X1 ?X2)) =>
+      apply (continuity_scal X2 X1);
+       try is_cont_glob || assumption
+            (* MULTIPLICATION *)
+  |  |- (continuity (?X1 * ?X2)) =>
+      apply (continuity_mult X1 X2);
+       try is_cont_glob || assumption
+            (* DIVISION *)
+  |  |- (continuity (?X1 / ?X2)) =>
+      apply (continuity_div X1 X2);
+       [ try is_cont_glob || assumption
+       | try is_cont_glob || assumption
+       | try
+          assumption ||
+            unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
+             id, fct_cte, pow_fct in |- * ]
+  |  |- (continuity (comp sqrt _)) =>
+      
+       (* COMPOSITION *)
+       unfold continuity_pt in |- *; intro; try is_cont_pt
+  |  |- (continuity (comp ?X1 ?X2)) =>
+      apply (continuity_comp X2 X1); try is_cont_glob || assumption
+  | _:(continuity ?X1) |- (continuity ?X1) => assumption
+  |  |- (True -> continuity _) =>
+      intro HypTruE; clear HypTruE; is_cont_glob
+  | _:(derivable ?X1) |- (continuity ?X1) =>
+      apply derivable_continuous; assumption
+  | _ =>
+      try
+       unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
+        fct_cte, comp, pow_fct in |- *
+  end.
 
 (**********)
-Recursive Tactic Definition RewTerm trm :=
-Match trm With
-| [(Rplus ?1 ?2)] -> Let p1= (RewTerm ?1) And p2 = (RewTerm ?2) In 
-  (Match p1 With
-   [(fct_cte ?3)] -> 
-    (Match p2 With
-    | [(fct_cte ?4)] -> '(fct_cte (Rplus ?3 ?4))
-    | _ -> '(plus_fct p1 p2))
-  | _ -> '(plus_fct p1 p2))
-| [(Rminus ?1 ?2)] -> Let p1 = (RewTerm ?1) And p2 = (RewTerm ?2) In
-  (Match p1 With
-   [(fct_cte ?3)] -> 
-    (Match p2 With
-    | [(fct_cte ?4)] -> '(fct_cte (Rminus ?3 ?4))
-    | _ -> '(minus_fct p1 p2))
-  | _ -> '(minus_fct p1 p2))
-| [(Rdiv ?1 ?2)] -> Let p1 = (RewTerm ?1) And p2 = (RewTerm ?2) In
-  (Match p1 With
-   [(fct_cte ?3)] -> 
-    (Match p2 With
-    | [(fct_cte ?4)] -> '(fct_cte (Rdiv ?3 ?4))
-    | _ -> '(div_fct p1 p2))
-  | _ -> 
-    (Match p2 With
-    | [(fct_cte ?4)] -> '(mult_fct p1 (fct_cte (Rinv ?4)))
-    | _ -> '(div_fct p1 p2)))
-| [(Rmult ?1 (Rinv ?2))] -> Let p1 = (RewTerm ?1) And p2 = (RewTerm ?2) In
-  (Match p1 With
-   [(fct_cte ?3)] -> 
-    (Match p2 With
-    | [(fct_cte ?4)] -> '(fct_cte (Rdiv ?3 ?4))
-    | _ -> '(div_fct p1 p2))
-  | _ -> 
-   (Match p2 With
-   | [(fct_cte ?4)] -> '(mult_fct p1 (fct_cte (Rinv ?4)))
-   | _ -> '(div_fct p1 p2)))
-| [(Rmult ?1 ?2)] -> Let p1 = (RewTerm ?1) And p2 = (RewTerm ?2) In
-  (Match p1 With
-   [(fct_cte ?3)] -> 
-    (Match p2 With
-    | [(fct_cte ?4)] -> '(fct_cte (Rmult ?3 ?4))
-    | _ -> '(mult_fct p1 p2))
-  | _ -> '(mult_fct p1 p2))
-| [(Ropp ?1)] -> Let p = (RewTerm ?1) In 
-  (Match p With
-   [(fct_cte ?2)] -> '(fct_cte (Ropp ?2))
-   | _ -> '(opp_fct p))
-| [(Rinv ?1)] -> Let p = (RewTerm ?1) In 
-  (Match p With
-   [(fct_cte ?2)] -> '(fct_cte (Rinv ?2))
-   | _ -> '(inv_fct p))
-| [(?1 AppVar)] -> '?1
-| [(?1 ?2)] -> Let p = (RewTerm ?2) In 
- (Match p With
- | [(fct_cte ?3)] -> '(fct_cte (?1 ?3))
- | _ -> '(comp ?1 p))
-| [AppVar] -> 'id
-| [(pow AppVar ?1)] -> '(pow_fct ?1)
-| [(pow ?1 ?2)] -> Let p = (RewTerm ?1) In 
- (Match p With
- | [(fct_cte ?3)] -> '(fct_cte (pow_fct ?2 ?3))
- | _ -> '(comp (pow_fct ?2) p))
-| [?1]-> '(fct_cte ?1).
+Ltac rew_term trm :=
+  match constr:trm with
+  | (?X1 + ?X2) =>
+      let p1 := rew_term X1 with p2 := rew_term X2 in
+      match constr:p1 with
+      | (fct_cte ?X3) =>
+          match constr:p2 with
+          | (fct_cte ?X4) => constr:(fct_cte (X3 + X4))
+          | _ => constr:(p1 + p2)%F
+          end
+      | _ => constr:(p1 + p2)%F
+      end
+  | (?X1 - ?X2) =>
+      let p1 := rew_term X1 with p2 := rew_term X2 in
+      match constr:p1 with
+      | (fct_cte ?X3) =>
+          match constr:p2 with
+          | (fct_cte ?X4) => constr:(fct_cte (X3 - X4))
+          | _ => constr:(p1 - p2)%F
+          end
+      | _ => constr:(p1 - p2)%F
+      end
+  | (?X1 / ?X2) =>
+      let p1 := rew_term X1 with p2 := rew_term X2 in
+      match constr:p1 with
+      | (fct_cte ?X3) =>
+          match constr:p2 with
+          | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
+          | _ => constr:(p1 / p2)%F
+          end
+      | _ =>
+          match constr:p2 with
+          | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
+          | _ => constr:(p1 / p2)%F
+          end
+      end
+  | (?X1 * / ?X2) =>
+      let p1 := rew_term X1 with p2 := rew_term X2 in
+      match constr:p1 with
+      | (fct_cte ?X3) =>
+          match constr:p2 with
+          | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
+          | _ => constr:(p1 / p2)%F
+          end
+      | _ =>
+          match constr:p2 with
+          | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
+          | _ => constr:(p1 / p2)%F
+          end
+      end
+  | (?X1 * ?X2) =>
+      let p1 := rew_term X1 with p2 := rew_term X2 in
+      match constr:p1 with
+      | (fct_cte ?X3) =>
+          match constr:p2 with
+          | (fct_cte ?X4) => constr:(fct_cte (X3 * X4))
+          | _ => constr:(p1 * p2)%F
+          end
+      | _ => constr:(p1 * p2)%F
+      end
+  | (- ?X1) =>
+      let p := rew_term X1 in
+      match constr:p with
+      | (fct_cte ?X2) => constr:(fct_cte (- X2))
+      | _ => constr:(- p)%F
+      end
+  | (/ ?X1) =>
+      let p := rew_term X1 in
+      match constr:p with
+      | (fct_cte ?X2) => constr:(fct_cte (/ X2))
+      | _ => constr:(/ p)%F
+      end
+  | (?X1 AppVar) => constr:X1
+  | (?X1 ?X2) =>
+      let p := rew_term X2 in
+      match constr:p with
+      | (fct_cte ?X3) => constr:(fct_cte (X1 X3))
+      | _ => constr:(comp X1 p)
+      end
+  | AppVar => constr:id
+  | (AppVar ^ ?X1) => constr:(pow_fct X1)
+  | (?X1 ^ ?X2) =>
+      let p := rew_term X1 in
+      match constr:p with
+      | (fct_cte ?X3) => constr:(fct_cte (pow_fct X2 X3))
+      | _ => constr:(comp (pow_fct X2) p)
+      end
+  | ?X1 => constr:(fct_cte X1)
+  end.
 
 (**********)
-Recursive Tactic Definition ConsProof trm pt :=
-Match trm With
-| [(plus_fct ?1 ?2)] -> Let p1 = (ConsProof ?1 pt) And p2 = (ConsProof ?2 pt) In '(derivable_pt_plus ?1 ?2 pt p1 p2)
-| [(minus_fct ?1 ?2)] -> Let p1 = (ConsProof ?1 pt) And p2 = (ConsProof ?2 pt) In '(derivable_pt_minus ?1 ?2 pt p1 p2)
-| [(mult_fct ?1 ?2)] -> Let p1 = (ConsProof ?1 pt) And p2 = (ConsProof ?2 pt) In '(derivable_pt_mult ?1 ?2 pt p1 p2)
-| [(div_fct ?1 ?2)] ->
- (Match Context With
- |[id:~((?2 pt)==R0) |- ?] -> Let p1 = (ConsProof ?1 pt) And p2 = (ConsProof ?2 pt) In '(derivable_pt_div ?1 ?2 pt p1 p2 id)
- | _ -> 'False)
-| [(inv_fct ?1)] ->
- (Match Context With
- |[id:~((?1 pt)==R0) |- ?] -> Let p1 = (ConsProof ?1 pt) In '(derivable_pt_inv ?1 pt p1 id)
- | _ -> 'False)
-| [(comp ?1 ?2)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In Let p1 = (ConsProof ?1 pt_f1) And p2 = (ConsProof ?2 pt) In '(derivable_pt_comp ?2 ?1 pt p2 p1)
-| [(opp_fct ?1)] -> Let p1 = (ConsProof ?1 pt) In '(derivable_pt_opp ?1 pt p1)
-| [sin] -> '(derivable_pt_sin pt)
-| [cos] -> '(derivable_pt_cos pt)
-| [sinh] -> '(derivable_pt_sinh pt)
-| [cosh] -> '(derivable_pt_cosh pt)
-| [exp] -> '(derivable_pt_exp pt)
-| [id] -> '(derivable_pt_id pt)
-| [Rsqr] -> '(derivable_pt_Rsqr pt)
-| [sqrt] ->
- (Match Context With
- |[id:(Rlt R0 pt) |- ?] -> '(derivable_pt_sqrt pt id)
- | _ -> 'False)
-| [(fct_cte ?1)] -> '(derivable_pt_const ?1 pt)
-| [?1] -> Let aux = ?1 In
- (Match Context With
-    [ id : (derivable_pt aux pt) |- ?] -> 'id
-   |[ id : (derivable aux) |- ?] -> '(id pt)
-   | _ -> 'False).
+Ltac deriv_proof trm pt :=
+  match constr:trm with
+  | (?X1 + ?X2)%F =>
+      let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
+      constr:(derivable_pt_plus X1 X2 pt p1 p2)
+  | (?X1 - ?X2)%F =>
+      let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
+      constr:(derivable_pt_minus X1 X2 pt p1 p2)
+  | (?X1 * ?X2)%F =>
+      let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
+      constr:(derivable_pt_mult X1 X2 pt p1 p2)
+  | (?X1 / ?X2)%F =>
+      match goal with
+      | id:(?X2 pt <> 0) |- _ =>
+          let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
+          constr:(derivable_pt_div X1 X2 pt p1 p2 id)
+      | _ => constr:False
+      end
+  | (/ ?X1)%F =>
+      match goal with
+      | id:(?X1 pt <> 0) |- _ =>
+          let p1 := deriv_proof X1 pt in
+          constr:(derivable_pt_inv X1 pt p1 id)
+      | _ => constr:False
+      end
+  | (comp ?X1 ?X2) =>
+      let pt_f1 := eval cbv beta in (X2 pt) in
+      let p1 := deriv_proof X1 pt_f1 with p2 := deriv_proof X2 pt in
+      constr:(derivable_pt_comp X2 X1 pt p2 p1)
+  | (- ?X1)%F =>
+      let p1 := deriv_proof X1 pt in
+      constr:(derivable_pt_opp X1 pt p1)
+  | sin => constr:(derivable_pt_sin pt)
+  | cos => constr:(derivable_pt_cos pt)
+  | sinh => constr:(derivable_pt_sinh pt)
+  | cosh => constr:(derivable_pt_cosh pt)
+  | exp => constr:(derivable_pt_exp pt)
+  | id => constr:(derivable_pt_id pt)
+  | Rsqr => constr:(derivable_pt_Rsqr pt)
+  | sqrt =>
+      match goal with
+      | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id)
+      | _ => constr:False
+      end
+  | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt)
+  | ?X1 =>
+      let aux := constr:X1 in
+      match goal with
+      | id:(derivable_pt aux pt) |- _ => constr:id
+      | id:(derivable aux) |- _ => constr:(id pt)
+      | _ => constr:False
+      end
+  end.
 
 (**********)
-Recursive Tactic Definition SimplifyDerive trm pt :=
-Match trm With
-| [(plus_fct ?1 ?2)] -> Try Rewrite derive_pt_plus; SimplifyDerive ?1 pt; SimplifyDerive ?2 pt
-| [(minus_fct ?1 ?2)] -> Try Rewrite derive_pt_minus; SimplifyDerive ?1 pt; SimplifyDerive ?2 pt
-| [(mult_fct ?1 ?2)] -> Try Rewrite derive_pt_mult; SimplifyDerive ?1 pt; SimplifyDerive ?2 pt
-| [(div_fct ?1 ?2)] -> Try Rewrite derive_pt_div; SimplifyDerive ?1 pt; SimplifyDerive ?2 pt
-| [(comp ?1 ?2)] -> Let pt_f1 = (Eval Cbv Beta in (?2 pt)) In Try Rewrite derive_pt_comp; SimplifyDerive ?1 pt_f1; SimplifyDerive ?2 pt
-| [(opp_fct ?1)] -> Try Rewrite derive_pt_opp; SimplifyDerive ?1 pt
-| [(inv_fct ?1)] -> Try Rewrite derive_pt_inv; SimplifyDerive ?1 pt
-| [(fct_cte ?1)] -> Try Rewrite derive_pt_const
-| [id] -> Try Rewrite derive_pt_id
-| [sin] -> Try Rewrite derive_pt_sin
-| [cos] -> Try Rewrite derive_pt_cos
-| [sinh] -> Try Rewrite derive_pt_sinh
-| [cosh] -> Try Rewrite derive_pt_cosh
-| [exp] -> Try Rewrite derive_pt_exp
-| [Rsqr] -> Try Rewrite derive_pt_Rsqr
-| [sqrt] -> Try Rewrite derive_pt_sqrt
-| [?1] -> Let aux = ?1 In
-  (Match Context With
-    [ id : (eqT ? (derive_pt aux pt ?2) ?); H : (derivable aux) |- ? ] -> Try Replace (derive_pt aux pt (H pt)) with (derive_pt aux pt ?2); [Rewrite id | Apply pr_nu]
-    |[ id : (eqT ? (derive_pt aux pt ?2) ?); H : (derivable_pt aux pt) |- ? ] -> Try Replace (derive_pt aux pt H) with (derive_pt aux pt ?2); [Rewrite id | Apply pr_nu]
-    | _ -> Idtac )
-| _ -> Idtac.
+Ltac simplify_derive trm pt :=
+  match constr:trm with
+  | (?X1 + ?X2)%F =>
+      try rewrite derive_pt_plus; simplify_derive X1 pt;
+       simplify_derive X2 pt
+  | (?X1 - ?X2)%F =>
+      try rewrite derive_pt_minus; simplify_derive X1 pt;
+       simplify_derive X2 pt
+  | (?X1 * ?X2)%F =>
+      try rewrite derive_pt_mult; simplify_derive X1 pt;
+       simplify_derive X2 pt
+  | (?X1 / ?X2)%F =>
+      try rewrite derive_pt_div; simplify_derive X1 pt; simplify_derive X2 pt
+  | (comp ?X1 ?X2) =>
+      let pt_f1 := eval cbv beta in (X2 pt) in
+      (try rewrite derive_pt_comp; simplify_derive X1 pt_f1;
+        simplify_derive X2 pt)
+  | (- ?X1)%F => try rewrite derive_pt_opp; simplify_derive X1 pt
+  | (/ ?X1)%F =>
+      try rewrite derive_pt_inv; simplify_derive X1 pt
+  | (fct_cte ?X1) => try rewrite derive_pt_const
+  | id => try rewrite derive_pt_id
+  | sin => try rewrite derive_pt_sin
+  | cos => try rewrite derive_pt_cos
+  | sinh => try rewrite derive_pt_sinh
+  | cosh => try rewrite derive_pt_cosh
+  | exp => try rewrite derive_pt_exp
+  | Rsqr => try rewrite derive_pt_Rsqr
+  | sqrt => try rewrite derive_pt_sqrt
+  | ?X1 =>
+      let aux := constr:X1 in
+      match goal with
+      | id:(derive_pt aux pt ?X2 = _),H:(derivable aux) |- _ =>
+          try replace (derive_pt aux pt (H pt)) with (derive_pt aux pt X2);
+           [ rewrite id | apply pr_nu ]
+      | id:(derive_pt aux pt ?X2 = _),H:(derivable_pt aux pt) |- _ =>
+          try replace (derive_pt aux pt H) with (derive_pt aux pt X2);
+           [ rewrite id | apply pr_nu ]
+      | _ => idtac
+      end
+  | _ => idtac
+  end.
 
 (**********)
-Tactic Definition Reg :=
-Match Context With
-| [|-(derivable_pt ?1 ?2)] -> 
-Let trm = Eval Cbv Beta in (?1 AppVar) In
-Let aux = (RewTerm trm) In IntroHypL aux ?2; Try (Change (derivable_pt aux ?2); IsDiff_pt) Orelse IsDiff_pt
-| [|-(derivable ?1)] ->
-Let trm = Eval Cbv Beta in (?1 AppVar) In
-Let aux = (RewTerm trm) In IntroHypG aux; Try (Change (derivable aux); IsDiff_glob) Orelse IsDiff_glob
-| [|-(continuity ?1)] ->
-Let trm = Eval Cbv Beta in (?1 AppVar) In
-Let aux = (RewTerm trm) In IntroHypG aux; Try (Change (continuity aux); IsCont_glob) Orelse IsCont_glob
-| [|-(continuity_pt ?1 ?2)] ->
-Let trm = Eval Cbv Beta in (?1 AppVar) In
-Let aux = (RewTerm trm) In IntroHypL aux ?2; Try (Change (continuity_pt aux ?2); IsCont_pt) Orelse IsCont_pt
-| [|-(eqT ? (derive_pt ?1 ?2 ?3) ?4)] -> 
-Let trm = Eval Cbv Beta in (?1 AppVar) In
-Let aux = (RewTerm trm) In
-IntroHypL aux ?2; Let aux2 = (ConsProof aux ?2) In Try (Replace (derive_pt ?1 ?2 ?3) with (derive_pt aux ?2 aux2); [SimplifyDerive aux ?2; Try Unfold plus_fct minus_fct mult_fct div_fct id fct_cte inv_fct opp_fct; Try Ring | Try Apply pr_nu]) Orelse IsDiff_pt.
+Ltac reg :=
+  match goal with
+  |  |- (derivable_pt ?X1 ?X2) =>
+      let trm := eval cbv beta in (X1 AppVar) in
+      let aux := rew_term trm in
+      (intro_hyp_pt aux X2;
+        try (change (derivable_pt aux X2) in |- *; is_diff_pt) || is_diff_pt)
+  |  |- (derivable ?X1) =>
+      let trm := eval cbv beta in (X1 AppVar) in
+      let aux := rew_term trm in
+      (intro_hyp_glob aux;
+        try (change (derivable aux) in |- *; is_diff_glob) || is_diff_glob)
+  |  |- (continuity ?X1) =>
+      let trm := eval cbv beta in (X1 AppVar) in
+      let aux := rew_term trm in
+      (intro_hyp_glob aux;
+        try (change (continuity aux) in |- *; is_cont_glob) || is_cont_glob)
+  |  |- (continuity_pt ?X1 ?X2) =>
+      let trm := eval cbv beta in (X1 AppVar) in
+      let aux := rew_term trm in
+      (intro_hyp_pt aux X2;
+        try (change (continuity_pt aux X2) in |- *; is_cont_pt) || is_cont_pt)
+  |  |- (derive_pt ?X1 ?X2 ?X3 = ?X4) =>
+      let trm := eval cbv beta in (X1 AppVar) in
+      let aux := rew_term trm in
+      (intro_hyp_pt aux X2;
+        let aux2 := deriv_proof aux X2 in
+        (try
+          (replace (derive_pt X1 X2 X3) with (derive_pt aux X2 aux2);
+            [ simplify_derive aux X2;
+               try
+                unfold plus_fct, minus_fct, mult_fct, div_fct, id, fct_cte,
+                 inv_fct, opp_fct in |- *; try ring
+            | try apply pr_nu ]) || is_diff_pt))
+  end.
\ No newline at end of file