X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FequalityTactics.ml;fp=helm%2Focaml%2Ftactics%2FequalityTactics.ml;h=0000000000000000000000000000000000000000;hp=0e9f72b0f96b73d65ea5644a85dbdceda93913d6;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
deleted file mode 100644
index 0e9f72b0f..000000000
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ /dev/null
@@ -1,213 +0,0 @@
-(* Copyright (C) 2002, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-
-let rewrite_tac ~term:equality (proof,goal) =
- let module C = Cic in
- let module U = UriManager in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-   let eq_ind_r,ty,t1,t2 =
-    match CicTypeChecker.type_of_aux' metasenv context equality with
-       C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
-        when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
-         let eq_ind_r =
-          C.Const
-           (HelmLibraryObjects.Logic.eq_ind_r_URI,[])
-         in
-          eq_ind_r,ty,t1,t2
-     | _ ->
-       raise
-        (ProofEngineTypes.Fail
-          "Rewrite: the argument is not a proof of an equality")
-   in
-    let pred =
-     let gty' = CicSubstitution.lift 1 gty in
-     let t1' = CicSubstitution.lift 1 t1 in
-     let gty'' =
-      ProofEngineReduction.replace_lifting
-       ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
-     in
-      C.Lambda
-       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
-         ty, gty'')
-    in
-    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
-    let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
-    let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
-
-     let (proof',goals) =
-      PrimitiveTactics.exact_tac
-       ~term:(C.Appl
-         [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
-          ((curi,metasenv',pbo,pty),goal)
-     in
-      assert (List.length goals = 0) ;
-      (proof',[fresh_meta])
-;;
-
-
-let rewrite_simpl_tac ~term status =
- Tacticals.then_ 
-  ~start:(rewrite_tac ~term)
-  ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
-  status
-;;
-
-
-let rewrite_back_tac ~term:equality (proof,goal) =
- let module C = Cic in
- let module U = UriManager in
-  let curi,metasenv,pbo,pty = proof in
-  let metano,context,gty = CicUtil.lookup_meta goal metasenv in
-   let eq_ind_r,ty,t1,t2 =
-    match CicTypeChecker.type_of_aux' metasenv context equality with
-       C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
-        when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
-         let eq_ind_r =
-          C.Const (HelmLibraryObjects.Logic.eq_ind_URI,[])
-         in
-          eq_ind_r,ty,t2,t1
-     | _ ->
-       raise
-        (ProofEngineTypes.Fail
-          "Rewrite: the argument is not a proof of an equality")
-   in
-    let pred =
-     let gty' = CicSubstitution.lift 1 gty in
-     let t1' = CicSubstitution.lift 1 t1 in
-     let gty'' =
-      ProofEngineReduction.replace_lifting
-       ~equality:ProofEngineReduction.alpha_equivalence
-       ~what:[t1'] ~with_what:[C.Rel 1] ~where:gty'
-     in
-      C.Lambda
-       (FreshNamesGenerator.mk_fresh_name metasenv context C.Anonymous ty,
-         ty, gty'')
-    in
-    let fresh_meta = ProofEngineHelpers.new_meta_of_proof proof in
-    let irl =
-     CicMkImplicit.identity_relocation_list_for_metavariable context in
-    let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
-
-     let (proof',goals) =
-      PrimitiveTactics.exact_tac
-       ~term:(C.Appl
-         [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
-        ((curi,metasenv',pbo,pty),goal)
-     in
-      assert (List.length goals = 0) ;
-      (proof',[fresh_meta])
-
-;;
-
-
-let rewrite_back_simpl_tac ~term status =
- Tacticals.then_ 
-  ~start:(rewrite_back_tac ~term)
-  ~continuation:
-   (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None)
-  status
-;;
-
-
-let replace_tac ~what ~with_what status =
-  let (proof, goal) = status in
-  let module C = Cic in
-  let module U = UriManager in
-  let module P = PrimitiveTactics in
-  let module T = Tacticals in
-   let _,metasenv,_,_ = proof in
-    let _,context,_ = CicUtil.lookup_meta goal metasenv in
-     let wty = CicTypeChecker.type_of_aux' metasenv context what in
-      try
-      if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
-       then
-         T.thens
-          ~start:(
-            P.cut_tac 
-             (C.Appl [
-               (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ;
-                 wty ; 
-                 what ; 
-                 with_what]))
-          ~continuations:[
-            T.then_
-               ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
-               ~continuation:(
-                 ProofEngineStructuralRules.clear
-                  ~hyp:(List.hd context)) ;
-            T.id_tac]
-          status
-       else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
-       with (Failure "hd") -> raise (ProofEngineTypes.Fail "Replace: empty context")
-;;
-
-
-(* All these tacs do is applying the right constructor/theorem *)
-
-let reflexivity_tac =
-  IntroductionTactics.constructor_tac ~n:1
-;;
-
-
-let symmetry_tac (proof, goal) =
-  let module C = Cic in
-  let module R = CicReduction in
-  let module U = UriManager in
-   let (_,metasenv,_,_) = proof in
-    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-     match (R.whd context ty) with
-        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri HelmLibraryObjects.Logic.eq_URI) ->
-         PrimitiveTactics.apply_tac (proof,goal)
-          ~term: (C.Const (HelmLibraryObjects.Logic.sym_eq_URI, []))
-
-      | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
-;;
-
-
-let transitivity_tac ~term status =
-  let (proof, goal) = status in
-  let module C = Cic in
-  let module R = CicReduction in
-  let module U = UriManager in
-  let module T = Tacticals in
-   let (_,metasenv,_,_) = proof in
-    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
-     match (R.whd context ty) with
-        (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = HelmLibraryObjects.Logic.eq_URI) ->
-         T.thens
-          ~start:(PrimitiveTactics.apply_tac
-            ~term: (C.Const (HelmLibraryObjects.Logic.trans_eq_URI, [])))
-          ~continuations:
-            [PrimitiveTactics.exact_tac ~term ; T.id_tac ; T.id_tac]
-          status
-
-      | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
-;;
-
-