1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Ranalysis.v,v 1.19.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
35 include "Reals/Rbase.ma".
37 include "Reals/Rfunctions.ma".
39 include "Reals/Rtrigo.ma".
41 include "Reals/SeqSeries.ma".
43 include "Reals/Ranalysis1.ma".
45 include "Reals/Ranalysis2.ma".
47 include "Reals/Ranalysis3.ma".
49 include "Reals/Rtopology.ma".
51 include "Reals/MVT.ma".
53 include "Reals/PSeries_reg.ma".
55 include "Reals/Exp_prop.ma".
57 include "Reals/Rtrigo_reg.ma".
59 include "Reals/Rsqrt_def.ma".
61 include "Reals/R_sqrt.ma".
63 include "Reals/Rtrigo_calc.ma".
65 include "Reals/Rgeom.ma".
67 include "Reals/RList.ma".
69 include "Reals/Sqrt_reg.ma".
71 include "Reals/Ranalysis4.ma".
73 include "Reals/Rpower.ma".
76 Open Local Scope R_scope.
79 inline procedural "cic:/Coq/Reals/Ranalysis/AppVar.con".
84 Ltac intro_hyp_glob trm :=
88 | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
89 | |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
94 | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
95 | |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
100 | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
101 | |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
105 let aux := constr:X2 in
107 | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
108 intro_hyp_glob X1; intro_hyp_glob X2
109 | _:(forall x0:R, aux x0 <> 0) |- (continuity _) =>
110 intro_hyp_glob X1; intro_hyp_glob X2
111 | |- (derivable _) =>
112 cut (forall x0:R, aux x0 <> 0);
113 [ intro; intro_hyp_glob X1; intro_hyp_glob X2 | try assumption ]
114 | |- (continuity _) =>
115 cut (forall x0:R, aux x0 <> 0);
116 [ intro; intro_hyp_glob X1; intro_hyp_glob X2 | try assumption ]
121 | |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
122 | |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
127 | |- (derivable _) => intro_hyp_glob X1
128 | |- (continuity _) => intro_hyp_glob X1
132 let aux := constr:X1 in
134 | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
136 | _:(forall x0:R, aux x0 <> 0) |- (continuity _) =>
138 | |- (derivable _) =>
139 cut (forall x0:R, aux x0 <> 0);
140 [ intro; intro_hyp_glob X1 | try assumption ]
141 | |- (continuity _) =>
142 cut (forall x0:R, aux x0 <> 0);
143 [ intro; intro_hyp_glob X1 | try assumption ]
154 | (fct_cte _) => idtac
155 | (pow_fct _) => idtac
158 let p := constr:X1 in
160 | _:(derivable p) |- _ => idtac
161 | |- (derivable p) => idtac
162 | |- (derivable _) =>
163 cut (True -> derivable p);
164 [ intro HYPPD; cut (derivable p);
165 [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
167 | _:(continuity p) |- _ => idtac
168 | |- (continuity p) => idtac
169 | |- (continuity _) =>
170 cut (True -> continuity p);
171 [ intro HYPPD; cut (continuity p);
172 [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
182 Ltac intro_hyp_pt trm pt :=
183 match constr:trm with
186 | |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
187 | |- (continuity_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
188 | |- (derive_pt _ _ _ = _) =>
189 intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
194 | |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
195 | |- (continuity_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
196 | |- (derive_pt _ _ _ = _) =>
197 intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
202 | |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
203 | |- (continuity_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
204 | |- (derive_pt _ _ _ = _) =>
205 intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
209 let aux := constr:X2 in
211 | _:(aux pt <> 0) |- (derivable_pt _ _) =>
212 intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
213 | _:(aux pt <> 0) |- (continuity_pt _ _) =>
214 intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
215 | _:(aux pt <> 0) |- (derive_pt _ _ _ = _) =>
216 intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
217 | id:(forall x0:R, aux x0 <> 0) |- (derivable_pt _ _) =>
218 generalize (id pt); intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
219 | id:(forall x0:R, aux x0 <> 0) |- (continuity_pt _ _) =>
220 generalize (id pt); intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
221 | id:(forall x0:R, aux x0 <> 0) |- (derive_pt _ _ _ = _) =>
222 generalize (id pt); intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
223 | |- (derivable_pt _ _) =>
225 [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
226 | |- (continuity_pt _ _) =>
228 [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
229 | |- (derive_pt _ _ _ = _) =>
231 [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
236 | |- (derivable_pt _ _) =>
237 let pt_f1 := eval cbv beta in (X2 pt) in
238 (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt)
239 | |- (continuity_pt _ _) =>
240 let pt_f1 := eval cbv beta in (X2 pt) in
241 (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt)
242 | |- (derive_pt _ _ _ = _) =>
243 let pt_f1 := eval cbv beta in (X2 pt) in
244 (intro_hyp_pt X1 pt_f1; intro_hyp_pt X2 pt)
249 | |- (derivable_pt _ _) => intro_hyp_pt X1 pt
250 | |- (continuity_pt _ _) => intro_hyp_pt X1 pt
251 | |- (derive_pt _ _ _ = _) => intro_hyp_pt X1 pt
255 let aux := constr:X1 in
257 | _:(aux pt <> 0) |- (derivable_pt _ _) =>
259 | _:(aux pt <> 0) |- (continuity_pt _ _) =>
261 | _:(aux pt <> 0) |- (derive_pt _ _ _ = _) =>
263 | id:(forall x0:R, aux x0 <> 0) |- (derivable_pt _ _) =>
264 generalize (id pt); intro; intro_hyp_pt X1 pt
265 | id:(forall x0:R, aux x0 <> 0) |- (continuity_pt _ _) =>
266 generalize (id pt); intro; intro_hyp_pt X1 pt
267 | id:(forall x0:R, aux x0 <> 0) |- (derive_pt _ _ _ = _) =>
268 generalize (id pt); intro; intro_hyp_pt X1 pt
269 | |- (derivable_pt _ _) =>
270 cut (aux pt <> 0); [ intro; intro_hyp_pt X1 pt | try assumption ]
271 | |- (continuity_pt _ _) =>
272 cut (aux pt <> 0); [ intro; intro_hyp_pt X1 pt | try assumption ]
273 | |- (derive_pt _ _ _ = _) =>
274 cut (aux pt <> 0); [ intro; intro_hyp_pt X1 pt | try assumption ]
284 | (fct_cte _) => idtac
285 | (pow_fct _) => idtac
288 | |- (derivable_pt _ _) => cut (0 < pt); [ intro | try assumption ]
289 | |- (continuity_pt _ _) =>
290 cut (0 <= pt); [ intro | try assumption ]
291 | |- (derive_pt _ _ _ = _) =>
292 cut (0 < pt); [ intro | try assumption ]
297 | |- (derivable_pt _ _) =>
298 cut (pt <> 0); [ intro | try assumption ]
302 let p := constr:X1 in
304 | _:(derivable_pt p pt) |- _ => idtac
305 | |- (derivable_pt p pt) => idtac
306 | |- (derivable_pt _ _) =>
307 cut (True -> derivable_pt p pt);
308 [ intro HYPPD; cut (derivable_pt p pt);
309 [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
311 | _:(continuity_pt p pt) |- _ => idtac
312 | |- (continuity_pt p pt) => idtac
313 | |- (continuity_pt _ _) =>
314 cut (True -> continuity_pt p pt);
315 [ intro HYPPD; cut (continuity_pt p pt);
316 [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
318 | |- (derive_pt _ _ _ = _) =>
319 cut (True -> derivable_pt p pt);
320 [ intro HYPPD; cut (derivable_pt p pt);
321 [ intro; clear HYPPD | apply HYPPD; clear HYPPD; trivial ]
333 | |- (derivable_pt Rsqr _) =>
335 (* fonctions de base *)
336 apply derivable_pt_Rsqr
337 | |- (derivable_pt id ?X1) => apply (derivable_pt_id X1)
338 | |- (derivable_pt (fct_cte _) _) => apply derivable_pt_const
339 | |- (derivable_pt sin _) => apply derivable_pt_sin
340 | |- (derivable_pt cos _) => apply derivable_pt_cos
341 | |- (derivable_pt sinh _) => apply derivable_pt_sinh
342 | |- (derivable_pt cosh _) => apply derivable_pt_cosh
343 | |- (derivable_pt exp _) => apply derivable_pt_exp
344 | |- (derivable_pt (pow_fct _) _) =>
345 unfold pow_fct in |- *; apply derivable_pt_pow
346 | |- (derivable_pt sqrt ?X1) =>
347 apply (derivable_pt_sqrt X1);
349 unfold plus_fct, minus_fct, opp_fct, mult_fct, div_fct, inv_fct,
350 comp, id, fct_cte, pow_fct in |- *
351 | |- (derivable_pt Rabs ?X1) =>
352 apply (Rderivable_pt_abs X1);
354 unfold plus_fct, minus_fct, opp_fct, mult_fct, div_fct, inv_fct,
355 comp, id, fct_cte, pow_fct in |- *
356 (* regles de differentiabilite *)
358 | |- (derivable_pt (?X1 + ?X2) ?X3) =>
359 apply (derivable_pt_plus X1 X2 X3); is_diff_pt
361 | |- (derivable_pt (?X1 - ?X2) ?X3) =>
362 apply (derivable_pt_minus X1 X2 X3); is_diff_pt
364 | |- (derivable_pt (- ?X1) ?X2) =>
365 apply (derivable_pt_opp X1 X2);
367 (* MULTIPLICATION PAR UN SCALAIRE *)
368 | |- (derivable_pt (mult_real_fct ?X1 ?X2) ?X3) =>
369 apply (derivable_pt_scal X2 X1 X3); is_diff_pt
371 | |- (derivable_pt (?X1 * ?X2) ?X3) =>
372 apply (derivable_pt_mult X1 X2 X3); is_diff_pt
374 | |- (derivable_pt (?X1 / ?X2) ?X3) =>
375 apply (derivable_pt_div X1 X2 X3);
380 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
381 comp, pow_fct, id, fct_cte in |- * ]
382 | |- (derivable_pt (/ ?X1) ?X2) =>
385 apply (derivable_pt_inv X1 X2);
387 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
388 comp, pow_fct, id, fct_cte in |- *
390 | |- (derivable_pt (comp ?X1 ?X2) ?X3) =>
393 apply (derivable_pt_comp X2 X1 X3); is_diff_pt
394 | _:(derivable_pt ?X1 ?X2) |- (derivable_pt ?X1 ?X2) =>
396 | _:(derivable ?X1) |- (derivable_pt ?X1 ?X2) =>
397 cut (derivable X1); [ intro HypDDPT; apply HypDDPT | assumption ]
398 | |- (True -> derivable_pt _ _) =>
399 intro HypTruE; clear HypTruE; is_diff_pt
402 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
403 fct_cte, comp, pow_fct in |- *
412 | |- (derivable Rsqr) =>
413 (* fonctions de base *)
415 | |- (derivable id) => apply derivable_id
416 | |- (derivable (fct_cte _)) => apply derivable_const
417 | |- (derivable sin) => apply derivable_sin
418 | |- (derivable cos) => apply derivable_cos
419 | |- (derivable cosh) => apply derivable_cosh
420 | |- (derivable sinh) => apply derivable_sinh
421 | |- (derivable exp) => apply derivable_exp
422 | |- (derivable (pow_fct _)) =>
423 unfold pow_fct in |- *;
425 (* regles de differentiabilite *)
427 | |- (derivable (?X1 + ?X2)) =>
428 apply (derivable_plus X1 X2); is_diff_glob
430 | |- (derivable (?X1 - ?X2)) =>
431 apply (derivable_minus X1 X2); is_diff_glob
433 | |- (derivable (- ?X1)) =>
434 apply (derivable_opp X1);
436 (* MULTIPLICATION PAR UN SCALAIRE *)
437 | |- (derivable (mult_real_fct ?X1 ?X2)) =>
438 apply (derivable_scal X2 X1); is_diff_glob
440 | |- (derivable (?X1 * ?X2)) =>
441 apply (derivable_mult X1 X2); is_diff_glob
443 | |- (derivable (?X1 / ?X2)) =>
444 apply (derivable_div X1 X2);
449 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
450 id, fct_cte, comp, pow_fct in |- * ]
451 | |- (derivable (/ ?X1)) =>
454 apply (derivable_inv X1);
457 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
458 id, fct_cte, comp, pow_fct in |- *
460 | |- (derivable (comp sqrt _)) =>
463 unfold derivable in |- *; intro; try is_diff_pt
464 | |- (derivable (comp Rabs _)) =>
465 unfold derivable in |- *; intro; try is_diff_pt
466 | |- (derivable (comp ?X1 ?X2)) =>
467 apply (derivable_comp X2 X1); is_diff_glob
468 | _:(derivable ?X1) |- (derivable ?X1) => assumption
469 | |- (True -> derivable _) =>
470 intro HypTruE; clear HypTruE; is_diff_glob
473 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
474 fct_cte, comp, pow_fct in |- *
483 | |- (continuity_pt Rsqr _) =>
485 (* fonctions de base *)
486 apply derivable_continuous_pt; apply derivable_pt_Rsqr
487 | |- (continuity_pt id ?X1) =>
488 apply derivable_continuous_pt; apply (derivable_pt_id X1)
489 | |- (continuity_pt (fct_cte _) _) =>
490 apply derivable_continuous_pt; apply derivable_pt_const
491 | |- (continuity_pt sin _) =>
492 apply derivable_continuous_pt; apply derivable_pt_sin
493 | |- (continuity_pt cos _) =>
494 apply derivable_continuous_pt; apply derivable_pt_cos
495 | |- (continuity_pt sinh _) =>
496 apply derivable_continuous_pt; apply derivable_pt_sinh
497 | |- (continuity_pt cosh _) =>
498 apply derivable_continuous_pt; apply derivable_pt_cosh
499 | |- (continuity_pt exp _) =>
500 apply derivable_continuous_pt; apply derivable_pt_exp
501 | |- (continuity_pt (pow_fct _) _) =>
502 unfold pow_fct in |- *; apply derivable_continuous_pt;
503 apply derivable_pt_pow
504 | |- (continuity_pt sqrt ?X1) =>
505 apply continuity_pt_sqrt;
507 unfold plus_fct, minus_fct, opp_fct, mult_fct, div_fct, inv_fct,
508 comp, id, fct_cte, pow_fct in |- *
509 | |- (continuity_pt Rabs ?X1) =>
510 apply (Rcontinuity_abs X1)
511 (* regles de differentiabilite *)
513 | |- (continuity_pt (?X1 + ?X2) ?X3) =>
514 apply (continuity_pt_plus X1 X2 X3); is_cont_pt
516 | |- (continuity_pt (?X1 - ?X2) ?X3) =>
517 apply (continuity_pt_minus X1 X2 X3); is_cont_pt
519 | |- (continuity_pt (- ?X1) ?X2) =>
520 apply (continuity_pt_opp X1 X2);
522 (* MULTIPLICATION PAR UN SCALAIRE *)
523 | |- (continuity_pt (mult_real_fct ?X1 ?X2) ?X3) =>
524 apply (continuity_pt_scal X2 X1 X3); is_cont_pt
526 | |- (continuity_pt (?X1 * ?X2) ?X3) =>
527 apply (continuity_pt_mult X1 X2 X3); is_cont_pt
529 | |- (continuity_pt (?X1 / ?X2) ?X3) =>
530 apply (continuity_pt_div X1 X2 X3);
535 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
536 comp, id, fct_cte, pow_fct in |- * ]
537 | |- (continuity_pt (/ ?X1) ?X2) =>
540 apply (continuity_pt_inv X1 X2);
543 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
544 comp, id, fct_cte, pow_fct in |- * ]
545 | |- (continuity_pt (comp ?X1 ?X2) ?X3) =>
548 apply (continuity_pt_comp X2 X1 X3); is_cont_pt
549 | _:(continuity_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
551 | _:(continuity ?X1) |- (continuity_pt ?X1 ?X2) =>
552 cut (continuity X1); [ intro HypDDPT; apply HypDDPT | assumption ]
553 | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
554 apply derivable_continuous_pt; assumption
555 | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) =>
557 [ intro HypDDPT; apply HypDDPT
558 | apply derivable_continuous; assumption ]
559 | |- (True -> continuity_pt _ _) =>
560 intro HypTruE; clear HypTruE; is_cont_pt
563 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
564 fct_cte, comp, pow_fct in |- *
573 | |- (continuity Rsqr) =>
575 (* fonctions de base *)
576 apply derivable_continuous; apply derivable_Rsqr
577 | |- (continuity id) => apply derivable_continuous; apply derivable_id
578 | |- (continuity (fct_cte _)) =>
579 apply derivable_continuous; apply derivable_const
580 | |- (continuity sin) => apply derivable_continuous; apply derivable_sin
581 | |- (continuity cos) => apply derivable_continuous; apply derivable_cos
582 | |- (continuity exp) => apply derivable_continuous; apply derivable_exp
583 | |- (continuity (pow_fct _)) =>
584 unfold pow_fct in |- *; apply derivable_continuous; apply derivable_pow
585 | |- (continuity sinh) =>
586 apply derivable_continuous; apply derivable_sinh
587 | |- (continuity cosh) =>
588 apply derivable_continuous; apply derivable_cosh
589 | |- (continuity Rabs) =>
590 apply Rcontinuity_abs
591 (* regles de continuite *)
593 | |- (continuity (?X1 + ?X2)) =>
594 apply (continuity_plus X1 X2);
595 try is_cont_glob || assumption
597 | |- (continuity (?X1 - ?X2)) =>
598 apply (continuity_minus X1 X2);
599 try is_cont_glob || assumption
601 | |- (continuity (- ?X1)) =>
602 apply (continuity_opp X1); try is_cont_glob || assumption
604 | |- (continuity (/ ?X1)) =>
605 apply (continuity_inv X1);
606 try is_cont_glob || assumption
607 (* MULTIPLICATION PAR UN SCALAIRE *)
608 | |- (continuity (mult_real_fct ?X1 ?X2)) =>
609 apply (continuity_scal X2 X1);
610 try is_cont_glob || assumption
612 | |- (continuity (?X1 * ?X2)) =>
613 apply (continuity_mult X1 X2);
614 try is_cont_glob || assumption
616 | |- (continuity (?X1 / ?X2)) =>
617 apply (continuity_div X1 X2);
618 [ try is_cont_glob || assumption
619 | try is_cont_glob || assumption
622 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
623 id, fct_cte, pow_fct in |- * ]
624 | |- (continuity (comp sqrt _)) =>
627 unfold continuity_pt in |- *; intro; try is_cont_pt
628 | |- (continuity (comp ?X1 ?X2)) =>
629 apply (continuity_comp X2 X1); try is_cont_glob || assumption
630 | _:(continuity ?X1) |- (continuity ?X1) => assumption
631 | |- (True -> continuity _) =>
632 intro HypTruE; clear HypTruE; is_cont_glob
633 | _:(derivable ?X1) |- (continuity ?X1) =>
634 apply derivable_continuous; assumption
637 unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
638 fct_cte, comp, pow_fct in |- *
646 match constr:trm with
648 let p1 := rew_term X1 with p2 := rew_term X2 in
652 | (fct_cte ?X4) => constr:(fct_cte (X3 + X4))
653 | _ => constr:(p1 + p2)%F
655 | _ => constr:(p1 + p2)%F
658 let p1 := rew_term X1 with p2 := rew_term X2 in
662 | (fct_cte ?X4) => constr:(fct_cte (X3 - X4))
663 | _ => constr:(p1 - p2)%F
665 | _ => constr:(p1 - p2)%F
668 let p1 := rew_term X1 with p2 := rew_term X2 in
672 | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
673 | _ => constr:(p1 / p2)%F
677 | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
678 | _ => constr:(p1 / p2)%F
682 let p1 := rew_term X1 with p2 := rew_term X2 in
686 | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
687 | _ => constr:(p1 / p2)%F
691 | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
692 | _ => constr:(p1 / p2)%F
696 let p1 := rew_term X1 with p2 := rew_term X2 in
700 | (fct_cte ?X4) => constr:(fct_cte (X3 * X4))
701 | _ => constr:(p1 * p2)%F
703 | _ => constr:(p1 * p2)%F
706 let p := rew_term X1 in
708 | (fct_cte ?X2) => constr:(fct_cte (- X2))
709 | _ => constr:(- p)%F
712 let p := rew_term X1 in
714 | (fct_cte ?X2) => constr:(fct_cte (/ X2))
715 | _ => constr:(/ p)%F
717 | (?X1 AppVar) => constr:X1
719 let p := rew_term X2 in
721 | (fct_cte ?X3) => constr:(fct_cte (X1 X3))
722 | _ => constr:(comp X1 p)
724 | AppVar => constr:id
725 | (AppVar ^ ?X1) => constr:(pow_fct X1)
727 let p := rew_term X1 in
729 | (fct_cte ?X3) => constr:(fct_cte (pow_fct X2 X3))
730 | _ => constr:(comp (pow_fct X2) p)
732 | ?X1 => constr:(fct_cte X1)
739 Ltac deriv_proof trm pt :=
740 match constr:trm with
742 let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
743 constr:(derivable_pt_plus X1 X2 pt p1 p2)
745 let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
746 constr:(derivable_pt_minus X1 X2 pt p1 p2)
748 let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
749 constr:(derivable_pt_mult X1 X2 pt p1 p2)
752 | id:(?X2 pt <> 0) |- _ =>
753 let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
754 constr:(derivable_pt_div X1 X2 pt p1 p2 id)
759 | id:(?X1 pt <> 0) |- _ =>
760 let p1 := deriv_proof X1 pt in
761 constr:(derivable_pt_inv X1 pt p1 id)
765 let pt_f1 := eval cbv beta in (X2 pt) in
766 let p1 := deriv_proof X1 pt_f1 with p2 := deriv_proof X2 pt in
767 constr:(derivable_pt_comp X2 X1 pt p2 p1)
769 let p1 := deriv_proof X1 pt in
770 constr:(derivable_pt_opp X1 pt p1)
771 | sin => constr:(derivable_pt_sin pt)
772 | cos => constr:(derivable_pt_cos pt)
773 | sinh => constr:(derivable_pt_sinh pt)
774 | cosh => constr:(derivable_pt_cosh pt)
775 | exp => constr:(derivable_pt_exp pt)
776 | id => constr:(derivable_pt_id pt)
777 | Rsqr => constr:(derivable_pt_Rsqr pt)
780 | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id)
783 | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt)
785 let aux := constr:X1 in
787 | id:(derivable_pt aux pt) |- _ => constr:id
788 | id:(derivable aux) |- _ => constr:(id pt)
797 Ltac simplify_derive trm pt :=
798 match constr:trm with
800 try rewrite derive_pt_plus; simplify_derive X1 pt;
801 simplify_derive X2 pt
803 try rewrite derive_pt_minus; simplify_derive X1 pt;
804 simplify_derive X2 pt
806 try rewrite derive_pt_mult; simplify_derive X1 pt;
807 simplify_derive X2 pt
809 try rewrite derive_pt_div; simplify_derive X1 pt; simplify_derive X2 pt
811 let pt_f1 := eval cbv beta in (X2 pt) in
812 (try rewrite derive_pt_comp; simplify_derive X1 pt_f1;
813 simplify_derive X2 pt)
814 | (- ?X1)%F => try rewrite derive_pt_opp; simplify_derive X1 pt
816 try rewrite derive_pt_inv; simplify_derive X1 pt
817 | (fct_cte ?X1) => try rewrite derive_pt_const
818 | id => try rewrite derive_pt_id
819 | sin => try rewrite derive_pt_sin
820 | cos => try rewrite derive_pt_cos
821 | sinh => try rewrite derive_pt_sinh
822 | cosh => try rewrite derive_pt_cosh
823 | exp => try rewrite derive_pt_exp
824 | Rsqr => try rewrite derive_pt_Rsqr
825 | sqrt => try rewrite derive_pt_sqrt
827 let aux := constr:X1 in
829 | id:(derive_pt aux pt ?X2 = _),H:(derivable aux) |- _ =>
830 try replace (derive_pt aux pt (H pt)) with (derive_pt aux pt X2);
831 [ rewrite id | apply pr_nu ]
832 | id:(derive_pt aux pt ?X2 = _),H:(derivable_pt aux pt) |- _ =>
833 try replace (derive_pt aux pt H) with (derive_pt aux pt X2);
834 [ rewrite id | apply pr_nu ]
846 | |- (derivable_pt ?X1 ?X2) =>
847 let trm := eval cbv beta in (X1 AppVar) in
848 let aux := rew_term trm in
849 (intro_hyp_pt aux X2;
850 try (change (derivable_pt aux X2) in |- *; is_diff_pt) || is_diff_pt)
851 | |- (derivable ?X1) =>
852 let trm := eval cbv beta in (X1 AppVar) in
853 let aux := rew_term trm in
855 try (change (derivable aux) in |- *; is_diff_glob) || is_diff_glob)
856 | |- (continuity ?X1) =>
857 let trm := eval cbv beta in (X1 AppVar) in
858 let aux := rew_term trm in
860 try (change (continuity aux) in |- *; is_cont_glob) || is_cont_glob)
861 | |- (continuity_pt ?X1 ?X2) =>
862 let trm := eval cbv beta in (X1 AppVar) in
863 let aux := rew_term trm in
864 (intro_hyp_pt aux X2;
865 try (change (continuity_pt aux X2) in |- *; is_cont_pt) || is_cont_pt)
866 | |- (derive_pt ?X1 ?X2 ?X3 = ?X4) =>
867 let trm := eval cbv beta in (X1 AppVar) in
868 let aux := rew_term trm in
869 (intro_hyp_pt aux X2;
870 let aux2 := deriv_proof aux X2 in
872 (replace (derive_pt X1 X2 X3) with (derive_pt aux X2 aux2);
873 [ simplify_derive aux X2;
875 unfold plus_fct, minus_fct, mult_fct, div_fct, id, fct_cte,
876 inv_fct, opp_fct in |- *; try ring
877 | try apply pr_nu ]) || is_diff_pt))