elim_tac rewritten almost entirely. It is now based on refinement +

one invocation of the (now more powerful than before) apply_tac.

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index d26de444714f312904017658a0fe7739dd82ea7b..2d741f1d1c317a72cfcf62d9b25be6f4cf88f496 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -453,7 +453,7 @@ let elim_tac ~term =
   let module U = UriManager in
   let module R = CicReduction in
   let module C = Cic in
-   let (curi,metasenv,_,_) = proof in
+   let (curi,metasenv,proofbo,proofty) = proof in
    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
     let termty = T.type_of_aux' metasenv context term in
     let uri,exp_named_subst,typeno,args =
@@ -484,95 +484,43 @@ let elim_tac ~term =
      in
       let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in
        let ety = T.type_of_aux' metasenv context eliminator_ref in
-       let newmeta = new_meta_of_proof ~proof in
-        let (econclusion,newmetas,arguments,lastmeta) =
-          new_metasenv_for_apply newmeta proof context ety
+        let rec find_args_no =
+         function
+            C.Prod (_,_,t) -> 1 + find_args_no t
+          | C.Cast (s,_) -> find_args_no s
+          | C.LetIn (_,_,t) -> 0 + find_args_no t
+          | _ -> 0
         in
-         (* Here we assume that we have only one inductive hypothesis to *)
-         (* eliminate and that it is the last hypothesis of the theorem. *)
-         (* A better approach would be fingering the hypotheses in some  *)
-         (* way.                                                         *)
-         let meta_of_corpse =
-          let (_,canonical_context,_) =
-            CicUtil.lookup_meta (lastmeta - 1) newmetas
+         let args_no = find_args_no ety in
+         let term_to_refine =
+          let rec make_tl base_case =
+           function
+              0 -> [base_case]
+            | n -> (C.Implicit None)::(make_tl base_case (n - 1))
           in
-           let irl =
-            CicMkImplicit.identity_relocation_list_for_metavariable
-             canonical_context
-           in
-            Cic.Meta (lastmeta - 1, irl)
-         in
-         let newmetasenv = newmetas @ metasenv in
-         let subst1,newmetasenv' =
-          CicUnification.fo_unif newmetasenv context term meta_of_corpse
+           C.Appl (eliminator_ref :: make_tl term (args_no - 1))
          in
-          let ueconclusion = CicMetaSubst.apply_subst subst1 econclusion in
-           (* The conclusion of our elimination principle is *)
-           (*  (?i farg1 ... fargn)                         *)
-           (* The conclusion of our goal is ty. So, we can   *)
-           (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
-           (* a new ty equal to (P farg1 ... fargn). Now     *)
-           (* ?i can be instantiated with P and we are ready *)
-           (* to refine the term.                            *)
-           let emeta, fargs =
-            match ueconclusion with
-               C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs
-             | C.Meta (emeta,_) -> emeta,[]
-             | _ -> raise NotTheRightEliminatorShape
+          let metasenv', term_to_refine' =
+           CicMkImplicit.expand_implicits metasenv context term_to_refine in
+          let refined_term,_,metasenv'' =
+           CicRefine.type_of_aux' metasenv' context term_to_refine'
+          in
+           let new_goals =
+            ProofEngineHelpers.compare_metasenvs
+             ~oldmetasenv:metasenv ~newmetasenv:metasenv''
            in
-            let ty' = CicMetaSubst.apply_subst subst1 ty in
-            let eta_expanded_ty =
- (*CSC: newmetasenv' era metasenv ??????????? *)
-             List.fold_left (eta_expand newmetasenv' context) ty' fargs
+           let proof' = curi,metasenv'',proofbo,proofty in
+            let proof'', new_goals' =
+             apply_tactic (apply_tac ~term:refined_term) (proof',goal)
             in
-             let subst2,newmetasenv'' =
- (*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite
- da subst1!!!! Dovrei rimuoverle o sono innocue?*)
-              CicUnification.fo_unif
-               newmetasenv' context ueconclusion eta_expanded_ty
+             (* The apply_tactic can have closed some of the new_goals *)
+             let patched_new_goals =
+              let (_,metasenv''',_,_) = proof'' in
+               List.filter
+                (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
+                ) new_goals @ new_goals'
              in
-              let in_subst_domain i =
-               let eq_to_i = function (j,_) -> i=j in
-                List.exists eq_to_i subst1 ||
-                List.exists eq_to_i subst2
-              in
-               (* When unwinding the META that corresponds to the elimination *)
-               (* predicate (which is emeta), we must also perform one-step   *)
-               (* beta-reduction. apply_subst doesn't need the context. Hence *)
-               (* the underscore.                                             *)
-               let apply_subst _ t =
-                let t' = CicMetaSubst.apply_subst subst1 t in
-                 CicMetaSubst.apply_subst_reducing
-                  (Some (emeta,List.length fargs)) subst2 t'
-               in
-                 let old_uninstantiatedmetas,new_uninstantiatedmetas =
-                  classify_metas newmeta in_subst_domain apply_subst
-                   newmetasenv''
-                 in
-                  let arguments' = List.map (apply_subst context) arguments in
-                   let bo' = Cic.Appl (eliminator_ref::arguments') in
-                    let newmetasenv''' =
-                     new_uninstantiatedmetas@old_uninstantiatedmetas
-                    in
-                     let (newproof, newmetasenv'''') =
-                      (* When unwinding the META that corresponds to the *)
-                      (* elimination predicate (which is emeta), we must *)
-                      (* also perform one-step beta-reduction.           *)
-                      (* The only difference w.r.t. apply_subst is that  *)
-                      (* we also substitute metano with bo'.             *)
-                      (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *)
-                      (*CSC: no?                                              *)
-                      let apply_subst' t =
-                       let t' = CicMetaSubst.apply_subst subst1 t in
-                        CicMetaSubst.apply_subst_reducing
-                         (Some (emeta,List.length fargs))
-                         ((metano,bo')::subst2) t'
-                      in
-                       subst_meta_and_metasenv_in_proof
-                         proof metano apply_subst' newmetasenv'''
-                     in
-                      (newproof,
-                       List.map (function (i,_,_) -> i) new_uninstantiatedmetas)
+              proof'', patched_new_goals
  in
   mk_tactic (elim_tac ~term)
 ;;