components/tactics/primitiveTactics.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 (* $Id$ *)
  27
  28 open ProofEngineTypes
  29
  30 exception TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
  31 exception NotAnInductiveTypeToEliminate
  32 exception WrongUriToVariable of string
  33 exception NotAnEliminator
  34
  35 (* lambda_abstract newmeta ty *)
  36 (* returns a triple [bo],[context],[ty'] where              *)
  37 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
  38 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta])       *)
  39 (* So, lambda_abstract is the core of the implementation of *)
  40 (* the Intros tactic.                                       *)
  41 (* howmany = -1 means Intros, howmany > 0 means Intros n    *)
  42 let lambda_abstract ?(howmany=(-1)) metasenv context newmeta ty mk_fresh_name =
  43  let module C = Cic in
  44   let rec collect_context context howmany do_whd ty =
  45    match howmany with
  46    | 0 ->
  47         let irl =
  48           CicMkImplicit.identity_relocation_list_for_metavariable context
  49         in
  50          context, ty, (C.Meta (newmeta,irl))
  51    | _ ->
  52       match ty with
  53         C.Cast (te,_)   -> collect_context context howmany do_whd te
  54       | C.Prod (n,s,t)  ->
  55          let n' = mk_fresh_name metasenv context n ~typ:s in
  56           let (context',ty,bo) =
  57            collect_context ((Some (n',(C.Decl s)))::context) (howmany - 1) do_whd t
  58           in
  59            (context',ty,C.Lambda(n',s,bo))
  60       | C.LetIn (n,s,t) ->
  61          let (context',ty,bo) =
  62           collect_context ((Some (n,(C.Def (s,None))))::context) (howmany - 1) do_whd t
  63          in
  64           (context',ty,C.LetIn(n,s,bo))
  65       | _ as t ->
  66         if howmany <= 0 then
  67          let irl =
  68           CicMkImplicit.identity_relocation_list_for_metavariable context
  69          in
  70           context, t, (C.Meta (newmeta,irl))
  71         else if do_whd then
  72           let t = CicReduction.whd ~delta:true context t in
  73           collect_context context howmany false t
  74         else
  75          raise (Fail (lazy "intro(s): not enough products or let-ins"))
  76   in
  77    collect_context context howmany true ty
  78
  79 let eta_expand metasenv context t arg =
  80  let module T = CicTypeChecker in
  81  let module S = CicSubstitution in
  82  let module C = Cic in
  83   let rec aux n =
  84    function
  85       t' when t' = S.lift n arg -> C.Rel (1 + n)
  86     | C.Rel m  -> if m <= n then C.Rel m else C.Rel (m+1)
  87     | C.Var (uri,exp_named_subst) ->
  88        let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
  89         C.Var (uri,exp_named_subst')
  90     | C.Meta (i,l) ->
  91        let l' =
  92         List.map (function None -> None | Some t -> Some (aux n t)) l
  93        in
  94         C.Meta (i, l')
  95     | C.Sort _
  96     | C.Implicit _ as t -> t
  97     | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
  98     | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
  99     | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
 100     | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
 101     | C.Appl l -> C.Appl (List.map (aux n) l)
 102     | C.Const (uri,exp_named_subst) ->
 103        let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
 104         C.Const (uri,exp_named_subst')
 105     | C.MutInd (uri,i,exp_named_subst) ->
 106        let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
 107         C.MutInd (uri,i,exp_named_subst')
 108     | C.MutConstruct (uri,i,j,exp_named_subst) ->
 109        let exp_named_subst' = aux_exp_named_subst n exp_named_subst in
 110         C.MutConstruct (uri,i,j,exp_named_subst')
 111     | C.MutCase (sp,i,outt,t,pl) ->
 112        C.MutCase (sp,i,aux n outt, aux n t,
 113         List.map (aux n) pl)
 114     | C.Fix (i,fl) ->
 115        let tylen = List.length fl in
 116         let substitutedfl =
 117          List.map
 118           (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
 119            fl
 120         in
 121          C.Fix (i, substitutedfl)
 122     | C.CoFix (i,fl) ->
 123        let tylen = List.length fl in
 124         let substitutedfl =
 125          List.map
 126           (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 127            fl
 128         in
 129          C.CoFix (i, substitutedfl)
 130   and aux_exp_named_subst n =
 131    List.map (function uri,t -> uri,aux n t)
 132   in
 133    let argty,_ =
 134     T.type_of_aux' metasenv context arg CicUniv.empty_ugraph (* TASSI: FIXME *)
 135    in
 136     let fresh_name =
 137      FreshNamesGenerator.mk_fresh_name ~subst:[]
 138       metasenv context (Cic.Name "Heta") ~typ:argty
 139     in
 140      (C.Appl [C.Lambda (fresh_name,argty,aux 0 t) ; arg])
 141
 142 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
 143 let classify_metas newmeta in_subst_domain subst_in metasenv =
 144  List.fold_right
 145   (fun (i,canonical_context,ty) (old_uninst,new_uninst) ->
 146     if in_subst_domain i then
 147      old_uninst,new_uninst
 148     else
 149      let ty' = subst_in canonical_context ty in
 150       let canonical_context' =
 151        List.fold_right
 152         (fun entry canonical_context' ->
 153           let entry' =
 154            match entry with
 155               Some (n,Cic.Decl s) ->
 156                Some (n,Cic.Decl (subst_in canonical_context' s))
 157             | Some (n,Cic.Def (s,None)) ->
 158                Some (n,Cic.Def ((subst_in canonical_context' s),None))
 159             | None -> None
 160             | Some (n,Cic.Def (bo,Some ty)) ->
 161                Some
 162                 (n,
 163                   Cic.Def
 164                    (subst_in canonical_context' bo,
 165                     Some (subst_in canonical_context' ty)))
 166           in
 167            entry'::canonical_context'
 168         ) canonical_context []
 169      in
 170       if i < newmeta then
 171        ((i,canonical_context',ty')::old_uninst),new_uninst
 172       else
 173        old_uninst,((i,canonical_context',ty')::new_uninst)
 174   ) metasenv ([],[])
 175
 176 (* Useful only inside apply_tac *)
 177 let
 178  generalize_exp_named_subst_with_fresh_metas context newmeta uri exp_named_subst
 179 =
 180  let module C = Cic in
 181   let params =
 182     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 183     CicUtil.params_of_obj o
 184   in
 185    let exp_named_subst_diff,new_fresh_meta,newmetasenvfragment,exp_named_subst'=
 186     let next_fresh_meta = ref newmeta in
 187     let newmetasenvfragment = ref [] in
 188     let exp_named_subst_diff = ref [] in
 189      let rec aux =
 190       function
 191          [],[] -> []
 192        | uri::tl,[] ->
 193           let ty =
 194             let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 195               match o with
 196                   C.Variable (_,_,ty,_,_) ->
 197                     CicSubstitution.subst_vars !exp_named_subst_diff ty
 198                 | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
 199           in
 200 (* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type
 201            (match ty with
 202                C.Sort (C.Type _) as s -> (* TASSI: ?? *)
 203                  let fresh_meta = !next_fresh_meta in
 204                  let fresh_meta' = fresh_meta + 1 in
 205                   next_fresh_meta := !next_fresh_meta + 2 ;
 206                   let subst_item = uri,C.Meta (fresh_meta',[]) in
 207                    newmetasenvfragment :=
 208                     (fresh_meta,[],C.Sort (C.Type (CicUniv.fresh()))) ::
 209                      (* TASSI: ?? *)
 210                      (fresh_meta',[],C.Meta (fresh_meta,[])) :: !newmetasenvfragment ;
 211                    exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
 212                    subst_item::(aux (tl,[]))
 213              | _ ->
 214 *)
 215               let irl =
 216                 CicMkImplicit.identity_relocation_list_for_metavariable context
 217               in
 218               let subst_item = uri,C.Meta (!next_fresh_meta,irl) in
 219                newmetasenvfragment :=
 220                 (!next_fresh_meta,context,ty)::!newmetasenvfragment ;
 221                exp_named_subst_diff := !exp_named_subst_diff @ [subst_item] ;
 222                incr next_fresh_meta ;
 223                subst_item::(aux (tl,[]))(*)*)
 224        | uri::tl1,((uri',_) as s)::tl2 ->
 225           assert (UriManager.eq uri uri') ;
 226           s::(aux (tl1,tl2))
 227        | [],_ -> assert false
 228      in
 229       let exp_named_subst' = aux (params,exp_named_subst) in
 230        !exp_named_subst_diff,!next_fresh_meta,
 231         List.rev !newmetasenvfragment, exp_named_subst'
 232    in
 233     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 234 ;;
 235
 236 let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
 237   let (consthead,newmetasenv,arguments,_) =
 238    TermUtil.saturate_term newmeta' metasenv' context termty
 239     goal_arity in
 240   let subst,newmetasenv',_ =
 241    CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
 242   in
 243   let t =
 244     if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
 245   in
 246   subst,newmetasenv',t
 247
 248 let rec count_prods context ty =
 249  match CicReduction.whd context ty with
 250     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
 251   | _ -> 0
 252
 253 let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
 254   (* Assumption: The term "term" must be closed in the current context *)
 255  let module T = CicTypeChecker in
 256  let module R = CicReduction in
 257  let module C = Cic in
 258   let (_,metasenv,_,_, _) = proof in
 259   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 260   let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
 261    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
 262     match term with
 263        C.Var (uri,exp_named_subst) ->
 264         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 265          generalize_exp_named_subst_with_fresh_metas context newmeta uri
 266           exp_named_subst
 267         in
 268          exp_named_subst_diff,newmeta',newmetasenvfragment,
 269           C.Var (uri,exp_named_subst')
 270      | C.Const (uri,exp_named_subst) ->
 271         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 272          generalize_exp_named_subst_with_fresh_metas context newmeta uri
 273           exp_named_subst
 274         in
 275          exp_named_subst_diff,newmeta',newmetasenvfragment,
 276           C.Const (uri,exp_named_subst')
 277      | C.MutInd (uri,tyno,exp_named_subst) ->
 278         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 279          generalize_exp_named_subst_with_fresh_metas context newmeta uri
 280           exp_named_subst
 281         in
 282          exp_named_subst_diff,newmeta',newmetasenvfragment,
 283           C.MutInd (uri,tyno,exp_named_subst')
 284      | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 285         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 286          generalize_exp_named_subst_with_fresh_metas context newmeta uri
 287           exp_named_subst
 288         in
 289          exp_named_subst_diff,newmeta',newmetasenvfragment,
 290           C.MutConstruct (uri,tyno,consno,exp_named_subst')
 291      | _ -> [],newmeta,[],term
 292    in
 293    let metasenv' = metasenv@newmetasenvfragment in
 294    let termty,_ =
 295      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
 296    in
 297    let termty =
 298      CicSubstitution.subst_vars exp_named_subst_diff termty in
 299    let goal_arity = count_prods context ty in
 300    let subst,newmetasenv',t =
 301     let rec add_one_argument n =
 302      try
 303       new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
 304         termty n
 305      with CicUnification.UnificationFailure _ when n > 0 ->
 306       add_one_argument (n - 1)
 307     in
 308      add_one_argument goal_arity
 309    in
 310    let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
 311    let apply_subst = CicMetaSubst.apply_subst subst in
 312    let old_uninstantiatedmetas,new_uninstantiatedmetas =
 313      (* subst_in doesn't need the context. Hence the underscore. *)
 314      let subst_in _ = CicMetaSubst.apply_subst subst in
 315      classify_metas newmeta in_subst_domain subst_in newmetasenv'
 316    in
 317    let bo' = apply_subst t in
 318    let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
 319    let subst_in =
 320      (* if we just apply the subtitution, the type is irrelevant:
 321               we may use Implicit, since it will be dropped *)
 322      CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
 323    in
 324    let (newproof, newmetasenv''') =
 325     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
 326      newmetasenv''
 327    in
 328    let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
 329    subst,
 330    (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
 331    max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
 332
 333
 334 (* ALB *)
 335 let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
 336   try
 337 (*     apply_tac_verbose ~term status *)
 338     apply_with_subst ~term ~subst ~maxmeta status
 339       (* TODO cacciare anche altre eccezioni? *)
 340   with
 341   | CicUnification.UnificationFailure msg
 342   | CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg)
 343
 344 (* ALB *)
 345 let apply_tac_verbose ~term status =
 346   let subst, status, _ = apply_with_subst ~term status in
 347   (CicMetaSubst.apply_subst subst), status
 348
 349 let apply_tac ~term status = snd (apply_tac_verbose ~term status)
 350
 351   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
 352   sollevino _solamente_ Fail *)
 353 let apply_tac ~term =
 354  let apply_tac ~term status =
 355   try
 356     apply_tac ~term status
 357       (* TODO cacciare anche altre eccezioni? *)
 358   with
 359   | CicUnification.UnificationFailure msg
 360   | CicTypeChecker.TypeCheckerFailure msg ->
 361       raise (Fail msg)
 362  in
 363   mk_tactic (apply_tac ~term)
 364
 365 let intros_tac ?howmany ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) ()=
 366  let intros_tac
 367   ?(mk_fresh_name_callback = (FreshNamesGenerator.mk_fresh_name ~subst:[])) ()
 368   (proof, goal)
 369  =
 370   let module C = Cic in
 371   let module R = CicReduction in
 372    let (_,metasenv,_,_, _) = proof in
 373    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 374     let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 375      let (context',ty',bo') =
 376       lambda_abstract ?howmany metasenv context newmeta ty mk_fresh_name_callback
 377      in
 378       let (newproof, _) =
 379        ProofEngineHelpers.subst_meta_in_proof proof metano bo'
 380         [newmeta,context',ty']
 381       in
 382        (newproof, [newmeta])
 383  in
 384   mk_tactic (intros_tac ~mk_fresh_name_callback ())
 385
 386 let cut_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
 387  let cut_tac
 388   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
 389   term (proof, goal)
 390  =
 391   let module C = Cic in
 392    let curi,metasenv,pbo,pty, attrs = proof in
 393    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 394     let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
 395     let newmeta2 = newmeta1 + 1 in
 396     let fresh_name =
 397      mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
 398     let context_for_newmeta1 =
 399      (Some (fresh_name,C.Decl term))::context in
 400     let irl1 =
 401      CicMkImplicit.identity_relocation_list_for_metavariable
 402       context_for_newmeta1
 403     in
 404     let irl2 =
 405       CicMkImplicit.identity_relocation_list_for_metavariable context
 406     in
 407      let newmeta1ty = CicSubstitution.lift 1 ty in
 408      let bo' =
 409       C.Appl
 410        [C.Lambda (fresh_name,term,C.Meta (newmeta1,irl1)) ;
 411         C.Meta (newmeta2,irl2)]
 412      in
 413       let (newproof, _) =
 414        ProofEngineHelpers.subst_meta_in_proof proof metano bo'
 415         [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
 416       in
 417        (newproof, [newmeta1 ; newmeta2])
 418  in
 419   mk_tactic (cut_tac ~mk_fresh_name_callback term)
 420
 421 let letin_tac ?(mk_fresh_name_callback=FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
 422  let letin_tac
 423   ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
 424   term (proof, goal)
 425  =
 426   let module C = Cic in
 427    let curi,metasenv,pbo,pty, attrs = proof in
 428    (* occur check *)
 429    let occur i t =
 430      let m = CicUtil.metas_of_term t in
 431      List.exists (fun (j,_) -> i=j) m
 432    in
 433    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 434    if occur metano term then
 435      raise
 436        (ProofEngineTypes.Fail (lazy
 437          "You can't letin a term containing the current goal"));
 438     let _,_ =
 439       CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
 440      let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 441      let fresh_name =
 442       mk_fresh_name_callback metasenv context (Cic.Name "Hletin") ~typ:term in
 443      let context_for_newmeta =
 444       (Some (fresh_name,C.Def (term,None)))::context in
 445      let irl =
 446       CicMkImplicit.identity_relocation_list_for_metavariable
 447        context_for_newmeta
 448      in
 449       let newmetaty = CicSubstitution.lift 1 ty in
 450       let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
 451        let (newproof, _) =
 452          ProofEngineHelpers.subst_meta_in_proof
 453            proof metano bo'[newmeta,context_for_newmeta,newmetaty]
 454        in
 455         (newproof, [newmeta])
 456  in
 457   mk_tactic (letin_tac ~mk_fresh_name_callback term)
 458
 459   (** functional part of the "exact" tactic *)
 460 let exact_tac ~term =
 461  let exact_tac ~term (proof, goal) =
 462   (* Assumption: the term bo must be closed in the current context *)
 463   let (_,metasenv,_,_, _) = proof in
 464   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 465   let module T = CicTypeChecker in
 466   let module R = CicReduction in
 467   let ty_term,u = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
 468   let b,_ = R.are_convertible context ty_term ty u in (* TASSI: FIXME *)
 469   if b then
 470    begin
 471     let (newproof, metasenv') =
 472       ProofEngineHelpers.subst_meta_in_proof proof metano term [] in
 473     (newproof, [])
 474    end
 475   else
 476    raise (Fail (lazy "The type of the provided term is not the one expected."))
 477  in
 478   mk_tactic (exact_tac ~term)
 479
 480 (* not really "primitive" tactics .... *)
 481
 482 module TC  = CicTypeChecker
 483 module U   = UriManager
 484 module R   = CicReduction
 485 module C   = Cic
 486 module PET = ProofEngineTypes
 487 module PEH = ProofEngineHelpers
 488 module PER = ProofEngineReduction
 489 module MS  = CicMetaSubst
 490 module S   = CicSubstitution
 491 module T   = Tacticals
 492 module RT  = ReductionTactics
 493
 494 let elim_tac ?using ?(pattern = PET.conclusion_pattern None) term =
 495  let elim_tac (proof, goal) =
 496    let ugraph = CicUniv.empty_ugraph in
 497    let curi, metasenv, proofbo, proofty, attrs = proof in
 498    let conjecture = CicUtil.lookup_meta goal metasenv in
 499    let metano, context, ty = conjecture in
 500 (*    let (term, metasenv, _ugraph), cpatt = match pattern with
 501        | Some f, [], Some cpatt -> f context metasenv ugraph, cpatt
 502        | _                      -> assert false
 503     in
 504 *)
 505     let termty,_ugraph = TC.type_of_aux' metasenv context term ugraph in
 506     let termty = CicReduction.whd context termty in
 507     let (termty,metasenv',arguments,_fresh_meta) =
 508      TermUtil.saturate_term
 509       (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
 510     let term = if arguments = [] then term else Cic.Appl (term::arguments) in
 511     let uri,exp_named_subst,typeno,args =
 512      match termty with
 513         C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
 514       | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
 515           (uri,exp_named_subst,typeno,args)
 516       | _ -> raise NotAnInductiveTypeToEliminate
 517     in
 518      let eliminator_uri =
 519       let buri = U.buri_of_uri uri in
 520       let name =
 521         let o,_ugraph = CicEnvironment.get_obj ugraph uri in
 522        match o with
 523           C.InductiveDefinition (tys,_,_,_) ->
 524            let (name,_,_,_) = List.nth tys typeno in
 525             name
 526         | _ -> assert false
 527       in
 528       let ty_ty,_ugraph = TC.type_of_aux' metasenv' context ty ugraph in
 529       let ext =
 530        match ty_ty with
 531           C.Sort C.Prop -> "_ind"
 532         | C.Sort C.Set  -> "_rec"
 533         | C.Sort C.CProp -> "_rec"
 534         | C.Sort (C.Type _)-> "_rect"
 535         | C.Meta (_,_) -> raise TheTypeOfTheCurrentGoalIsAMetaICannotChooseTheRightElimiantionPrinciple
 536         | _ -> assert false
 537       in
 538        U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
 539      in
 540       let eliminator_ref = match using with
 541          | None   -> C.Const (eliminator_uri,exp_named_subst)
 542          | Some t -> t
 543        in
 544        let ety,_ugraph =
 545          TC.type_of_aux' metasenv' context eliminator_ref ugraph in
 546 (* FG: ADDED PART ***********************************************************)
 547 (* FG: we can not assume eliminator is the default eliminator ***************)
 548    let add_lambdas n t =
 549       let rec aux n t =
 550          if n <= 0 then t
 551          else C.Lambda (C.Anonymous, C.Implicit None, aux (pred n) t)
 552       in
 553       aux n (S.lift n t)
 554    in
 555    let rec args_init n f =
 556       if n <= 0 then [] else f n :: args_init (pred n) f
 557    in
 558    let splits, args_no = PEH.split_with_whd (context, ety) in
 559    let pred_pos = match List.hd splits with
 560       | _, C.Rel i when i > 1 && i <= args_no -> i
 561       | _, C.Appl (C.Rel i :: _) when i > 1 && i <= args_no -> i
 562       | _ -> raise NotAnEliminator
 563    in
 564    let _, lambdas = PEH.split_with_whd (List.nth splits pred_pos) in
 565    let termty_ty =
 566       let termty_ty,_ugraph = TC.type_of_aux' metasenv' context termty ugraph in
 567       CicReduction.whd context termty_ty
 568    in
 569 (*
 570    let metasenv', term, pred, upto = match cpatt, termty_ty with
 571       | C.Implicit (Some `Hole), _
 572       | _, C.Sort C.Prop when lambdas = 0 -> metasenv', term, C.Implicit None, 0
 573       | _                                 ->
 574 (* FG: we find the predicate for the eliminator as in the rewrite tactic ****)
 575          let fresh_name =
 576              FreshNamesGenerator.mk_fresh_name
 577              ~subst:[] metasenv' context C.Anonymous ~typ:termty
 578          in
 579          let lazy_term c m u =
 580             let distance  = List.length c - List.length context in
 581             S.lift distance term, m, u
 582          in
 583          let pattern = Some lazy_term, [], Some cpatt in
 584          let subst, metasenv', _ugraph, _conjecture, selected_terms =
 585             ProofEngineHelpers.select
 586             ~metasenv:metasenv' ~ugraph ~conjecture ~pattern
 587          in
 588          let metasenv' = MS.apply_subst_metasenv subst metasenv' in
 589          let map (_context_of_t, t) l = t :: l in
 590          let what = List.fold_right map selected_terms [] in
 591          let ty = MS.apply_subst subst ty in
 592          let term = MS.apply_subst subst term in
 593          let termty = MS.apply_subst subst termty in
 594          let abstr_ty = PER.replace_with_rel_1_from ~equality:(==) ~what 1 ty in
 595          let abstr_ty = MS.apply_subst subst abstr_ty in
 596          let pred_body = C.Lambda (fresh_name, termty, abstr_ty) in
 597          metasenv', term, add_lambdas (pred lambdas) pred_body, lambdas
 598    in
 599 (* FG: END OF ADDED PART ****************************************************)
 600 *)
 601          let pred, upto = C.Implicit None, 0 in
 602
 603          let term_to_refine =
 604           let f n =
 605            if n = pred_pos then pred else
 606            if n = 1 then term else C.Implicit None
 607           in
 608            C.Appl (eliminator_ref :: args_init args_no f)
 609          in
 610           let refined_term,_refined_termty,metasenv'',_ugraph =
 611            CicRefine.type_of_aux' metasenv' context term_to_refine
 612              ugraph
 613           in
 614            let new_goals =
 615             ProofEngineHelpers.compare_metasenvs
 616              ~oldmetasenv:metasenv ~newmetasenv:metasenv''
 617            in
 618            let proof' = curi,metasenv'',proofbo,proofty, attrs in
 619             let proof'', new_goals' =
 620              apply_tactic (apply_tac ~term:refined_term) (proof',goal)
 621             in
 622              (* The apply_tactic can have closed some of the new_goals *)
 623              let patched_new_goals =
 624               let (_,metasenv''',_,_, _) = proof'' in
 625                List.filter
 626                 (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
 627                 ) new_goals @ new_goals'
 628              in
 629               let res = proof'', patched_new_goals in
 630                if upto = 0 then res else
 631                 let pattern = PET.conclusion_pattern None in
 632                 let continuation =
 633                  RT.simpl_tac ~pattern
 634                  (* RT.head_beta_reduce_tac ~delta:false ~upto ~pattern *)
 635                 in
 636                  let dummy_status = proof,goal in
 637                   PET.apply_tactic
 638                    (T.then_ ~start:(PET.mk_tactic (fun _ -> res)) ~continuation)
 639                    dummy_status
 640  in
 641   mk_tactic elim_tac
 642 ;;
 643
 644 let cases_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) term =
 645  let cases_tac ~term (proof, goal) =
 646   let module TC = CicTypeChecker in
 647   let module U = UriManager in
 648   let module R = CicReduction in
 649   let module C = Cic in
 650    let (curi,metasenv,proofbo,proofty, attrs) = proof in
 651    let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 652     let termty,_ = TC.type_of_aux' metasenv context term CicUniv.empty_ugraph in
 653     let termty = CicReduction.whd context termty in
 654     let (termty,metasenv',arguments,fresh_meta) =
 655      TermUtil.saturate_term
 656       (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in
 657     let term = if arguments = [] then term else Cic.Appl (term::arguments) in
 658     let uri,exp_named_subst,typeno,args =
 659      match termty with
 660         C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
 661       | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
 662           (uri,exp_named_subst,typeno,args)
 663       | _ -> raise NotAnInductiveTypeToEliminate
 664     in
 665      let paramsno,itty,patterns =
 666       match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
 667          C.InductiveDefinition (tys,_,paramsno,_),_ ->
 668           let _,_,itty,cl = List.nth tys typeno in
 669           let rec aux n context t =
 670            match n,CicReduction.whd context t with
 671               0,C.Prod (name,source,target) ->
 672                let fresh_name =
 673                 mk_fresh_name_callback metasenv' context name
 674                  (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
 675                  ~typ:source
 676                in
 677                 C.Lambda (fresh_name,C.Implicit None,
 678                  aux 0 (Some (fresh_name,C.Decl source)::context) target)
 679             | n,C.Prod (name,source,target) ->
 680                let fresh_name =
 681                 mk_fresh_name_callback metasenv' context name
 682                  (*CSC: WRONG TYPE HERE: I can get a "bad" name*)
 683                  ~typ:source
 684                in
 685                 aux (n-1) (Some (fresh_name,C.Decl source)::context) target
 686             | 0,_ -> C.Implicit None
 687             | _,_ -> assert false
 688           in
 689            paramsno,itty,
 690            List.map (function (_,cty) -> aux paramsno context cty) cl
 691        | _ -> assert false
 692      in
 693       let outtype =
 694        let target =
 695         C.Lambda (C.Name "fixme",C.Implicit None,
 696          ProofEngineReduction.replace_lifting
 697           ~equality:(ProofEngineReduction.alpha_equivalence)
 698           ~what:[CicSubstitution.lift (paramsno+1) term]
 699           ~with_what:[C.Rel (paramsno+1)]
 700           ~where:(CicSubstitution.lift (paramsno+1) ty))
 701        in
 702         let rec add_lambdas =
 703          function
 704             0 -> target
 705           | n -> C.Lambda (C.Name "fixme",C.Implicit None,add_lambdas (n-1))
 706         in
 707          add_lambdas (count_prods context itty - paramsno)
 708       in
 709        let term_to_refine =
 710         C.MutCase (uri,typeno,outtype,term,patterns)
 711        in
 712         let refined_term,_,metasenv'',_ =
 713          CicRefine.type_of_aux' metasenv' context term_to_refine
 714            CicUniv.empty_ugraph
 715         in
 716          let new_goals =
 717           ProofEngineHelpers.compare_metasenvs
 718            ~oldmetasenv:metasenv ~newmetasenv:metasenv''
 719          in
 720          let proof' = curi,metasenv'',proofbo,proofty, attrs in
 721           let proof'', new_goals' =
 722            apply_tactic (apply_tac ~term:refined_term) (proof',goal)
 723           in
 724            (* The apply_tactic can have closed some of the new_goals *)
 725            let patched_new_goals =
 726             let (_,metasenv''',_,_,_) = proof'' in
 727              List.filter
 728               (function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
 729               ) new_goals @ new_goals'
 730            in
 731             proof'', patched_new_goals
 732  in
 733   mk_tactic (cases_tac ~term)
 734 ;;
 735
 736
 737 let elim_intros_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
 738                     ?depth ?using ?pattern what =
 739  Tacticals.then_ ~start:(elim_tac ?using ?pattern what)
 740   ~continuation:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
 741 ;;
 742
 743 (* The simplification is performed only on the conclusion *)
 744 let elim_intros_simpl_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[])
 745                           ?depth ?using ?pattern what =
 746  Tacticals.then_ ~start:(elim_tac ?using ?pattern what)
 747   ~continuation:
 748    (Tacticals.thens
 749      ~start:(intros_tac ~mk_fresh_name_callback ?howmany:depth ())
 750      ~continuations:
 751        [ReductionTactics.simpl_tac
 752          ~pattern:(ProofEngineTypes.conclusion_pattern None)])
 753 ;;
 754
 755 (* FG: insetrts a "hole" in the context (derived from letin_tac) *)
 756
 757 let letout_tac =
 758    let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
 759    let term = C.Sort C.Set in
 760    let letout_tac (proof, goal) =
 761       let curi, metasenv, pbo, pty, attrs = proof in
 762       let metano, context, ty = CicUtil.lookup_meta goal metasenv in
 763       let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
 764       let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
 765       let context_for_newmeta = None :: context in
 766       let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
 767       let newmetaty = CicSubstitution.lift 1 ty in
 768       let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
 769       let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
 770       newproof, [newmeta]
 771    in
 772    mk_tactic letout_tac