Quelques ameliorations dans Reg

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

1 files changed, 70 insertions, 63 deletions

diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v
index a2fbac997..585a6d773 100644
--- a/theories/Reals/Ranalysis4.v
+++ b/theories/Reals/Ranalysis4.v
@@ -432,8 +432,11 @@ Match trm With
 |[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
@@ -509,6 +512,7 @@ Match trm With
 |[Rsqr] -> Idtac
 |[id] -> Idtac
 |[(fct_cte ?)] -> Idtac
+|[(pow_fct ?)] -> Idtac
 |[sqrt] ->
  (Match Context With
  |[|-(derivable_pt ? ?)] -> Cut ``0<pt``; [Intro | Try Assumption]
@@ -529,6 +533,43 @@ Match trm With
  |[|-(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).
+ 
+(**********)
+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.
 
 (**********)
 Recursive Tactic Definition IsDiff_glob :=
@@ -559,46 +600,50 @@ Match Context With
   (* 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.
- 
+
 (**********)
-Recursive Tactic Definition IsDiff_pt :=
+Recursive Tactic Definition IsCont_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
+ [|-(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 *)
-|[|-(derivable_pt (plus_fct ?1 ?2) ?3)] -> Apply (derivable_pt_plus ?1 ?2 ?3); IsDiff_pt
+|[|-(continuity_pt (plus_fct ?1 ?2) ?3)] -> Apply (continuity_pt_plus ?1 ?2 ?3); IsCont_pt
  (* MOINS *)
-|[|-(derivable_pt (minus_fct ?1 ?2) ?3)] -> Apply (derivable_pt_minus ?1 ?2 ?3); IsDiff_pt
+|[|-(continuity_pt (minus_fct ?1 ?2) ?3)] -> Apply (continuity_pt_minus ?1 ?2 ?3); IsCont_pt
  (* OPPOSE *)
-|[|-(derivable_pt (opp_fct ?1) ?2)] -> Apply (derivable_pt_opp ?1 ?2); IsDiff_pt
+|[|-(continuity_pt (opp_fct ?1) ?2)] -> Apply (continuity_pt_opp ?1 ?2); IsCont_pt
  (* MULTIPLICATION PAR UN SCALAIRE *)
-|[|-(derivable_pt (mult_real_fct ?1 ?2) ?3)] -> Apply (derivable_pt_scal ?2 ?1 ?3); IsDiff_pt
+|[|-(continuity_pt (mult_real_fct ?1 ?2) ?3)] -> Apply (continuity_pt_scal ?2 ?1 ?3); IsCont_pt
  (* MULTIPLICATION *)
-|[|-(derivable_pt (mult_fct ?1 ?2) ?3)] -> Apply (derivable_pt_mult ?1 ?2 ?3); IsDiff_pt
+|[|-(continuity_pt (mult_fct ?1 ?2) ?3)] -> Apply (continuity_pt_mult ?1 ?2 ?3); IsCont_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]
+ |[|-(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 *)
- |[|-(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]
+ |[|-(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 *)
-|[|-(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
+|[|-(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.
 
 (**********)
@@ -631,6 +676,7 @@ Match Context With
   (* 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
@@ -638,45 +684,6 @@ Match Context With
  | _ -> Try Unfold plus_fct mult_fct div_fct minus_fct opp_fct inv_fct id fct_cte comp pow_fct.
 
 (**********)
-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.
-
-(**********)
 Recursive Tactic Definition RewTerm trm :=
 Match trm With
 | [(Rplus ?1 ?2)] -> Let p1= (RewTerm ?1) And p2 = (RewTerm ?2) In