helm/gTopLevel/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 open ProofEngineHelpers
  27 open ProofEngineTypes
  28
  29 exception NotAnInductiveTypeToEliminate
  30 exception NotTheRightEliminatorShape
  31 exception NoHypothesesFound
  32
  33 (* TODO problemone del fresh_name, aggiungerlo allo status? *)
  34 let fresh_name () = "FOO"
  35
  36 (* lambda_abstract newmeta ty *)
  37 (* returns a triple [bo],[context],[ty'] where              *)
  38 (* [ty] = Pi/LetIn [context].[ty'] ([context] is a vector!) *)
  39 (* and [bo] = Lambda/LetIn [context].(Meta [newmeta])       *)
  40 (* So, lambda_abstract is the core of the implementation of *)
  41 (* the Intros tactic.                                       *)
  42 let lambda_abstract context newmeta ty name =
  43  let module C = Cic in
  44   let rec collect_context context =
  45    function
  46       C.Cast (te,_)   -> collect_context context te
  47     | C.Prod (n,s,t)  ->
  48        let n' =
  49         match n with
  50            C.Name _ -> n
  51 (*CSC: generatore di nomi? Chiedere il nome? *)
  52          | C.Anonimous -> C.Name name
  53        in
  54         let (context',ty,bo) =
  55          collect_context ((Some (n',(C.Decl s)))::context) t
  56         in
  57          (context',ty,C.Lambda(n',s,bo))
  58     | C.LetIn (n,s,t) ->
  59        let (context',ty,bo) =
  60         collect_context ((Some (n,(C.Def s)))::context) t
  61        in
  62         (context',ty,C.LetIn(n,s,bo))
  63     | _ as t ->
  64       let irl = identity_relocation_list_for_metavariable context in
  65        context, t, (C.Meta (newmeta,irl))
  66   in
  67    collect_context context ty
  68
  69 let eta_expand metasenv context t arg =
  70  let module T = CicTypeChecker in
  71  let module S = CicSubstitution in
  72  let module C = Cic in
  73   let rec aux n =
  74    function
  75       t' when t' = S.lift n arg -> C.Rel (1 + n)
  76     | C.Rel m  -> if m <= n then C.Rel m else C.Rel (m+1)
  77     | C.Var _
  78     | C.Meta _
  79     | C.Sort _
  80     | C.Implicit as t -> t
  81     | C.Cast (te,ty) -> C.Cast (aux n te, aux n ty)
  82     | C.Prod (nn,s,t) -> C.Prod (nn, aux n s, aux (n+1) t)
  83     | C.Lambda (nn,s,t) -> C.Lambda (nn, aux n s, aux (n+1) t)
  84     | C.LetIn (nn,s,t) -> C.LetIn (nn, aux n s, aux (n+1) t)
  85     | C.Appl l -> C.Appl (List.map (aux n) l)
  86     | C.Const _ as t -> t
  87     | C.MutInd _
  88     | C.MutConstruct _ as t -> t
  89     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
  90        C.MutCase (sp,cookingsno,i,aux n outt, aux n t,
  91         List.map (aux n) pl)
  92     | C.Fix (i,fl) ->
  93        let tylen = List.length fl in
  94         let substitutedfl =
  95          List.map
  96           (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
  97            fl
  98         in
  99          C.Fix (i, substitutedfl)
 100     | C.CoFix (i,fl) ->
 101        let tylen = List.length fl in
 102         let substitutedfl =
 103          List.map
 104           (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
 105            fl
 106         in
 107          C.CoFix (i, substitutedfl)
 108   in
 109    let argty =
 110     T.type_of_aux' metasenv context arg
 111    in
 112     (C.Appl [C.Lambda ((C.Name "dummy"),argty,aux 0 t) ; arg])
 113
 114 (*CSC: The call to the Intros tactic is embedded inside the code of the *)
 115 (*CSC: Elim tactic. Do we already need tacticals?                       *)
 116 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
 117 (* head, a META environment in which there is new a META for each hypothesis,*)
 118 (* a list of arguments for the new applications and the indexes of the first *)
 119 (* and last new METAs introduced. The nth argument in the list of arguments  *)
 120 (* is the nth new META lambda-abstracted as much as possible. Hence, this    *)
 121 (* functions already provides the behaviour of Intros on the new goals.      *)
 122 let new_metasenv_for_apply_intros proof context ty =
 123  let module C = Cic in
 124  let module S = CicSubstitution in
 125   let rec aux newmeta =
 126    function
 127       C.Cast (he,_) -> aux newmeta he
 128     | C.Prod (name,s,t) ->
 129        let newcontext,ty',newargument =
 130          lambda_abstract context newmeta s (fresh_name ())
 131        in
 132         let (res,newmetasenv,arguments,lastmeta) =
 133          aux (newmeta + 1) (S.subst newargument t)
 134         in
 135          res,(newmeta,newcontext,ty')::newmetasenv,newargument::arguments,lastmeta
 136     | t -> t,[],[],newmeta
 137   in
 138    let newmeta = new_meta ~proof in
 139     (* WARNING: here we are using the invariant that above the most *)
 140     (* recente new_meta() there are no used metas.                  *)
 141     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
 142      res,newmetasenv,arguments,newmeta,lastmeta
 143
 144 (*CSC: ma serve solamente la prima delle new_uninst e l'unione delle due!!! *)
 145 let classify_metas newmeta in_subst_domain subst_in metasenv =
 146  List.fold_right
 147   (fun (i,canonical_context,ty) (old_uninst,new_uninst) ->
 148     if in_subst_domain i then
 149      old_uninst,new_uninst
 150     else
 151      let ty' = subst_in canonical_context ty in
 152       let canonical_context' =
 153        List.fold_right
 154         (fun entry canonical_context' ->
 155           let entry' =
 156            match entry with
 157               Some (n,Cic.Decl s) ->
 158                Some (n,Cic.Decl (subst_in canonical_context' s))
 159             | Some (n,Cic.Def s) ->
 160                Some (n,Cic.Def (subst_in canonical_context' s))
 161             | None -> None
 162           in
 163            entry'::canonical_context'
 164         ) canonical_context []
 165      in
 166       if i < newmeta then
 167        ((i,canonical_context',ty')::old_uninst),new_uninst
 168       else
 169        old_uninst,((i,canonical_context',ty')::new_uninst)
 170   ) metasenv ([],[])
 171
 172 (* Auxiliary function for apply: given a type (a backbone), it returns its   *)
 173 (* head, a META environment in which there is new a META for each hypothesis,*)
 174 (* a list of arguments for the new applications and the indexes of the first *)
 175 (* and last new METAs introduced. The nth argument in the list of arguments  *)
 176 (* is just the nth new META.                                                 *)
 177 let new_metasenv_for_apply proof context ty =
 178  let module C = Cic in
 179  let module S = CicSubstitution in
 180   let rec aux newmeta =
 181    function
 182       C.Cast (he,_) -> aux newmeta he
 183     | C.Prod (name,s,t) ->
 184        let irl = identity_relocation_list_for_metavariable context in
 185         let newargument = C.Meta (newmeta,irl) in
 186          let (res,newmetasenv,arguments,lastmeta) =
 187           aux (newmeta + 1) (S.subst newargument t)
 188          in
 189           res,(newmeta,context,s)::newmetasenv,newargument::arguments,lastmeta
 190     | t -> t,[],[],newmeta
 191   in
 192    let newmeta = new_meta ~proof in
 193     (* WARNING: here we are using the invariant that above the most *)
 194     (* recente new_meta() there are no used metas.                  *)
 195     let (res,newmetasenv,arguments,lastmeta) = aux newmeta ty in
 196      res,newmetasenv,arguments,newmeta,lastmeta
 197
 198 let apply_tac ~status:(proof, goal) ~term =
 199   (* Assumption: The term "term" must be closed in the current context *)
 200  let module T = CicTypeChecker in
 201  let module R = CicReduction in
 202  let module C = Cic in
 203   let metasenv =
 204    match proof with
 205       None -> assert false
 206     | Some (_,metasenv,_,_) -> metasenv
 207   in
 208   let metano,context,ty =
 209    match goal with
 210       None -> assert false
 211     | Some metano ->
 212        List.find (function (m,_,_) -> m=metano) metasenv
 213   in
 214    let termty = CicTypeChecker.type_of_aux' metasenv context term in
 215     (* newmeta is the lowest index of the new metas introduced *)
 216     let (consthead,newmetas,arguments,newmeta,_) =
 217      new_metasenv_for_apply proof context termty
 218     in
 219      let newmetasenv = newmetas@metasenv in
 220       let subst,newmetasenv' =
 221        CicUnification.fo_unif newmetasenv context consthead ty
 222       in
 223        let in_subst_domain i = List.exists (function (j,_) -> i=j) subst in
 224        let apply_subst = CicUnification.apply_subst subst in
 225         let old_uninstantiatedmetas,new_uninstantiatedmetas =
 226          (* subst_in doesn't need the context. Hence the underscore. *)
 227          let subst_in _ = CicUnification.apply_subst subst in
 228           classify_metas newmeta in_subst_domain subst_in newmetasenv'
 229         in
 230          let bo' =
 231           if List.length newmetas = 0 then
 232            term
 233           else
 234            let arguments' = List.map apply_subst arguments in
 235             Cic.Appl (term::arguments')
 236          in
 237           let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
 238           let (newproof, newmetasenv''') =
 239            let subst_in = CicUnification.apply_subst ((metano,bo')::subst) in
 240             subst_meta_and_metasenv_in_proof
 241               proof metano subst_in newmetasenv''
 242           in
 243            (newproof,
 244             (match newmetasenv''' with
 245             | [] -> None
 246             | (i,_,_)::_ -> Some i))
 247
 248   (* TODO per implementare i tatticali e' necessario che tutte le tattiche
 249   sollevino _solamente_ Fail *)
 250 let apply_tac ~status ~term =
 251   try
 252     apply_tac ~status ~term
 253       (* TODO cacciare anche altre eccezioni? *)
 254   with CicUnification.UnificationFailed as e ->
 255     raise (Fail (Printexc.to_string e))
 256
 257 let intros_tac ~status:(proof, goal) ~name =
 258  let module C = Cic in
 259  let module R = CicReduction in
 260   let metasenv =
 261    match proof with
 262       None -> assert false
 263     | Some (_,metasenv,_,_) -> metasenv
 264   in
 265   let metano,context,ty =
 266    match goal with
 267       None -> assert false
 268     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 269   in
 270    let newmeta = new_meta ~proof in
 271     let (context',ty',bo') = lambda_abstract context newmeta ty name in
 272      let (newproof, _) =
 273        subst_meta_in_proof proof metano bo' [newmeta,context',ty']
 274      in
 275       let newgoal = Some newmeta in
 276        (newproof, newgoal)
 277
 278 let cut_tac ~status:(proof, goal) ~term =
 279  let module C = Cic in
 280   let curi,metasenv,pbo,pty =
 281    match proof with
 282       None -> assert false
 283     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 284   in
 285   let metano,context,ty =
 286    match goal with
 287       None -> assert false
 288     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 289   in
 290    let newmeta1 = new_meta ~proof in
 291    let newmeta2 = newmeta1 + 1 in
 292    let context_for_newmeta1 =
 293     (Some (C.Name "dummy_for_cut",C.Decl term))::context in
 294    let irl1 =
 295     identity_relocation_list_for_metavariable context_for_newmeta1 in
 296    let irl2 = identity_relocation_list_for_metavariable context in
 297     let newmeta1ty = CicSubstitution.lift 1 ty in
 298     let bo' =
 299      C.Appl
 300       [C.Lambda (C.Name "dummy_for_cut",term,C.Meta (newmeta1,irl1)) ;
 301        C.Meta (newmeta2,irl2)]
 302     in
 303      let (newproof, _) =
 304       subst_meta_in_proof proof metano bo'
 305        [newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
 306      in
 307       let newgoal = Some newmeta1 in
 308        (newproof, newgoal)
 309
 310 let letin_tac ~status:(proof, goal) ~term =
 311  let module C = Cic in
 312   let curi,metasenv,pbo,pty =
 313    match proof with
 314       None -> assert false
 315     | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
 316   in
 317   let metano,context,ty =
 318    match goal with
 319       None -> assert false
 320     | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 321   in
 322    let _ = CicTypeChecker.type_of_aux' metasenv context term in
 323     let newmeta = new_meta ~proof in
 324     let context_for_newmeta =
 325      (Some (C.Name "dummy_for_letin",C.Def term))::context in
 326     let irl =
 327      identity_relocation_list_for_metavariable context_for_newmeta in
 328      let newmetaty = CicSubstitution.lift 1 ty in
 329      let bo' = C.LetIn (C.Name "dummy_for_letin",term,C.Meta (newmeta,irl)) in
 330       let (newproof, _) =
 331         subst_meta_in_proof
 332           proof metano bo'[newmeta,context_for_newmeta,newmetaty]
 333       in
 334        let newgoal = Some newmeta in
 335         (newproof, newgoal)
 336
 337   (** functional part of the "exact" tactic *)
 338 let exact_tac ~status:(proof, goal) ~term =
 339  (* Assumption: the term bo must be closed in the current context *)
 340  let metasenv =
 341   match proof with
 342      None -> assert false
 343    | Some (_,metasenv,_,_) -> metasenv
 344  in
 345  let metano,context,ty =
 346   match goal with
 347      None -> assert false
 348    | Some metano -> List.find (function (m,_,_) -> m=metano) metasenv
 349  in
 350  let module T = CicTypeChecker in
 351  let module R = CicReduction in
 352  if R.are_convertible context (T.type_of_aux' metasenv context term) ty then
 353   begin
 354    let (newproof, metasenv') =
 355      subst_meta_in_proof proof metano term [] in
 356    let newgoal =
 357     (match metasenv' with
 358        [] -> None
 359      | (n,_,_)::_ -> Some n)
 360    in
 361    (newproof, newgoal)
 362   end
 363  else
 364   raise (Fail "The type of the provided term is not the one expected.")
 365
 366
 367 (* not really "primite" tactics .... *)
 368
 369 let elim_intros_simpl_tac ~status:(proof, goal) ~term =
 370  let module T = CicTypeChecker in
 371  let module U = UriManager in
 372  let module R = CicReduction in
 373  let module C = Cic in
 374   let curi,metasenv =
 375    match proof with
 376       None -> assert false
 377     | Some (curi,metasenv,_,_) -> curi,metasenv
 378   in
 379   let metano,context,ty =
 380    match goal with
 381       None -> assert false
 382     | Some metano ->
 383        List.find (function (m,_,_) -> m=metano) metasenv
 384   in
 385    let termty = T.type_of_aux' metasenv context term in
 386    let uri,cookingno,typeno,args =
 387     match termty with
 388        C.MutInd (uri,cookingno,typeno) -> (uri,cookingno,typeno,[])
 389      | C.Appl ((C.MutInd (uri,cookingno,typeno))::args) ->
 390          (uri,cookingno,typeno,args)
 391      | _ ->
 392          prerr_endline ("MALFATTORE" ^ (CicPp.ppterm termty));
 393          flush stderr;
 394          raise NotAnInductiveTypeToEliminate
 395    in
 396     let eliminator_uri =
 397      let buri = U.buri_of_uri uri in
 398      let name =
 399       match CicEnvironment.get_cooked_obj uri cookingno with
 400          C.InductiveDefinition (tys,_,_) ->
 401           let (name,_,_,_) = List.nth tys typeno in
 402            name
 403        | _ -> assert false
 404      in
 405      let ext =
 406       match T.type_of_aux' metasenv context ty with
 407          C.Sort C.Prop -> "_ind"
 408        | C.Sort C.Set  -> "_rec"
 409        | C.Sort C.Type -> "_rect"
 410        | _ -> assert false
 411      in
 412       U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
 413     in
 414      let eliminator_cookingno =
 415       UriManager.relative_depth curi eliminator_uri 0
 416      in
 417      let eliminator_ref = C.Const (eliminator_uri,eliminator_cookingno) in
 418       let ety =
 419        T.type_of_aux' [] [] eliminator_ref
 420       in
 421        let (econclusion,newmetas,arguments,newmeta,lastmeta) =
 422 (*
 423         new_metasenv_for_apply context ety
 424 *)
 425         new_metasenv_for_apply_intros proof context ety
 426        in
 427         (* Here we assume that we have only one inductive hypothesis to *)
 428         (* eliminate and that it is the last hypothesis of the theorem. *)
 429         (* A better approach would be fingering the hypotheses in some  *)
 430         (* way.                                                         *)
 431         let meta_of_corpse =
 432          let (_,canonical_context,_) =
 433           List.find (function (m,_,_) -> m=(lastmeta - 1)) newmetas
 434          in
 435           let irl =
 436            identity_relocation_list_for_metavariable canonical_context
 437           in
 438            Cic.Meta (lastmeta - 1, irl)
 439         in
 440         let newmetasenv = newmetas @ metasenv in
 441         let subst1,newmetasenv' =
 442          CicUnification.fo_unif newmetasenv context term meta_of_corpse
 443         in
 444          let ueconclusion = CicUnification.apply_subst subst1 econclusion in
 445           (* The conclusion of our elimination principle is *)
 446           (*  (?i farg1 ... fargn)                         *)
 447           (* The conclusion of our goal is ty. So, we can   *)
 448           (* eta-expand ty w.r.t. farg1 .... fargn to get   *)
 449           (* a new ty equal to (P farg1 ... fargn). Now     *)
 450           (* ?i can be instantiated with P and we are ready *)
 451           (* to refine the term.                            *)
 452           let emeta, fargs =
 453            match ueconclusion with
 454 (*CSC: Code to be used for Apply
 455               C.Appl ((C.Meta (emeta,_))::fargs) -> emeta,fargs
 456             | C.Meta (emeta,_) -> emeta,[]
 457 *)
 458 (*CSC: Code to be used for ApplyIntros *)
 459               C.Appl (he::fargs) ->
 460                let rec find_head =
 461                 function
 462                    C.Meta (emeta,_) -> emeta
 463                  | C.Lambda (_,_,t) -> find_head t
 464                  | C.LetIn (_,_,t) -> find_head t
 465                  | _ ->raise NotTheRightEliminatorShape
 466                in
 467                 find_head he,fargs
 468             | C.Meta (emeta,_) -> emeta,[]
 469 (* *)
 470             | _ -> raise NotTheRightEliminatorShape
 471           in
 472            let ty' = CicUnification.apply_subst subst1 ty in
 473            let eta_expanded_ty =
 474 (*CSC: newmetasenv' era metasenv ??????????? *)
 475             List.fold_left (eta_expand newmetasenv' context) ty' fargs
 476            in
 477             let subst2,newmetasenv'' =
 478 (*CSC: passo newmetasenv', ma alcune variabili sono gia' state sostituite
 479 da subst1!!!! Dovrei rimuoverle o sono innocue?*)
 480              CicUnification.fo_unif
 481               newmetasenv' context ueconclusion eta_expanded_ty
 482             in
 483              let in_subst_domain i =
 484               let eq_to_i = function (j,_) -> i=j in
 485                List.exists eq_to_i subst1 ||
 486                List.exists eq_to_i subst2
 487              in
 488 (*CSC: codice per l'elim
 489               (* When unwinding the META that corresponds to the elimination *)
 490               (* predicate (which is emeta), we must also perform one-step   *)
 491               (* beta-reduction. apply_subst doesn't need the context. Hence *)
 492               (* the underscore.                                             *)
 493               let apply_subst _ t =
 494                let t' = CicUnification.apply_subst subst1 t in
 495                 CicUnification.apply_subst_reducing
 496                  subst2 (Some (emeta,List.length fargs)) t'
 497               in
 498 *)
 499 (*CSC: codice per l'elim_intros_simpl. Non effettua semplificazione. *)
 500               let apply_subst context t =
 501                let t' = CicUnification.apply_subst (subst1@subst2) t in
 502                 ProofEngineReduction.simpl context t'
 503               in
 504 (* *)
 505                 let old_uninstantiatedmetas,new_uninstantiatedmetas =
 506                  classify_metas newmeta in_subst_domain apply_subst
 507                   newmetasenv''
 508                 in
 509                  let arguments' = List.map (apply_subst context) arguments in
 510                   let bo' = Cic.Appl (eliminator_ref::arguments') in
 511                    let newmetasenv''' =
 512                     new_uninstantiatedmetas@old_uninstantiatedmetas
 513                    in
 514                     let (newproof, newmetasenv'''') =
 515                      (* When unwinding the META that corresponds to the *)
 516                      (* elimination predicate (which is emeta), we must *)
 517                      (* also perform one-step beta-reduction.           *)
 518                      (* The only difference w.r.t. apply_subst is that  *)
 519                      (* we also substitute metano with bo'.             *)
 520                      (*CSC: Nota: sostituire nuovamente subst1 e' superfluo, *)
 521                      (*CSC: no?                                              *)
 522 (*CSC: codice per l'elim
 523                      let apply_subst' t =
 524                       let t' = CicUnification.apply_subst subst1 t in
 525                        CicUnification.apply_subst_reducing
 526                         ((metano,bo')::subst2)
 527                         (Some (emeta,List.length fargs)) t'
 528                      in
 529 *)
 530 (*CSC: codice per l'elim_intros_simpl *)
 531                      let apply_subst' t =
 532                       CicUnification.apply_subst
 533                        ((metano,bo')::(subst1@subst2)) t
 534                      in
 535 (* *)
 536                       subst_meta_and_metasenv_in_proof
 537                         proof metano apply_subst' newmetasenv'''
 538                     in
 539                      (newproof,
 540                       (match newmetasenv'''' with
 541                       | [] -> None
 542                       | (i,_,_)::_ -> Some i))
 543