helm/software/matita/contribs/CoRN-Decl/tactics/DiffTactics3.ma

   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 set "baseuri" "cic:/matita/CoRN-Decl/tactics/DiffTactics3".
  18
  19 (* $Id: DiffTactics3.v,v 1.1.1.1 2004/02/05 16:25:44 lionelm Exp $ *)
  20
  21 (* begin hide *)
  22
  23 (* INCLUDE
  24 MoreFunSeries
  25 *)
  26
  27 (* INCLUDE
  28 Composition
  29 *)
  30
  31 (* INCLUDE
  32 DiffTactics2
  33 *)
  34
  35 (* UNEXPORTED
  36 Ltac Deriv_substR :=
  37   match goal with
  38   |  |- (Derivative ?X1 _) =>
  39       let t := derivative_of X1 in
  40       apply Derivative_wdr with t
  41   end.
  42 *)
  43
  44 inline cic:/CoRN/tactics/DiffTactics3/symbPF.ind.
  45
  46 (*
  47   | ssum0     : nat->(nat->symbPF)->symbPF
  48   | ssumx     : (n:nat)((i:nat)(lt i n)->symbPF)->symbPF
  49   | ssum      : nat->nat->(nat->symbPF)->symbPF
  50 *)
  51
  52 inline cic:/CoRN/tactics/DiffTactics3/symb_to_PartIR.con.
  53
  54 inline cic:/CoRN/tactics/DiffTactics3/symbPF_deriv.con.
  55
  56 (* UNEXPORTED
  57 Ltac PartIR_to_symbPF f :=
  58   match constr:f with
  59   | ([-C-]?X3) => constr:(sconst X3)
  60   | FId => constr:sid
  61   | (?X3{+}?X4) =>
  62       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
  63       constr:(splus t1 t2)
  64   | ({--}?X3) =>
  65       let t1 := PartIR_to_symbPF X3 in
  66       constr:(sinv t1)
  67   | (?X3{-}?X4) =>
  68       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
  69       constr:(sminus t1 t2)
  70   | (?X3{*}?X4) =>
  71       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
  72       constr:(smult t1 t2)
  73   | (?X3{**}?X4) =>
  74       let t := PartIR_to_symbPF X4 in
  75       constr:(sscalmult X3 t)
  76   | (?X3{^}?X4) =>
  77       let t1 := PartIR_to_symbPF X3 in
  78       constr:(snth t1 X4)
  79   | ({1/}?X3) =>
  80       let t1 := PartIR_to_symbPF X3 in
  81       constr:(srecip t1)
  82   | (?X3{/}?X4) =>
  83       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
  84       constr:(sdiv t1 t2)
  85   | (?X3[o]?X4) =>
  86       let t1 := PartIR_to_symbPF X3 with t2 := PartIR_to_symbPF X4 in
  87       constr:(scomp t1 t2)
  88   | ?X3 =>
  89       let t := constr:X3 in
  90       match goal with
  91       | H:(Derivative ?X1 ?X2 t ?X4) |- _ =>
  92           constr:(shyp X1 X2 t X4 H)
  93       | H:(Diffble ?X1 ?X2 t) |- _ => constr:(shyp' X1 X2 t H)
  94       end
  95   end.
  96 *)
  97
  98 (* UNEXPORTED
  99 Ltac Derivative_Help :=
 100   match goal with
 101   |  |- (Derivative ?X1 ?X2 ?X3 ?X4) =>
 102       let r := PartIR_to_symbPF X3 in
 103       (apply Derivative_wdr with (symbPF_deriv r);
 104         [ unfold symbPF_deriv, symb_to_PartIR in |- *
 105         | simpl in |- *; Deriv ])
 106   end.
 107 *)
 108
 109 (* end hide *)
 110