diff options
Diffstat (limited to 'theories/Reals/Ranalysis.v')
| -rw-r--r-- | theories/Reals/Ranalysis.v | 1061 |
1 files changed, 530 insertions, 531 deletions
diff --git a/theories/Reals/Ranalysis.v b/theories/Reals/Ranalysis.v index b885e4ce..d712f74b 100644 --- a/theories/Reals/Ranalysis.v +++ b/theories/Reals/Ranalysis.v @@ -5,8 +5,8 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) - -(*i $Id: Ranalysis.v 5920 2004-07-16 20:01:26Z herbelin $ i*) + +(*i $Id: Ranalysis.v 9319 2006-10-30 12:41:21Z barras $ i*) Require Import Rbase. Require Import Rfunctions. @@ -34,769 +34,768 @@ Axiom AppVar : R. (**********) Ltac intro_hyp_glob trm := match constr:trm with - | (?X1 + ?X2)%F => + | (?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 + | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 + | |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2 + | _ => idtac end - | (?X1 - ?X2)%F => + | (?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 + | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 + | |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2 + | _ => idtac end - | (?X1 * ?X2)%F => + | (?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 + | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 + | |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2 + | _ => idtac end - | (?X1 / ?X2)%F => + | (?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 - | _:(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 + | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2 + | |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2 + | _ => idtac end - | (- ?X1)%F => + | (- ?X1)%F => match goal with - | |- (derivable _) => intro_hyp_glob X1 - | |- (continuity _) => intro_hyp_glob X1 - | _ => idtac + | |- (derivable _) => intro_hyp_glob X1 + | |- (continuity _) => intro_hyp_glob X1 + | _ => idtac end - | (/ ?X1)%F => + | (/ ?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 => + 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 + 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. (**********) Ltac intro_hyp_pt trm pt := match constr:trm with - | (?X1 + ?X2)%F => + | (?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 _ _ _ = _) => + | |- (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 + | _ => idtac end - | (?X1 - ?X2)%F => + | (?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 _ _ _ = _) => + | |- (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 + | _ => idtac end - | (?X1 * ?X2)%F => + | (?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 _ _ _ = _) => + | |- (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 + | _ => idtac end - | (?X1 / ?X2)%F => + | (?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 - | _:(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 _ _) => + | |- (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 _ _) => + (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 _ _ _ = _) => + (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 + (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt) + | _ => idtac end - | (- ?X1)%F => + | (- ?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 + | |- (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 => + | (/ ?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 - | _:(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 _ _) => + | |- (derivable_pt _ _) => cut (0 < pt); [ intro | try assumption ] + | |- (continuity_pt _ _) => cut (0 <= pt); [ intro | try assumption ] - | |- (derive_pt _ _ _ = _) => + | |- (derive_pt _ _ _ = _) => cut (0 < pt); [ intro | try assumption ] - | _ => idtac + | _ => idtac end - | Rabs => + | Rabs => match goal with - | |- (derivable_pt _ _) => + | |- (derivable_pt _ _) => cut (pt <> 0); [ intro | try assumption ] - | _ => idtac + | _ => idtac end - | ?X1 => + | ?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 + 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. - + (**********) Ltac is_diff_pt := match goal with - | |- (derivable_pt Rsqr _) => + | |- (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 _) _) => + 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) => + | |- (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) => + 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 |- * + 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) => + | |- (derivable_pt (?X1 + ?X2) ?X3) => apply (derivable_pt_plus X1 X2 X3); is_diff_pt (* MOINS *) - | |- (derivable_pt (?X1 - ?X2) ?X3) => + | |- (derivable_pt (?X1 - ?X2) ?X3) => apply (derivable_pt_minus X1 X2 X3); is_diff_pt (* OPPOSE *) - | |- (derivable_pt (- ?X1) ?X2) => + | |- (derivable_pt (- ?X1) ?X2) => apply (derivable_pt_opp X1 X2); - is_diff_pt + is_diff_pt (* MULTIPLICATION PAR UN SCALAIRE *) - | |- (derivable_pt (mult_real_fct ?X1 ?X2) ?X3) => + | |- (derivable_pt (mult_real_fct ?X1 ?X2) ?X3) => apply (derivable_pt_scal X2 X1 X3); is_diff_pt (* MULTIPLICATION *) - | |- (derivable_pt (?X1 * ?X2) ?X3) => + | |- (derivable_pt (?X1 * ?X2) ?X3) => apply (derivable_pt_mult X1 X2 X3); is_diff_pt (* DIVISION *) - | |- (derivable_pt (?X1 / ?X2) ?X3) => + | |- (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) => + [ 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, + 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) => + | 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) => + 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) => + | _:(derivable ?X1) |- (derivable_pt ?X1 ?X2) => cut (derivable X1); [ intro HypDDPT; apply HypDDPT | assumption ] - | |- (True -> derivable_pt _ _) => + | |- (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 |- * + unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id, + fct_cte, comp, pow_fct in |- * end. (**********) Ltac is_diff_glob := match goal with - | |- (derivable Rsqr) => + | |- (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 _)) => + 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 + apply derivable_pow (* regles de differentiabilite *) (* PLUS *) - | |- (derivable (?X1 + ?X2)) => + | |- (derivable (?X1 + ?X2)) => apply (derivable_plus X1 X2); is_diff_glob (* MOINS *) - | |- (derivable (?X1 - ?X2)) => + | |- (derivable (?X1 - ?X2)) => apply (derivable_minus X1 X2); is_diff_glob (* OPPOSE *) - | |- (derivable (- ?X1)) => + | |- (derivable (- ?X1)) => apply (derivable_opp X1); - is_diff_glob + is_diff_glob (* MULTIPLICATION PAR UN SCALAIRE *) - | |- (derivable (mult_real_fct ?X1 ?X2)) => + | |- (derivable (mult_real_fct ?X1 ?X2)) => apply (derivable_scal X2 X1); is_diff_glob (* MULTIPLICATION *) - | |- (derivable (?X1 * ?X2)) => + | |- (derivable (?X1 * ?X2)) => apply (derivable_mult X1 X2); is_diff_glob (* DIVISION *) - | |- (derivable (?X1 / ?X2)) => + | |- (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)) => + [ 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 + 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 _)) => + 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)) => + | |- (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 _) => + | _:(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 |- * + unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id, + fct_cte, comp, pow_fct in |- * end. (**********) Ltac is_cont_pt := match goal with - | |- (continuity_pt Rsqr _) => + | |- (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_Rsqr + | |- (continuity_pt id ?X1) => apply derivable_continuous_pt; apply (derivable_pt_id X1) - | |- (continuity_pt (fct_cte _) _) => + | |- (continuity_pt (fct_cte _) _) => apply derivable_continuous_pt; apply derivable_pt_const - | |- (continuity_pt sin _) => + | |- (continuity_pt sin _) => apply derivable_continuous_pt; apply derivable_pt_sin - | |- (continuity_pt cos _) => + | |- (continuity_pt cos _) => apply derivable_continuous_pt; apply derivable_pt_cos - | |- (continuity_pt sinh _) => + | |- (continuity_pt sinh _) => apply derivable_continuous_pt; apply derivable_pt_sinh - | |- (continuity_pt cosh _) => + | |- (continuity_pt cosh _) => apply derivable_continuous_pt; apply derivable_pt_cosh - | |- (continuity_pt exp _) => + | |- (continuity_pt exp _) => apply derivable_continuous_pt; apply derivable_pt_exp - | |- (continuity_pt (pow_fct _) _) => + | |- (continuity_pt (pow_fct _) _) => unfold pow_fct in |- *; apply derivable_continuous_pt; - apply derivable_pt_pow - | |- (continuity_pt sqrt ?X1) => + 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) => + 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) => + | |- (continuity_pt (?X1 + ?X2) ?X3) => apply (continuity_pt_plus X1 X2 X3); is_cont_pt (* MOINS *) - | |- (continuity_pt (?X1 - ?X2) ?X3) => + | |- (continuity_pt (?X1 - ?X2) ?X3) => apply (continuity_pt_minus X1 X2 X3); is_cont_pt (* OPPOSE *) - | |- (continuity_pt (- ?X1) ?X2) => + | |- (continuity_pt (- ?X1) ?X2) => apply (continuity_pt_opp X1 X2); - is_cont_pt + is_cont_pt (* MULTIPLICATION PAR UN SCALAIRE *) - | |- (continuity_pt (mult_real_fct ?X1 ?X2) ?X3) => + | |- (continuity_pt (mult_real_fct ?X1 ?X2) ?X3) => apply (continuity_pt_scal X2 X1 X3); is_cont_pt (* MULTIPLICATION *) - | |- (continuity_pt (?X1 * ?X2) ?X3) => + | |- (continuity_pt (?X1 * ?X2) ?X3) => apply (continuity_pt_mult X1 X2 X3); is_cont_pt (* DIVISION *) - | |- (continuity_pt (?X1 / ?X2) ?X3) => + | |- (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) => + [ 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) => + 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) => + 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) => + | _:(continuity ?X1) |- (continuity_pt ?X1 ?X2) => cut (continuity X1); [ intro HypDDPT; apply HypDDPT | assumption ] - | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) => + | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) => apply derivable_continuous_pt; assumption - | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) => + | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) => cut (continuity X1); - [ intro HypDDPT; apply HypDDPT - | apply derivable_continuous; assumption ] - | |- (True -> continuity_pt _ _) => + [ 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 |- * + unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id, + fct_cte, comp, pow_fct in |- * end. (**********) Ltac is_cont_glob := match goal with - | |- (continuity Rsqr) => + | |- (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_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 _)) => + | |- (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) => + | |- (continuity sinh) => apply derivable_continuous; apply derivable_sinh - | |- (continuity cosh) => + | |- (continuity cosh) => apply derivable_continuous; apply derivable_cosh - | |- (continuity Rabs) => + | |- (continuity Rabs) => apply Rcontinuity_abs (* regles de continuite *) (* PLUS *) - | |- (continuity (?X1 + ?X2)) => + | |- (continuity (?X1 + ?X2)) => apply (continuity_plus X1 X2); - try is_cont_glob || assumption + try is_cont_glob || assumption (* MOINS *) - | |- (continuity (?X1 - ?X2)) => + | |- (continuity (?X1 - ?X2)) => apply (continuity_minus X1 X2); - try is_cont_glob || assumption + try is_cont_glob || assumption (* OPPOSE *) - | |- (continuity (- ?X1)) => + | |- (continuity (- ?X1)) => apply (continuity_opp X1); try is_cont_glob || assumption (* INVERSE *) - | |- (continuity (/ ?X1)) => + | |- (continuity (/ ?X1)) => apply (continuity_inv X1); - try is_cont_glob || assumption + try is_cont_glob || assumption (* MULTIPLICATION PAR UN SCALAIRE *) - | |- (continuity (mult_real_fct ?X1 ?X2)) => + | |- (continuity (mult_real_fct ?X1 ?X2)) => apply (continuity_scal X2 X1); - try is_cont_glob || assumption + try is_cont_glob || assumption (* MULTIPLICATION *) - | |- (continuity (?X1 * ?X2)) => + | |- (continuity (?X1 * ?X2)) => apply (continuity_mult X1 X2); - try is_cont_glob || assumption + try is_cont_glob || assumption (* DIVISION *) - | |- (continuity (?X1 / ?X2)) => + | |- (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 _)) => + [ 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)) => + 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 _) => + | _:(continuity ?X1) |- (continuity ?X1) => assumption + | |- (True -> continuity _) => intro HypTruE; clear HypTruE; is_cont_glob - | _:(derivable ?X1) |- (continuity ?X1) => + | _:(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 |- * + unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id, + fct_cte, comp, pow_fct in |- * end. (**********) Ltac rew_term trm := match constr:trm with - | (?X1 + ?X2) => + | (?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)) + 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 - | _ => constr:(p1 + p2)%F - end - | (?X1 - ?X2) => + 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)) + 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 - | _ => constr:(p1 - p2)%F - end - | (?X1 / ?X2) => + 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) => + 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) => + 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)) + 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 - | _ => constr:(p1 * p2)%F - end - | (- ?X1) => + end + | (- ?X1) => let p := rew_term X1 in - match constr:p with - | (fct_cte ?X2) => constr:(fct_cte (- X2)) - | _ => constr:(- p)%F - end - | (/ ?X1) => + 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) => + 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) => + 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) + 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. (**********) Ltac deriv_proof trm pt := match constr:trm with - | (?X1 + ?X2)%F => + | (?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 => + 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 => + 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 => + constr:(derivable_pt_mult X1 X2 pt p1 p2) + | (?X1 / ?X2)%F => match goal with - | id:(?X2 pt <> 0) |- _ => + | 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 + constr:(derivable_pt_div X1 X2 pt p1 p2 id) + | _ => constr:False end - | (/ ?X1)%F => + | (/ ?X1)%F => match goal with - | id:(?X1 pt <> 0) |- _ => + | id:(?X1 pt <> 0) |- _ => let p1 := deriv_proof X1 pt in - constr:(derivable_pt_inv X1 pt p1 id) - | _ => constr:False + constr:(derivable_pt_inv X1 pt p1 id) + | _ => constr:False end - | (comp ?X1 ?X2) => + | (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_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 => + 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 + | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id) + | _ => constr:False end - | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt) - | ?X1 => + | (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 + match goal with + | id:(derivable_pt aux pt) |- _ => constr:id + | id:(derivable aux) |- _ => constr:(id pt) + | _ => constr:False + end end. (**********) Ltac simplify_derive trm pt := match constr:trm with - | (?X1 + ?X2)%F => + | (?X1 + ?X2)%F => try rewrite derive_pt_plus; simplify_derive X1 pt; - simplify_derive X2 pt - | (?X1 - ?X2)%F => + simplify_derive X2 pt + | (?X1 - ?X2)%F => try rewrite derive_pt_minus; simplify_derive X1 pt; - simplify_derive X2 pt - | (?X1 * ?X2)%F => + simplify_derive X2 pt + | (?X1 * ?X2)%F => try rewrite derive_pt_mult; simplify_derive X1 pt; - simplify_derive X2 pt - | (?X1 / ?X2)%F => + simplify_derive X2 pt + | (?X1 / ?X2)%F => try rewrite derive_pt_div; simplify_derive X1 pt; simplify_derive X2 pt - | (comp ?X1 ?X2) => + | (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_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 => + | (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 + 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. (**********) Ltac reg := match goal with - | |- (derivable_pt ?X1 ?X2) => + | |- (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 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 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 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 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 + 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 |- *; ring || ring_simplify + | try apply pr_nu ]) || is_diff_pt) + end. |