matita/components/ng_tactics/nInversion.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 (*let pp m = prerr_endline (Lazy.force m);;*)
  15 let pp _ = ();;
  16
  17 let fresh_name =
  18  let i = ref 0 in
  19  function () ->
  20   incr i;
  21   "z" ^ string_of_int !i
  22 ;;
  23
  24 let mk_id id =
  25  let id = if id = "_" then fresh_name () else id in
  26   NotationPt.Ident (id,None)
  27 ;;
  28
  29 let mk_sym s = NotationPt.Symbol (s,0);;
  30
  31 let rec split_arity status ~subst context te =
  32   match NCicReduction.whd status ~subst context te with
  33    | NCic.Prod (name,so,ta) ->
  34        split_arity status ~subst ((name, (NCic.Decl so))::context) ta
  35    | t -> context, t
  36 ;;
  37
  38 let mk_appl =
  39  function
  40     [] -> assert false
  41   | [x] -> x
  42   | l -> NotationPt.Appl l
  43 ;;
  44
  45 let rec mk_prods l t =
  46   match l with
  47     [] -> t
  48   | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
  49 ;;
  50
  51 let rec leibpatt = function
  52   | [] -> NotationPt.UserInput
  53   | false::sel -> leibpatt sel
  54   | true::sel -> NotationPt.Binder (`Forall, (mk_id "_",
  55                      Some (mk_appl [NotationPt.Implicit `JustOne
  56                                    ;NotationPt.Implicit `JustOne
  57                                    ;NotationPt.Implicit `JustOne
  58                                    ;NotationPt.UserInput])),
  59                      leibpatt sel);;
  60 let rec jmeqpatt = function
  61   | [] -> NotationPt.UserInput
  62   | false::sel -> jmeqpatt sel
  63   | true::sel -> NotationPt.Binder (`Forall, (mk_id "_",
  64                      Some (mk_appl [NotationPt.Implicit `JustOne
  65                                    ;NotationPt.Implicit `JustOne
  66                                    ;NotationPt.Implicit `JustOne
  67                                    ;NotationPt.UserInput
  68                                    ;NotationPt.UserInput])),
  69                      jmeqpatt sel);;
  70
  71 let rec mk_arrows ~jmeq xs ys selection target =
  72   match selection,xs,ys with
  73     [],[],[] -> target
  74   | false :: l,_x::xs,_y::ys -> mk_arrows ~jmeq xs ys l target
  75   | true :: l,x::xs,y::ys when jmeq ->
  76      NotationPt.Binder (`Forall, (mk_id "_",
  77        Some (mk_appl [mk_sym "jmsimeq" ;
  78              NotationPt.Implicit `JustOne;x;
  79              NotationPt.Implicit `JustOne;y])),
  80        mk_arrows ~jmeq xs ys l target)
  81   | true :: l,x::xs,y::ys ->
  82      NotationPt.Binder (`Forall, (mk_id "_",
  83        Some (mk_appl [mk_sym "eq" ;
  84              NotationPt.Implicit `JustOne;x;y])),
  85        mk_arrows ~jmeq xs ys l target)
  86   | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
  87 ;;
  88
  89 let subst_metasenv_and_fix_names status =
  90   let u,h,metasenv, subst,o = status#obj in
  91   let o =
  92     NCicUntrusted.map_obj_kind ~skip_body:true
  93      (NCicUntrusted.apply_subst status subst []) o
  94   in
  95    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
  96 ;;
  97
  98 let mk_inverter ~jmeq name _is_ind it leftno ?selection outsort (status: #NCic.status) baseuri =
  99  pp (lazy ("leftno = " ^ string_of_int leftno));
 100  let _,ind_name,ty,cl = it in
 101  pp (lazy ("arity: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
 102  let ncons = List.length cl in
 103  (**)let params,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in
 104  let params = List.rev_map (function name,_ -> mk_id name) params in
 105  pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));(**)
 106  let args,sort= split_arity status ~subst:[] [] ty in
 107  pp (lazy ("arity sort: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:args sort));
 108  (**)let args = List.rev_map (function name,_ -> mk_id name) args in
 109  pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));(**)
 110  let nparams = List.length args in
 111
 112  (* the default is a dependent inversion *)
 113  let is_dependent = (selection = None && (jmeq || nparams = 0)) in
 114
 115  pp (lazy ("nparams = " ^ string_of_int nparams));
 116  if (nparams = 0 && not is_dependent)
 117    then raise (Failure "inverter: the type must have at least one right parameter")
 118    else
 119      let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+nparams+1)) in
 120      pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs)));
 121      let ls, rs = HExtlib.split_nth leftno xs in
 122      pp (lazy ("lunghezza ls = " ^ string_of_int (List.length ls)));
 123      pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs)));
 124
 125      (* dependent -> add Hterm to rs *)
 126      let rs = if is_dependent then (rs@["Hterm"]) else rs in
 127
 128      let _id_xs = List.map mk_id xs in
 129      let id_rs = List.map mk_id rs in
 130
 131
 132      let selection =
 133        match selection with
 134          None -> HExtlib.mk_list true (List.length rs)
 135        | Some s -> s
 136      in
 137
 138      let hyplist =
 139        let rec hypaux k = function
 140            0 -> []
 141          | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1)
 142        in (hypaux 1 ncons)
 143      in
 144
 145      let outsort, _suffix = NCicElim.ast_of_sort outsort in
 146      let theorem =
 147       mk_prods xs
 148        (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))),
 149         (NotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length rs)) (NotationPt.Sort outsort))),
 150         mk_prods hyplist (mk_appl (mk_id "P"::id_rs))))))
 151      in
 152      let status, theorem =
 153       let attrs = `Generated, `Theorem, `InversionPrinciple in
 154       GrafiteDisambiguate.disambiguate_nobj status ~baseuri
 155        (baseuri ^ name ^ ".def",0,
 156          NotationPt.Theorem
 157           (name,theorem, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
 158      in
 159      let _uri,_height,nmenv,_nsubst,_nobj = theorem in
 160      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
 161      let status = status#set_obj theorem in
 162      let status = status#set_stack ninitial_stack in
 163      let status = subst_metasenv_and_fix_names status in
 164
 165      let cut_theorem =
 166        let rs = List.map (fun x -> mk_id x) rs in
 167          mk_arrows ~jmeq rs rs selection (mk_appl (mk_id "P"::rs)) in
 168
 169      let cut = mk_appl [NotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
 170
 171 NotationPt.Implicit (`Tagged "end"));
 172                         NotationPt.Implicit (`Tagged "cut")] in
 173      let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["Hterm";"P"]@hyplist) in
 174      let where =
 175       "",0,(None,[],
 176         Some (if jmeq then jmeqpatt selection
 177                      else leibpatt selection)) in
 178      (* let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in *)
 179      let elim_tac ~what ~where s =
 180        try NTactics.elim_tac ~what ~where s
 181        with NTacStatus.Error _ -> NTactics.cases_tac ~what ~where s
 182      in
 183      let status =
 184       NTactics.block_tac
 185        (NTactics.branch_tac ::
 186         NTactics.case_tac "inv" ::
 187         (intros @
 188          [NTactics.apply_tac ("",0,cut);
 189           NTactics.branch_tac;
 190           NTactics.case_tac "end";
 191           NTactics.apply_tac ("",0,mk_id "Hcut");
 192           NTactics.apply_tac ("",0,mk_sym "refl");
 193           NTactics.shift_tac;
 194           elim_tac ~what:("",0,mk_id "Hterm") ~where;
 195           NTactics.branch_tac ~force:true] @
 196            HExtlib.list_concat ~sep:[NTactics.shift_tac]
 197             (List.map (fun id-> [NTactics.apply_tac ("",0,mk_id id)]) hyplist) @
 198          [NTactics.merge_tac;
 199           NTactics.merge_tac;
 200           NTactics.merge_tac;
 201           NTactics.skip_tac])) status in
 202      pp (lazy "inv 3");
 203      status,status#obj
 204 ;;
 205
 206 let mk_inverter name is_ind it leftno ?selection outsort status baseuri =
 207  try mk_inverter ~jmeq:true name is_ind it leftno ?selection outsort status baseuri
 208  with NTacStatus.Error (_s,_) ->
 209    mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri
 210 ;;