helm/gTopLevel/eliminationTactics.ml

   1 (* Copyright (C) 2002, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (*
  27 let induction_tac ~term ~status:((proof,goal) as status) =
  28   let module C = Cic in
  29   let module R = CicReduction in
  30   let module P = PrimitiveTactics in
  31   let module T = Tacticals in
  32   let module S = ProofEngineStructuralRules in
  33   let module U = UriManager in
  34    let (_,metasenv,_,_) = proof in
  35     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
  36      let termty = T.type_of_aux' metasenv context term in
  37      let uri,exp_named_subst,typeno,args =
  38       match termty with
  39          C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
  40        | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) -> (uri,exp_named_subst,typeno,args)
  41        | _ -> raise (ProofEngineTypes.Fail "Induction: Not an Inductive Type to Eliminate")
  42      in
  43       let eliminator_uri =
  44        let base = U.buri_of_uri uri in
  45        let name =
  46         match CicEnvironment.get_obj uri with
  47            C.InductiveDefinition (tys,_,_) ->
  48             let (name,_,_,_) = List.nth tys typeno in
  49              name
  50          | _ -> assert false
  51        in
  52        let ext =
  53         match T.type_of_aux' metasenv context ty with
  54            C.Sort C.Prop -> "_ind"
  55          | C.Sort C.Set  -> "_rec"
  56          | C.Sort C.Type -> "_rect"
  57          | _ -> assert false
  58        in
  59         U.uri_of_string (base ^ "/" ^ name ^ ext ^ ".con")
  60       in
  61        apply_tac ~term:(C.Const (eliminator_uri , exp_named_subst))     (* come mi devo comportare con gli args??? *)
  62 ;;
  63 *)
  64
  65 let elim_type_tac ~term ~status =
  66   let module C = Cic in
  67   let module P = PrimitiveTactics in
  68   let module T = Tacticals in
  69    T.thens
  70     ~start: (P.cut_tac ~term)
  71     ~continuations:[ P.elim_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
  72     ~status
  73 ;;
  74
  75 (* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-)
  76 let elim_type_tac ~term ~status =
  77   warn "in Ring.elim_type_tac";
  78   Tacticals.thens ~start:(cut_tac ~term)
  79    ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
  80 *)
  81
  82
  83 (* PROVE DI DECOMPOSE
  84
  85 (* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *)
  86 let decompose_tac ~what ~where ~status:((proof,goal) as status) =
  87   let module C = Cic in
  88   let module R = CicReduction in
  89   let module P = PrimitiveTactics in
  90   let module T = Tacticals in
  91   let module S = ProofEngineStructuralRules in
  92
  93    let rec decomposing ty what =
  94     match (what) with
  95        [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *)
  96      | hd::tl as what ->
  97         match ty with
  98            (C.Appl (hd::_)) -> hd
  99          | _ -> decomposing ty tl
 100     in
 101
 102    let (_,metasenv,_,_) = proof in
 103     let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
 104      T.repeat_tactic
 105        ~tactic:(T.then_
 106                    ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what))
 107                    ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where))))                (* ma che ipotesi sto cancellando??? *)
 108                )
 109        ~status
 110 ;;
 111
 112
 113 let decompose_tac ~clist ~status:((proof,goal) as status) =
 114   let module C = Cic in
 115   let module R = CicReduction in
 116   let module P = PrimitiveTactics in
 117   let module T = Tacticals in
 118   let module S = ProofEngineStructuralRules in
 119    let (_,metasenv,_,_) = proof in
 120     let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 121
 122      let rec repeat_elim ~term ~status =                (* term -> status -> proof * (goal list) *)
 123       try
 124        let (proof, goallist) =
 125         T.then_
 126            ~start:(P.elim_simpl_intros_tac ~term)
 127            ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty))))                (* non so che ipotesi sto cancellando??? *)
 128            ~status
 129         in
 130          let rec step proof goallist =
 131           match goallist with
 132              [] -> (proof, [])
 133            | hd::tl ->
 134               let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in
 135                let (proof'', goallist'') = step proof' tl in
 136                 proof'', goallist'@goallist''
 137           in
 138            step proof goallist
 139        with
 140         (Fail _) -> T.id_tac
 141
 142     in
 143                                                                   let rec decomposing ty clist =             (* term -> (term list) -> bool *)
 144       match (clist) with
 145         [] -> false
 146       | hd::tl as clist ->
 147          match ty with
 148            (C.Appl (hd::_)) -> true
 149          | _ -> decomposing ty tl
 150
 151       in
 152        let term = decomposing (R.whd context ty) clist in
 153         if (term == C.Implicit)
 154          then (Fail "Decompose: nothing to decompose or no application")
 155          else repeat_elim ~term ~status
 156 ;;
 157 *)
 158
 159 let decompose_tac ~clist ~status =
 160   let module C = Cic in
 161   let module R = CicReduction in
 162   let module P = PrimitiveTactics in
 163   let module T = Tacticals in
 164   let module S = ProofEngineStructuralRules in
 165
 166    let rec choose ty =
 167     function
 168        [] -> C.Implicit (* a cosa serve? *)
 169      | hd::tl ->
 170         match ty with
 171            (C.Appl (hd::_)) -> hd
 172          | _ -> choose ty tl
 173      in
 174
 175     let decompose_one_tac ~clist ~status:((proof,goal) as status) =
 176      let (_,metasenv,_,_) = proof in
 177       let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 178        let term = choose (R.whd context ty) clist in
 179         if (term == C.Implicit)
 180          then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
 181          else T.then_
 182                  ~start:(P.elim_intros_simpl_tac ~term)
 183                  ~continuation:(S.clear ~hyp:(List.hd context))
 184 (*                              (S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty))))                (* ma che ipotesi sto cancellando??? *)*)
 185                  ~status
 186      in
 187       T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status
 188 ;;
 189
 190