helm/ocaml/tactics/equalityTactics.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 let rewrite_tac ~term:equality =
  27   let rewrite_tac ~term:equality (proof,goal) =
  28     let module C = Cic in
  29     let module U = UriManager in
  30     let curi,metasenv,pbo,pty = proof in
  31     let metano,context,gty = CicUtil.lookup_meta goal metasenv in
  32     let ty_eq,_ =
  33       CicTypeChecker.type_of_aux' metasenv context equality
  34         CicUniv.empty_ugraph in
  35     let eq_ind_r,ty,t1,t2 =
  36       match ty_eq with
  37         C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
  38          when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
  39           let eq_ind_r =
  40            C.Const
  41             (HelmLibraryObjects.Logic.eq_ind_r_URI,[])
  42           in
  43            eq_ind_r,ty,t1,t2
  44       | _ ->
  45         raise
  46          (ProofEngineTypes.Fail
  47            "Rewrite: the argument is not a proof of an equality")
  48     in
  49      let pred =
  50       let gty' = CicSubstitution.lift 1 gty in
  51       let t1' = CicSubstitution.lift 1 t1 in
  52       let gty'' =
  53        ProofEngineReduction.replace_lifting
  54         ~equality:ProofEngineReduction.alpha_equivalence
  55         ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
  56       in
  57        C.Lambda
  58         (FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context C.Anonymous ~typ:ty,
  59           ty, gty'')
  60      in
  61      let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
  62      let irl =CicMkImplicit.identity_relocation_list_for_metavariable context in
  63      let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
  64
  65       let (proof',goals) =
  66        ProofEngineTypes.apply_tactic
  67         (PrimitiveTactics.exact_tac
  68          ~term:(C.Appl
  69           [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]))        ((curi,metasenv',pbo,pty),goal)
  70       in
  71        assert (List.length goals = 0) ;
  72         (proof',[fresh_meta])
  73   in
  74     ProofEngineTypes.mk_tactic (rewrite_tac ~term:equality)
  75 ;;
  76
  77
  78 let rewrite_simpl_tac ~term =
  79  let rewrite_simpl_tac ~term status =
  80   ProofEngineTypes.apply_tactic
  81   (Tacticals.then_
  82    ~start:(rewrite_tac ~term)
  83    ~continuation:
  84     (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
  85    status
  86  in
  87    ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
  88 ;;
  89
  90
  91 let rewrite_back_tac ~term:equality =
  92  let rewrite_back_tac equality (proof,goal) =
  93   let module C = Cic in
  94   let module U = UriManager in
  95    let curi,metasenv,pbo,pty = proof in
  96    let metano,context,gty = CicUtil.lookup_meta goal metasenv in
  97    let ty_eq,_ =
  98      CicTypeChecker.type_of_aux' metasenv context equality
  99        CicUniv.empty_ugraph in
 100     let eq_ind_r,ty,t1,t2 =
 101      match ty_eq with
 102         C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
 103          when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
 104           let eq_ind_r =
 105            C.Const (HelmLibraryObjects.Logic.eq_ind_URI,[])
 106           in
 107            eq_ind_r,ty,t2,t1
 108       | _ ->
 109         raise
 110          (ProofEngineTypes.Fail
 111            "Rewrite: the argument is not a proof of an equality")
 112     in
 113      let pred =
 114       let gty' = CicSubstitution.lift 1 gty in
 115       let t1' = CicSubstitution.lift 1 t1 in
 116       let gty'' =
 117        ProofEngineReduction.replace_lifting
 118         ~equality:ProofEngineReduction.alpha_equivalence
 119         ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
 120       in
 121        C.Lambda
 122         (FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context C.Anonymous ~typ:ty,
 123           ty, gty'')
 124      in
 125      let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
 126      let irl =
 127       CicMkImplicit.identity_relocation_list_for_metavariable context in
 128      let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
 129
 130       let (proof',goals) =
 131        ProofEngineTypes.apply_tactic
 132         (PrimitiveTactics.exact_tac
 133          ~term:(C.Appl
 134           [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]))
 135          ((curi,metasenv',pbo,pty),goal)
 136       in
 137        assert (List.length goals = 0) ;
 138        (proof',[fresh_meta])
 139  in
 140   ProofEngineTypes.mk_tactic (rewrite_back_tac equality)
 141 ;;
 142
 143
 144 let rewrite_back_simpl_tac ~term =
 145  let rewrite_back_simpl_tac ~term status =
 146   ProofEngineTypes.apply_tactic
 147    (Tacticals.then_
 148     ~start:(rewrite_back_tac ~term)
 149     ~continuation:
 150      (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
 151    status
 152  in
 153   ProofEngineTypes.mk_tactic (rewrite_back_simpl_tac ~term)
 154 ;;
 155
 156 let replace_tac ~what ~with_what =
 157  let replace_tac ~what ~with_what status =
 158   let (proof, goal) = status in
 159   let module C = Cic in
 160   let module U = UriManager in
 161   let module P = PrimitiveTactics in
 162   let module T = Tacticals in
 163   let _,metasenv,_,_ = proof in
 164   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 165   let wty,u = (* TASSI: FIXME *)
 166     CicTypeChecker.type_of_aux' metasenv context what CicUniv.empty_ugraph in
 167   let wwty,_ = CicTypeChecker.type_of_aux' metasenv context with_what u in
 168     try
 169       if (wty = wwty) then
 170         ProofEngineTypes.apply_tactic
 171           (T.thens
 172              ~start:(
 173                P.cut_tac
 174                        (C.Appl [
 175                           (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ;
 176                           wty ;
 177                           what ;
 178                           with_what]))
 179              ~continuations:[
 180
 181                T.then_     ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
 182                            ~continuation:(
 183                                  ProofEngineStructuralRules.clear
 184                                                 ~hyp:(List.hd context)) ;
 185                T.id_tac])
 186           status
 187       else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
 188     with (Failure "hd") ->
 189       raise (ProofEngineTypes.Fail "Replace: empty context")
 190  in
 191    ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
 192 ;;
 193
 194
 195 (* All these tacs do is applying the right constructor/theorem *)
 196
 197 let reflexivity_tac =
 198   IntroductionTactics.constructor_tac ~n:1
 199 ;;
 200
 201 let symmetry_tac =
 202  let symmetry_tac (proof, goal) =
 203   let module C = Cic in
 204   let module R = CicReduction in
 205   let module U = UriManager in
 206    let (_,metasenv,_,_) = proof in
 207     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 208      match (R.whd context ty) with
 209         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
 210          when (U.eq uri HelmLibraryObjects.Logic.eq_URI) ->
 211           ProofEngineTypes.apply_tactic
 212            (PrimitiveTactics.apply_tac
 213             ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, [])))
 214            (proof,goal)
 215
 216       | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
 217  in
 218   ProofEngineTypes.mk_tactic symmetry_tac
 219 ;;
 220
 221 let transitivity_tac ~term =
 222  let transitivity_tac ~term status =
 223   let (proof, goal) = status in
 224   let module C = Cic in
 225   let module R = CicReduction in
 226   let module U = UriManager in
 227   let module T = Tacticals in
 228    let (_,metasenv,_,_) = proof in
 229     let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 230      match (R.whd context ty) with
 231         (C.Appl [(C.MutInd (uri, 0, [])); _; _; _])
 232         when (uri = HelmLibraryObjects.Logic.eq_URI) ->
 233          ProofEngineTypes.apply_tactic
 234          (T.thens
 235           ~start:(PrimitiveTactics.apply_tac
 236             ~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, [])))
 237           ~continuations:
 238             [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac])
 239           status
 240
 241       | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
 242  in
 243   ProofEngineTypes.mk_tactic (transitivity_tac ~term)
 244 ;;
 245
 246