helm/software/matita/contribs/procedural/Coq/Reals/Ranalysis.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: Ranalysis.v,v 1.19.2.1 2004/07/16 19:31:12 herbelin Exp $ i*)
  34
  35 include "Reals/Rbase.ma".
  36
  37 include "Reals/Rfunctions.ma".
  38
  39 include "Reals/Rtrigo.ma".
  40
  41 include "Reals/SeqSeries.ma".
  42
  43 include "Reals/Ranalysis1.ma".
  44
  45 include "Reals/Ranalysis2.ma".
  46
  47 include "Reals/Ranalysis3.ma".
  48
  49 include "Reals/Rtopology.ma".
  50
  51 include "Reals/MVT.ma".
  52
  53 include "Reals/PSeries_reg.ma".
  54
  55 include "Reals/Exp_prop.ma".
  56
  57 include "Reals/Rtrigo_reg.ma".
  58
  59 include "Reals/Rsqrt_def.ma".
  60
  61 include "Reals/R_sqrt.ma".
  62
  63 include "Reals/Rtrigo_calc.ma".
  64
  65 include "Reals/Rgeom.ma".
  66
  67 include "Reals/RList.ma".
  68
  69 include "Reals/Sqrt_reg.ma".
  70
  71 include "Reals/Ranalysis4.ma".
  72
  73 include "Reals/Rpower.ma".
  74
  75 (* UNEXPORTED
  76 Open Local Scope R_scope.
  77 *)
  78
  79 inline procedural "cic:/Coq/Reals/Ranalysis/AppVar.con".
  80
  81 (*#*********)
  82
  83 (* UNEXPORTED
  84 Ltac intro_hyp_glob trm :=
  85   match constr:trm with
  86   | (?X1 + ?X2)%F =>
  87       match goal with
  88       |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
  89       |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
  90       | _ => idtac
  91       end
  92   | (?X1 - ?X2)%F =>
  93       match goal with
  94       |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
  95       |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
  96       | _ => idtac
  97       end
  98   | (?X1 * ?X2)%F =>
  99       match goal with
 100       |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
 101       |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
 102       | _ => idtac
 103       end
 104   | (?X1 / ?X2)%F =>
 105       let aux := constr:X2 in
 106       match goal with
 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 ]
 117       | _ => idtac
 118       end
 119   | (comp ?X1 ?X2) =>
 120       match goal with
 121       |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
 122       |  |- (continuity _) => intro_hyp_glob X1; intro_hyp_glob X2
 123       | _ => idtac
 124       end
 125   | (- ?X1)%F =>
 126       match goal with
 127       |  |- (derivable _) => intro_hyp_glob X1
 128       |  |- (continuity _) => intro_hyp_glob X1
 129       | _ => idtac
 130       end
 131   | (/ ?X1)%F =>
 132       let aux := constr:X1 in
 133       match goal with
 134       | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
 135           intro_hyp_glob X1
 136       | _:(forall x0:R, aux x0 <> 0) |- (continuity _) =>
 137       intro_hyp_glob X1
 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 ]
 144       | _ => idtac
 145       end
 146   | cos => idtac
 147   | sin => idtac
 148   | cosh => idtac
 149   | sinh => idtac
 150   | exp => idtac
 151   | Rsqr => idtac
 152   | sqrt => idtac
 153   | id => idtac
 154   | (fct_cte _) => idtac
 155   | (pow_fct _) => idtac
 156   | Rabs => idtac
 157   | ?X1 =>
 158       let p := constr:X1 in
 159       match goal with
 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 ]
 166            | idtac ]
 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 ]
 173            | idtac ]
 174       | _ => idtac
 175       end
 176   end.
 177 *)
 178
 179 (*#*********)
 180
 181 (* UNEXPORTED
 182 Ltac intro_hyp_pt trm pt :=
 183   match constr:trm with
 184   | (?X1 + ?X2)%F =>
 185       match goal 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
 190       | _ => idtac
 191       end
 192   | (?X1 - ?X2)%F =>
 193       match goal with
 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
 198       | _ => idtac
 199       end
 200   | (?X1 * ?X2)%F =>
 201       match goal with
 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
 206       | _ => idtac
 207       end
 208   | (?X1 / ?X2)%F =>
 209       let aux := constr:X2 in
 210       match goal with
 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 _ _) =>
 224           cut (aux pt <> 0);
 225            [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
 226       |  |- (continuity_pt _ _) =>
 227           cut (aux pt <> 0);
 228            [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
 229       |  |- (derive_pt _ _ _ = _) =>
 230           cut (aux pt <> 0);
 231            [ intro; intro_hyp_pt X1 pt; intro_hyp_pt X2 pt | try assumption ]
 232       | _ => idtac
 233       end
 234   | (comp ?X1 ?X2) =>
 235       match goal with
 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)
 245       | _ => idtac
 246       end
 247   | (- ?X1)%F =>
 248       match goal with
 249       |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt
 250       |  |- (continuity_pt _ _) => intro_hyp_pt X1 pt
 251       |  |- (derive_pt _ _ _ = _) => intro_hyp_pt X1 pt
 252       | _ => idtac
 253       end
 254   | (/ ?X1)%F =>
 255       let aux := constr:X1 in
 256       match goal with
 257       | _:(aux pt <> 0) |- (derivable_pt _ _) =>
 258           intro_hyp_pt X1 pt
 259       | _:(aux pt <> 0) |- (continuity_pt _ _) =>
 260           intro_hyp_pt X1 pt
 261       | _:(aux pt <> 0) |- (derive_pt _ _ _ = _) =>
 262           intro_hyp_pt X1 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 ]
 275       | _ => idtac
 276       end
 277   | cos => idtac
 278   | sin => idtac
 279   | cosh => idtac
 280   | sinh => idtac
 281   | exp => idtac
 282   | Rsqr => idtac
 283   | id => idtac
 284   | (fct_cte _) => idtac
 285   | (pow_fct _) => idtac
 286   | sqrt =>
 287       match goal with
 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 ]
 293       | _ => idtac
 294       end
 295   | Rabs =>
 296       match goal with
 297       |  |- (derivable_pt _ _) =>
 298           cut (pt <> 0); [ intro | try assumption ]
 299       | _ => idtac
 300       end
 301   | ?X1 =>
 302       let p := constr:X1 in
 303       match goal with
 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 ]
 310            | idtac ]
 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 ]
 317            | idtac ]
 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 ]
 322            | idtac ]
 323       | _ => idtac
 324       end
 325   end.
 326 *)
 327
 328 (*#*********)
 329
 330 (* UNEXPORTED
 331 Ltac is_diff_pt :=
 332   match goal with
 333   |  |- (derivable_pt Rsqr _) =>
 334
 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);
 348        assumption ||
 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);
 353        assumption ||
 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 *)
 357         (* PLUS *)
 358   |  |- (derivable_pt (?X1 + ?X2) ?X3) =>
 359       apply (derivable_pt_plus X1 X2 X3); is_diff_pt
 360        (* MOINS *)
 361   |  |- (derivable_pt (?X1 - ?X2) ?X3) =>
 362       apply (derivable_pt_minus X1 X2 X3); is_diff_pt
 363        (* OPPOSE *)
 364   |  |- (derivable_pt (- ?X1) ?X2) =>
 365       apply (derivable_pt_opp X1 X2);
 366        is_diff_pt
 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
 370        (* MULTIPLICATION *)
 371   |  |- (derivable_pt (?X1 * ?X2) ?X3) =>
 372       apply (derivable_pt_mult X1 X2 X3); is_diff_pt
 373        (* DIVISION *)
 374   |  |- (derivable_pt (?X1 / ?X2) ?X3) =>
 375       apply (derivable_pt_div X1 X2 X3);
 376        [ is_diff_pt
 377        | is_diff_pt
 378        | try
 379           assumption ||
 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) =>
 383
 384        (* INVERSION *)
 385        apply (derivable_pt_inv X1 X2);
 386        [ assumption ||
 387            unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
 388             comp, pow_fct, id, fct_cte in |- *
 389        | is_diff_pt ]
 390   |  |- (derivable_pt (comp ?X1 ?X2) ?X3) =>
 391
 392        (* COMPOSITION *)
 393        apply (derivable_pt_comp X2 X1 X3); is_diff_pt
 394   | _:(derivable_pt ?X1 ?X2) |- (derivable_pt ?X1 ?X2) =>
 395       assumption
 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
 400   | _ =>
 401       try
 402        unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
 403         fct_cte, comp, pow_fct in |- *
 404   end.
 405 *)
 406
 407 (*#*********)
 408
 409 (* UNEXPORTED
 410 Ltac is_diff_glob :=
 411   match goal with
 412   |  |- (derivable Rsqr) =>
 413   (* fonctions de base *)
 414   apply derivable_Rsqr
 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 |- *;
 424        apply derivable_pow
 425         (* regles de differentiabilite *)
 426         (* PLUS *)
 427   |  |- (derivable (?X1 + ?X2)) =>
 428       apply (derivable_plus X1 X2); is_diff_glob
 429        (* MOINS *)
 430   |  |- (derivable (?X1 - ?X2)) =>
 431       apply (derivable_minus X1 X2); is_diff_glob
 432        (* OPPOSE *)
 433   |  |- (derivable (- ?X1)) =>
 434       apply (derivable_opp X1);
 435        is_diff_glob
 436        (* MULTIPLICATION PAR UN SCALAIRE *)
 437   |  |- (derivable (mult_real_fct ?X1 ?X2)) =>
 438       apply (derivable_scal X2 X1); is_diff_glob
 439        (* MULTIPLICATION *)
 440   |  |- (derivable (?X1 * ?X2)) =>
 441       apply (derivable_mult X1 X2); is_diff_glob
 442        (* DIVISION *)
 443   |  |- (derivable (?X1 / ?X2)) =>
 444       apply (derivable_div X1 X2);
 445        [ is_diff_glob
 446        | is_diff_glob
 447        | try
 448           assumption ||
 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)) =>
 452
 453        (* INVERSION *)
 454        apply (derivable_inv X1);
 455        [ try
 456           assumption ||
 457             unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct,
 458              id, fct_cte, comp, pow_fct in |- *
 459        | is_diff_glob ]
 460   |  |- (derivable (comp sqrt _)) =>
 461
 462        (* COMPOSITION *)
 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
 471   | _ =>
 472       try
 473        unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
 474         fct_cte, comp, pow_fct in |- *
 475   end.
 476 *)
 477
 478 (*#*********)
 479
 480 (* UNEXPORTED
 481 Ltac is_cont_pt :=
 482   match goal with
 483   |  |- (continuity_pt Rsqr _) =>
 484
 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;
 506        assumption ||
 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 *)
 512        (* PLUS *)
 513   |  |- (continuity_pt (?X1 + ?X2) ?X3) =>
 514       apply (continuity_pt_plus X1 X2 X3); is_cont_pt
 515        (* MOINS *)
 516   |  |- (continuity_pt (?X1 - ?X2) ?X3) =>
 517       apply (continuity_pt_minus X1 X2 X3); is_cont_pt
 518        (* OPPOSE *)
 519   |  |- (continuity_pt (- ?X1) ?X2) =>
 520       apply (continuity_pt_opp X1 X2);
 521        is_cont_pt
 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
 525        (* MULTIPLICATION *)
 526   |  |- (continuity_pt (?X1 * ?X2) ?X3) =>
 527       apply (continuity_pt_mult X1 X2 X3); is_cont_pt
 528        (* DIVISION *)
 529   |  |- (continuity_pt (?X1 / ?X2) ?X3) =>
 530       apply (continuity_pt_div X1 X2 X3);
 531        [ is_cont_pt
 532        | is_cont_pt
 533        | try
 534           assumption ||
 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) =>
 538
 539        (* INVERSION *)
 540        apply (continuity_pt_inv X1 X2);
 541        [ is_cont_pt
 542        | assumption ||
 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) =>
 546
 547        (* COMPOSITION *)
 548        apply (continuity_pt_comp X2 X1 X3); is_cont_pt
 549   | _:(continuity_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
 550       assumption
 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) =>
 556       cut (continuity X1);
 557        [ intro HypDDPT; apply HypDDPT
 558        | apply derivable_continuous; assumption ]
 559   |  |- (True -> continuity_pt _ _) =>
 560       intro HypTruE; clear HypTruE; is_cont_pt
 561   | _ =>
 562       try
 563        unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
 564         fct_cte, comp, pow_fct in |- *
 565   end.
 566 *)
 567
 568 (*#*********)
 569
 570 (* UNEXPORTED
 571 Ltac is_cont_glob :=
 572   match goal with
 573   |  |- (continuity Rsqr) =>
 574
 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 *)
 592        (* PLUS *)
 593   |  |- (continuity (?X1 + ?X2)) =>
 594       apply (continuity_plus X1 X2);
 595        try is_cont_glob || assumption
 596             (* MOINS *)
 597   |  |- (continuity (?X1 - ?X2)) =>
 598       apply (continuity_minus X1 X2);
 599        try is_cont_glob || assumption
 600             (* OPPOSE *)
 601   |  |- (continuity (- ?X1)) =>
 602       apply (continuity_opp X1); try is_cont_glob || assumption
 603                                       (* INVERSE *)
 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
 611             (* MULTIPLICATION *)
 612   |  |- (continuity (?X1 * ?X2)) =>
 613       apply (continuity_mult X1 X2);
 614        try is_cont_glob || assumption
 615             (* DIVISION *)
 616   |  |- (continuity (?X1 / ?X2)) =>
 617       apply (continuity_div X1 X2);
 618        [ try is_cont_glob || assumption
 619        | try is_cont_glob || assumption
 620        | try
 621           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 _)) =>
 625
 626        (* COMPOSITION *)
 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
 635   | _ =>
 636       try
 637        unfold plus_fct, mult_fct, div_fct, minus_fct, opp_fct, inv_fct, id,
 638         fct_cte, comp, pow_fct in |- *
 639   end.
 640 *)
 641
 642 (*#*********)
 643
 644 (* UNEXPORTED
 645 Ltac rew_term trm :=
 646   match constr:trm with
 647   | (?X1 + ?X2) =>
 648       let p1 := rew_term X1 with p2 := rew_term X2 in
 649       match constr:p1 with
 650       | (fct_cte ?X3) =>
 651           match constr:p2 with
 652           | (fct_cte ?X4) => constr:(fct_cte (X3 + X4))
 653           | _ => constr:(p1 + p2)%F
 654           end
 655       | _ => constr:(p1 + p2)%F
 656       end
 657   | (?X1 - ?X2) =>
 658       let p1 := rew_term X1 with p2 := rew_term X2 in
 659       match constr:p1 with
 660       | (fct_cte ?X3) =>
 661           match constr:p2 with
 662           | (fct_cte ?X4) => constr:(fct_cte (X3 - X4))
 663           | _ => constr:(p1 - p2)%F
 664           end
 665       | _ => constr:(p1 - p2)%F
 666       end
 667   | (?X1 / ?X2) =>
 668       let p1 := rew_term X1 with p2 := rew_term X2 in
 669       match constr:p1 with
 670       | (fct_cte ?X3) =>
 671           match constr:p2 with
 672           | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
 673           | _ => constr:(p1 / p2)%F
 674           end
 675       | _ =>
 676           match constr:p2 with
 677           | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
 678           | _ => constr:(p1 / p2)%F
 679           end
 680       end
 681   | (?X1 * / ?X2) =>
 682       let p1 := rew_term X1 with p2 := rew_term X2 in
 683       match constr:p1 with
 684       | (fct_cte ?X3) =>
 685           match constr:p2 with
 686           | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
 687           | _ => constr:(p1 / p2)%F
 688           end
 689       | _ =>
 690           match constr:p2 with
 691           | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
 692           | _ => constr:(p1 / p2)%F
 693           end
 694       end
 695   | (?X1 * ?X2) =>
 696       let p1 := rew_term X1 with p2 := rew_term X2 in
 697       match constr:p1 with
 698       | (fct_cte ?X3) =>
 699           match constr:p2 with
 700           | (fct_cte ?X4) => constr:(fct_cte (X3 * X4))
 701           | _ => constr:(p1 * p2)%F
 702           end
 703       | _ => constr:(p1 * p2)%F
 704       end
 705   | (- ?X1) =>
 706       let p := rew_term X1 in
 707       match constr:p with
 708       | (fct_cte ?X2) => constr:(fct_cte (- X2))
 709       | _ => constr:(- p)%F
 710       end
 711   | (/ ?X1) =>
 712       let p := rew_term X1 in
 713       match constr:p with
 714       | (fct_cte ?X2) => constr:(fct_cte (/ X2))
 715       | _ => constr:(/ p)%F
 716       end
 717   | (?X1 AppVar) => constr:X1
 718   | (?X1 ?X2) =>
 719       let p := rew_term X2 in
 720       match constr:p with
 721       | (fct_cte ?X3) => constr:(fct_cte (X1 X3))
 722       | _ => constr:(comp X1 p)
 723       end
 724   | AppVar => constr:id
 725   | (AppVar ^ ?X1) => constr:(pow_fct X1)
 726   | (?X1 ^ ?X2) =>
 727       let p := rew_term X1 in
 728       match constr:p with
 729       | (fct_cte ?X3) => constr:(fct_cte (pow_fct X2 X3))
 730       | _ => constr:(comp (pow_fct X2) p)
 731       end
 732   | ?X1 => constr:(fct_cte X1)
 733   end.
 734 *)
 735
 736 (*#*********)
 737
 738 (* UNEXPORTED
 739 Ltac deriv_proof trm pt :=
 740   match constr:trm with
 741   | (?X1 + ?X2)%F =>
 742       let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
 743       constr:(derivable_pt_plus X1 X2 pt p1 p2)
 744   | (?X1 - ?X2)%F =>
 745       let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
 746       constr:(derivable_pt_minus X1 X2 pt p1 p2)
 747   | (?X1 * ?X2)%F =>
 748       let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
 749       constr:(derivable_pt_mult X1 X2 pt p1 p2)
 750   | (?X1 / ?X2)%F =>
 751       match goal with
 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)
 755       | _ => constr:False
 756       end
 757   | (/ ?X1)%F =>
 758       match goal with
 759       | id:(?X1 pt <> 0) |- _ =>
 760           let p1 := deriv_proof X1 pt in
 761           constr:(derivable_pt_inv X1 pt p1 id)
 762       | _ => constr:False
 763       end
 764   | (comp ?X1 ?X2) =>
 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)
 768   | (- ?X1)%F =>
 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)
 778   | sqrt =>
 779       match goal with
 780       | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id)
 781       | _ => constr:False
 782       end
 783   | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt)
 784   | ?X1 =>
 785       let aux := constr:X1 in
 786       match goal with
 787       | id:(derivable_pt aux pt) |- _ => constr:id
 788       | id:(derivable aux) |- _ => constr:(id pt)
 789       | _ => constr:False
 790       end
 791   end.
 792 *)
 793
 794 (*#*********)
 795
 796 (* UNEXPORTED
 797 Ltac simplify_derive trm pt :=
 798   match constr:trm with
 799   | (?X1 + ?X2)%F =>
 800       try rewrite derive_pt_plus; simplify_derive X1 pt;
 801        simplify_derive X2 pt
 802   | (?X1 - ?X2)%F =>
 803       try rewrite derive_pt_minus; simplify_derive X1 pt;
 804        simplify_derive X2 pt
 805   | (?X1 * ?X2)%F =>
 806       try rewrite derive_pt_mult; simplify_derive X1 pt;
 807        simplify_derive X2 pt
 808   | (?X1 / ?X2)%F =>
 809       try rewrite derive_pt_div; simplify_derive X1 pt; simplify_derive X2 pt
 810   | (comp ?X1 ?X2) =>
 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
 815   | (/ ?X1)%F =>
 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
 826   | ?X1 =>
 827       let aux := constr:X1 in
 828       match goal with
 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 ]
 835       | _ => idtac
 836       end
 837   | _ => idtac
 838   end.
 839 *)
 840
 841 (*#*********)
 842
 843 (* UNEXPORTED
 844 Ltac reg :=
 845   match goal with
 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
 854       (intro_hyp_glob aux;
 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
 859       (intro_hyp_glob aux;
 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
 871         (try
 872           (replace (derive_pt X1 X2 X3) with (derive_pt aux X2 aux2);
 873             [ simplify_derive aux X2;
 874                try
 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))
 878   end.
 879 *)
 880