helm/software/components/tactics/discriminationTactics.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 let debug = false
  29 let debug_print =
  30   if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
  31 ;;
  32
  33 (* term ha tipo t1=t2; funziona solo se t1 e t2 hanno in testa costruttori
  34 diversi *)
  35
  36 let discriminate_tac ~term =
  37  let module C = Cic in
  38  let module U = UriManager in
  39  let module P = PrimitiveTactics in
  40  let module T = Tacticals in
  41  let true_URI =
  42   match LibraryObjects.true_URI () with
  43      Some uri -> uri
  44    | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
  45  let false_URI =
  46   match LibraryObjects.false_URI () with
  47      Some uri -> uri
  48    | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
  49  let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
  50  let find_discriminating_consno t1 t2 =
  51    let rec aux t1 t2 =
  52      match t1, t2 with
  53      | C.MutConstruct _, C.MutConstruct _ when t1 = t2 -> None
  54      | C.Appl ((C.MutConstruct _ as constr1) :: args1),
  55        C.Appl ((C.MutConstruct _ as constr2) :: args2)
  56        when constr1 = constr2 ->
  57          let rec aux_list l1 l2 =
  58            match l1, l2 with
  59            | [], [] -> None
  60            | hd1 :: tl1, hd2 :: tl2 ->
  61                (match aux hd1 hd2 with
  62                | None -> aux_list tl1 tl2
  63                | Some _ as res -> res)
  64            | _ -> (* same constructor applied to a different number of args *)
  65                assert false
  66          in
  67          aux_list args1 args2
  68      | ((C.MutConstruct (_,_,consno1,subst1)),
  69        (C.MutConstruct (_,_,consno2,subst2)))
  70      | ((C.MutConstruct (_,_,consno1,subst1)),
  71        (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
  72      | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
  73        (C.MutConstruct (_,_,consno2,subst2)))
  74      | ((C.Appl ((C.MutConstruct (_,_,consno1,subst1)) :: _)),
  75        (C.Appl ((C.MutConstruct (_,_,consno2,subst2)) :: _)))
  76        when (consno1 <> consno2) || (subst1 <> subst2) ->
  77          Some consno2
  78      | _ -> fail "not a discriminable equality"
  79    in
  80    aux t1 t2
  81  in
  82  let mk_branches_and_outtype turi typeno consno context args =
  83     (* a list of "True" except for the element in position consno which
  84      * is "False" *)
  85     match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
  86     | C.InductiveDefinition (ind_type_list,_,paramsno,_)  ->
  87         let _,_,rty,constructor_list = List.nth ind_type_list typeno in
  88         let false_constr_id,_ = List.nth constructor_list (consno - 1) in
  89         let branches =
  90          List.map
  91            (fun (id,cty) ->
  92              (* dubbio: e' corretto ridurre in questo context ??? *)
  93              let red_ty = CicReduction.whd context cty in
  94              let rec aux t k =
  95                match t with
  96                | C.Prod (_,_,target) when (k <= paramsno) ->
  97                    CicSubstitution.subst (List.nth args (k-1))
  98                      (aux target (k+1))
  99                | C.Prod (binder,source,target) when (k > paramsno) ->
 100                    C.Lambda (binder, source, (aux target (k+1)))
 101                | _ ->
 102                    if (id = false_constr_id)
 103                    then (C.MutInd(false_URI,0,[]))
 104                    else (C.MutInd(true_URI,0,[]))
 105              in
 106              (CicSubstitution.lift 1 (aux red_ty 1)))
 107            constructor_list in
 108         let outtype =
 109          let seed = ref 0 in
 110          let rec mk_lambdas rev_left_args =
 111           function
 112              0, args, C.Prod (_,so,ta) ->
 113               C.Lambda
 114                (C.Name (incr seed; "x" ^ string_of_int !seed),
 115                so,
 116                mk_lambdas rev_left_args (0,args,ta))
 117            | 0, args, C.Sort _ ->
 118               let rec mk_rels =
 119                function
 120                   0 -> []
 121                 | n -> C.Rel n :: mk_rels (n - 1) in
 122               let argsno = List.length args in
 123                C.Lambda
 124                 (C.Name "x",
 125                  (if argsno + List.length rev_left_args > 0 then
 126                    C.Appl
 127                     (C.MutInd (turi, typeno, []) ::
 128                      (List.map
 129                       (CicSubstitution.lift (argsno + 1))
 130                       (List.rev rev_left_args)) @
 131                      mk_rels argsno)
 132                   else
 133                    C.MutInd (turi,typeno,[])),
 134                  C.Sort C.Prop)
 135            | 0, _, _ -> assert false (* seriously screwed up *)
 136            | n, he::tl, C.Prod (_,_,ta) ->
 137               mk_lambdas (he::rev_left_args)(n-1,tl,CicSubstitution.subst he ta)
 138            | n,_,_ ->
 139               assert false (* we should probably reduce in some context *)
 140          in
 141           mk_lambdas [] (paramsno, args, rty)
 142         in
 143          branches, outtype
 144     | _ -> assert false
 145  in
 146  let discriminate'_tac ~term status =
 147   let (proof, goal) = status in
 148   let _,metasenv,_subst,_,_, _ = proof in
 149   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 150   let termty,_ =
 151     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
 152   in
 153   match termty with
 154    | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
 155      when LibraryObjects.is_eq_URI equri ->
 156       let turi,typeno,exp_named_subst,args =
 157         match tty with
 158         | (C.MutInd (turi,typeno,exp_named_subst)) ->
 159             turi,typeno,exp_named_subst,[]
 160         | (C.Appl (C.MutInd (turi,typeno,exp_named_subst)::args)) ->
 161             turi,typeno,exp_named_subst,args
 162         | _ -> fail "not a discriminable equality"
 163       in
 164       let consno =
 165         match find_discriminating_consno t1 t2 with
 166         | Some consno -> consno
 167         | None -> fail "discriminating terms are structurally equal"
 168       in
 169       let branches,outtype =
 170        mk_branches_and_outtype turi typeno consno context args
 171       in
 172       ProofEngineTypes.apply_tactic
 173        (T.then_
 174          ~start:(EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
 175          ~continuation:
 176            (T.then_
 177              ~start:
 178                (ReductionTactics.change_tac
 179                  ~pattern:(ProofEngineTypes.conclusion_pattern None)
 180                  (fun _ m u ->
 181                    C.Appl [
 182                      C.Lambda ( C.Name "x", tty,
 183                        C.MutCase (turi, typeno, outtype, (C.Rel 1), branches));
 184                      t2 ],
 185                    m, u))
 186              ~continuation:
 187                (T.then_
 188                  ~start:
 189                    (EqualityTactics.rewrite_simpl_tac
 190                      ~direction:`RightToLeft
 191                      ~pattern:(ProofEngineTypes.conclusion_pattern None)
 192                      term [])
 193                  ~continuation:
 194                    (IntroductionTactics.constructor_tac ~n:1)))) status
 195     | _ -> fail "not an equality"
 196   in
 197   ProofEngineTypes.mk_tactic (discriminate'_tac ~term)
 198 ;;
 199
 200 let exn_nonproj =
 201   ProofEngineTypes.Fail (lazy "Injection: not a projectable equality");;
 202 let exn_noneq =
 203   ProofEngineTypes.Fail (lazy "Injection: not an equality");;
 204 let exn_nothingtodo =
 205   ProofEngineTypes.Fail (lazy "Nothing to do");;
 206 let exn_discrnonind =
 207   ProofEngineTypes.Fail (lazy "Discriminate: object is not an Inductive Definition: it's imposible");;
 208 let exn_injwronggoal =
 209   ProofEngineTypes.Fail (lazy "Injection: goal after cut is not correct");;
 210 let exn_noneqind =
 211   ProofEngineTypes.Fail (lazy "Injection: not an equality over elements of an inductive type");;
 212
 213 let pp ctx t =
 214   let names = List.map (function Some (n,_) -> Some n | None -> None) ctx in
 215   CicPp.pp t names
 216 ;;
 217
 218 let rec injection_tac ~first_time ~term ~liftno ~continuation =
 219  let module C = Cic in
 220  let module CR = CicReduction in
 221  let module U = UriManager in
 222  let module P = PrimitiveTactics in
 223  let module T = Tacticals in
 224  let module PST = ProofEngineStructuralRules in
 225  let module PET = ProofEngineTypes in
 226  let are_convertible hd1 hd2 metasenv context =
 227    fst (CR.are_convertible ~metasenv context hd1 hd2 CicUniv.empty_ugraph)
 228  in
 229  let injection_tac ~term status =
 230   let (proof, goal) = status in
 231   let _,metasenv,_subst, _,_, _ = proof in
 232   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 233   let term = CicSubstitution.lift liftno term in
 234   let termty,_ =
 235     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
 236   in
 237   debug_print (lazy ("\ninjection su: " ^ pp context termty));
 238   let tac =
 239     match termty with
 240     | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
 241       when LibraryObjects.is_eq_URI equri -> begin
 242         match (CicReduction.whd ~delta:true context tty) with
 243         | C.MutInd (turi,typeno,ens)
 244         | C.Appl (C.MutInd (turi,typeno,ens)::_) -> begin
 245             match t1,t2 with
 246             | C.MutConstruct (uri1,typeno1,consno1,ens1),
 247               C.MutConstruct (uri2,typeno2,consno2,ens2)
 248               when (uri1 = uri2) && (typeno1 = typeno2) &&
 249                     (consno1 = consno2) && (ens1 = ens2) ->
 250                 if first_time then raise exn_nothingtodo
 251                 else continuation ~liftno
 252             | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1),
 253               C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2)
 254               when (uri1 = uri2) && (typeno1 = typeno2) &&
 255               (consno1 = consno2) && (ens1 = ens2) ->
 256                 let rec traverse_list i l1 l2 =
 257                   match l1,l2 with
 258                   | [],[] when first_time -> continuation
 259                   | [],[] -> begin
 260                      match term with
 261                      | C.Rel n -> begin
 262                         match List.nth context (n-1) with
 263                         | Some (C.Name id,_) ->
 264                            fun ~liftno ->
 265                              T.then_ ~start:(PST.clear ~hyps:[id])
 266                                ~continuation:(continuation ~liftno)
 267                         | _ -> assert false
 268                         end
 269                      | _ -> assert false
 270                      end
 271                   | hd1::tl1,hd2::tl2 ->
 272                      if are_convertible hd1 hd2 metasenv context then
 273                        traverse_list (i+1) tl1 tl2
 274                      else
 275                        injection1_tac ~i ~term
 276                          ~continuation:(traverse_list (i+1) tl1 tl2)
 277                   | _ -> assert false
 278                       (* i 2 termini hanno in testa lo stesso costruttore,
 279                        * ma applicato a un numero diverso di termini *)
 280                 in
 281                   traverse_list 1 applist1 applist2 ~liftno
 282             | C.MutConstruct (uri1,typeno1,consno1,ens1),
 283               C.MutConstruct (uri2,typeno2,consno2,ens2)
 284             | C.MutConstruct (uri1,typeno1,consno1,ens1),
 285               C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_)
 286             | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_),
 287               C.MutConstruct (uri2,typeno2,consno2,ens2)
 288             | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::_),
 289               C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::_)
 290               when (consno1 <> consno2) || (ens1 <> ens2) ->
 291                 discriminate_tac ~term
 292             | _ when not first_time -> continuation ~liftno
 293             | _ (* when first_time *) ->
 294                 match term with
 295                 | Cic.Rel i ->
 296                   let name =
 297                     match List.nth context (i-1) with
 298                     | Some (Cic.Name s, Cic.Def _) -> s
 299                     | Some (Cic.Name s, Cic.Decl _) -> s
 300                     | _ -> assert false
 301                   in
 302                   Tacticals.then_
 303                     ~start:(ReductionTactics.simpl_tac
 304                       ~pattern:(None,[name,Cic.Implicit (Some `Hole)],None))
 305                     ~continuation:(injection_tac ~first_time:false ~term ~liftno
 306                       ~continuation)
 307                 | _ -> raise exn_nonproj
 308             end
 309         | _ when not first_time -> continuation ~liftno
 310         | _ (* when first_time *) -> raise exn_nonproj
 311         end
 312     | _ -> raise exn_nonproj
 313   in
 314     PET.apply_tactic tac status
 315  in
 316    PET.mk_tactic (injection_tac ~term)
 317
 318 and injection1_tac ~term ~i ~liftno ~continuation =
 319  let module C = Cic in
 320  let module CTC = CicTypeChecker in
 321  let module CU = CicUniv in
 322  let module S = CicSubstitution in
 323  let module U = UriManager in
 324  let module P = PrimitiveTactics in
 325  let module PET = ProofEngineTypes in
 326  let module T = Tacticals in
 327  let give_name seed = function
 328    | C.Name _ as name -> name
 329    | C.Anonymous -> C.Name (incr seed; "y" ^ string_of_int !seed)
 330  in
 331  let rec mk_rels = function | 0 -> [] | n -> C.Rel n :: (mk_rels (n - 1)) in
 332  let injection1_tac ~term ~i status =
 333   let (proof, goal) = status in
 334   (* precondizione: t1 e t2 hanno in testa lo stesso costruttore ma
 335    * differiscono (o potrebbero differire?) nell'i-esimo parametro
 336    * del costruttore *)
 337   let term = CicSubstitution.lift liftno term in
 338   let _,metasenv,_subst,_,_, _ = proof in
 339   let _,context,_ = CicUtil.lookup_meta goal metasenv in
 340   let termty,_ =
 341     CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph
 342   in
 343   debug_print (lazy ("\ninjection1 su : " ^ pp context termty));
 344   match termty with (* an equality *)
 345   | C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]
 346     when LibraryObjects.is_eq_URI equri ->
 347       let turi,typeno,ens,params =
 348         match tty with (* some inductive type *)
 349         | C.MutInd (turi,typeno,ens) -> turi,typeno,ens,[]
 350         | C.Appl (C.MutInd (turi,typeno,ens)::params) -> turi,typeno,ens,params
 351         | _ -> raise exn_noneqind
 352       in
 353       let t1',t2',consno = (* sono i due sottotermini che differiscono *)
 354         match t1,t2 with
 355         | C.Appl ((C.MutConstruct (uri1,typeno1,consno1,ens1))::applist1),
 356           C.Appl ((C.MutConstruct (uri2,typeno2,consno2,ens2))::applist2)
 357           when (uri1 = uri2) && (typeno1 = typeno2) &&
 358                (consno1 = consno2) && (ens1 = ens2) ->
 359                (* controllo ridondante *)
 360             List.nth applist1 (i-1),List.nth applist2 (i-1),consno2
 361         | _ -> assert false
 362       in
 363       let tty',_ = CTC.type_of_aux' metasenv context t1' CU.empty_ugraph in
 364       let patterns,outtype =
 365         match fst (CicEnvironment.get_obj CicUniv.empty_ugraph turi) with
 366         | C.InductiveDefinition (ind_type_list,_,paramsno,_)->
 367            let left_params, right_params = HExtlib.split_nth paramsno params in
 368            let _,_,_,constructor_list = List.nth ind_type_list typeno in
 369            let i_constr_id,_ = List.nth constructor_list (consno - 1) in
 370            let patterns =
 371              let seed = ref 0 in
 372              List.map
 373                (function (id,cty) ->
 374                  let reduced_cty = CicReduction.whd context cty in
 375                  let rec aux k = function
 376                    | C.Prod (_,_,tgt) when k <= paramsno ->
 377                        let left = List.nth left_params (k-1) in
 378                        aux (k+1) (CicSubstitution.subst left tgt)
 379                    | C.Prod (binder,source,target) when k > paramsno ->
 380                       let binder' = give_name seed binder in
 381                       C.Lambda (binder',source,(aux (k+1) target))
 382                    | _ ->
 383                      let nr_param_constr = k - paramsno - 1 in
 384                      if id = i_constr_id then C.Rel (k - i)
 385                      else S.lift nr_param_constr t1'
 386                      (* + 1 per liftare anche il lambda aggiunto
 387                       * esternamente al case *)
 388                  in CicSubstitution.lift 1 (aux 1 reduced_cty))
 389                constructor_list
 390            in
 391            (* this code should be taken from cases_tac *)
 392            let outtype =
 393              let seed = ref 0 in
 394              let rec to_lambdas te head =
 395                match CicReduction.whd context te with
 396                | C.Prod (binder,so,ta) ->
 397                    let binder' = give_name seed binder in
 398                    C.Lambda (binder',so,to_lambdas ta head)
 399                | _ -> head
 400              in
 401              let rec skip_prods params te =
 402                match params, CicReduction.whd context te with
 403                | [], _ -> te
 404                | left::tl, C.Prod (_,_,ta) ->
 405                    skip_prods tl (CicSubstitution.subst left ta)
 406                | _, _ -> assert false
 407              in
 408              let abstracted_tty =
 409                let tty =
 410                  List.fold_left (fun x y -> CicSubstitution.subst y x) tty left_params
 411                in
 412                (* non lift, ma subst coi left! *)
 413                match S.lift 1 tty with
 414                | C.MutInd _ as tty' -> tty'
 415                | C.Appl l ->
 416                    let keep,abstract = HExtlib.split_nth (paramsno +1) l in
 417                    let keep = List.map (S.lift paramsno) keep in
 418                    C.Appl (keep@mk_rels (List.length abstract))
 419                | _ -> assert false
 420              in
 421              match ind_type_list with
 422              | [] -> assert false
 423              | (_,_,ty,_)::_ ->
 424                (* this is in general wrong, do as in cases_tac *)
 425                to_lambdas (skip_prods left_params ty)
 426                  (C.Lambda
 427                    (C.Name "cased", abstracted_tty,
 428                      (* here we should capture right parameters *)
 429                      (* 1 for his Lambda, one for the Lambda outside the match
 430                       * and then one for each to_lambda *)
 431                      S.lift (2+List.length right_params) tty'))
 432           in
 433             patterns,outtype
 434         | _ -> raise exn_discrnonind
 435       in
 436       let cutted = C.Appl [C.MutInd (equri,0,[]) ; tty' ; t1' ; t2'] in
 437       let changed =
 438         C.Appl [ C.Lambda (C.Name "x", tty,
 439                   C.MutCase (turi,typeno,outtype,C.Rel 1,patterns)) ; t1]
 440       in
 441       (* check if cutted and changed are well typed and if t1' ~ changed *)
 442       let go_on =
 443         try
 444           let _,g = CicTypeChecker.type_of_aux' metasenv context  cutted
 445             CicUniv.empty_ugraph
 446           in
 447           let _,g = CicTypeChecker.type_of_aux' metasenv context changed g in
 448           fst (CicReduction.are_convertible ~metasenv context  t1' changed g)
 449         with
 450         | CicTypeChecker.TypeCheckerFailure _ -> false
 451       in
 452       if not go_on then
 453         PET.apply_tactic Tacticals.id_tac status
 454       else
 455         (debug_print (lazy ("CUT: " ^ pp context cutted));
 456         PET.apply_tactic
 457           (T.thens ~start: (P.cut_tac cutted)
 458              ~continuations:
 459                [injection_tac ~first_time:false ~liftno:0 ~term:(C.Rel 1)
 460                   ~continuation:
 461                    (fun ~liftno:x -> continuation ~liftno:(liftno+1+x))
 462                     (* here I need to lift all the continuations by 1;
 463                        since I am setting back liftno to 0, I actually
 464                        need to lift all the continuations by liftno + 1 *)
 465                ;T.then_
 466                   ~start:(PET.mk_tactic
 467                     (fun status ->
 468                       debug_print (lazy "riempo il cut");
 469                       let (proof, goal) = status in
 470                       let _,metasenv,_subst,_,_, _ = proof in
 471                       let _,context,gty =CicUtil.lookup_meta goal metasenv in
 472                       let gty = Unshare.unshare gty in
 473                       let new_t1' =
 474                         match gty with
 475                         | (C.Appl (C.MutInd (_,_,_)::_::t::_)) -> t
 476                         | _ -> raise exn_injwronggoal
 477                       in
 478                       debug_print
 479                         (lazy ("metto questo: " ^ pp context changed));
 480                       debug_print
 481                         (lazy ("al posto di questo: " ^ pp context new_t1'));
 482                       debug_print
 483                         (lazy ("nel goal: " ^ pp context gty));
 484                       debug_print
 485                         (lazy ("nel contesto:\n" ^ CicPp.ppcontext context));
 486                       debug_print
 487                         (lazy ("e poi rewrite con: "^pp context term));
 488                       let rc =
 489                         PET.apply_tactic
 490                           (ReductionTactics.change_tac
 491                             ~pattern:(None, [],
 492                               Some (ProofEngineHelpers.pattern_of
 493                               ~term:gty [new_t1']))
 494                             (fun _ m u -> changed,m,u))
 495                           status
 496                         in rc
 497                       ))
 498                   ~continuation:
 499                     (T.then_
 500                       ~start:
 501                         (EqualityTactics.rewrite_simpl_tac
 502                           ~direction:`LeftToRight
 503                           ~pattern:(PET.conclusion_pattern None)
 504                           term [])
 505                       ~continuation:EqualityTactics.reflexivity_tac)
 506                ])
 507           status)
 508    | _ -> raise exn_noneq
 509  in
 510   PET.mk_tactic (injection1_tac ~term ~i)
 511 ;;
 512
 513 (* destruct performs either injection or discriminate *)
 514 (* equivalent to Coq's "analyze equality"             *)
 515 let destruct_tac =
 516  injection_tac
 517   ~first_time:true ~liftno:0 ~continuation:(fun ~liftno -> Tacticals.id_tac)
 518 ;;