matitaB/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,`Ambiguous)
  27 ;;
  28
  29 let rec split_arity status ~subst context te =
  30   match NCicReduction.whd status ~subst context te with
  31    | NCic.Prod (name,so,ta) ->
  32        split_arity status ~subst ((name, (NCic.Decl so))::context) ta
  33    | t -> context, t
  34 ;;
  35
  36 let mk_appl =
  37  function
  38     [] -> assert false
  39   | [x] -> x
  40   | l -> NotationPt.Appl l
  41 ;;
  42
  43 let rec mk_prods l t =
  44   match l with
  45     [] -> t
  46   | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
  47 ;;
  48
  49 let rec mk_arrows ?(pattern=false) xs ys selection target =
  50   match selection,xs,ys with
  51     [],[],[] -> target
  52   | false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target
  53   | true :: l,x::xs,y::ys  ->
  54      NotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then NotationPt.Implicit `JustOne else mk_id "eq" ; NotationPt.Implicit `JustOne;x;y])),
  55                            mk_arrows ~pattern xs ys l target)
  56   | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
  57 ;;
  58
  59 let subst_metasenv_and_fix_names status =
  60   let u,h,metasenv, subst,o = status#obj in
  61   let o =
  62     NCicUntrusted.map_obj_kind ~skip_body:true
  63      (NCicUntrusted.apply_subst status subst []) o
  64   in
  65    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
  66 ;;
  67
  68 let mk_inverter name is_ind it leftno ?selection outsort (status: #NCic.status) baseuri =
  69  pp (lazy ("leftno = " ^ string_of_int leftno));
  70  let _,ind_name,ty,cl = it in
  71  pp (lazy ("arity: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
  72  let ncons = List.length cl in
  73  (**)let params,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in
  74  let params = List.rev_map (function name,_ -> mk_id name) params in
  75  pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));(**)
  76  let args,sort= split_arity status ~subst:[] [] ty in
  77  pp (lazy ("arity sort: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:args sort));
  78  (**)let args = List.rev_map (function name,_ -> mk_id name) args in
  79  pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));(**)
  80  let nparams = List.length args in
  81
  82  pp (lazy ("nparams = " ^ string_of_int nparams));
  83  if nparams = 0
  84    then raise (Failure "inverter: the type must have at least one right parameter")
  85    else
  86      let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+nparams+1)) in
  87      pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs)));
  88      let ls, rs = HExtlib.split_nth leftno xs in
  89      pp (lazy ("lunghezza ls = " ^ string_of_int (List.length ls)));
  90      pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs)));
  91      let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (leftno+nparams+1)) in
  92
  93      let _id_xs = List.map mk_id xs in
  94      let id_ls = List.map mk_id ls in
  95      let id_rs = List.map mk_id rs in
  96      let id_ys = List.map mk_id ys in
  97
  98      (* pseudocode  let t = Lambda y1 ... yr. xs_ = ys_ -> pred *)
  99
 100      (* check: assuming we have more than one right parameter *)
 101      (* pred := P yr- *)
 102      let pred = mk_appl ((mk_id "P")::id_ys) in
 103
 104      let selection = match selection with
 105          None -> HExtlib.mk_list true (List.length ys)
 106        | Some s -> s
 107      in
 108      let prods = mk_arrows id_rs id_ys selection pred in
 109
 110      let hyplist =
 111        let rec hypaux k = function
 112            0 -> []
 113          | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1)
 114        in (hypaux 1 ncons)
 115      in
 116      pp (lazy ("lunghezza ys = " ^ string_of_int (List.length ys)));
 117
 118      let outsort, suffix = NCicElim.ast_of_sort outsort in
 119      let theorem =
 120       mk_prods xs
 121        (NotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (NotationPt.Sort outsort))),
 122        mk_prods hyplist (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), mk_appl (mk_id "P"::id_rs)))))
 123      in
 124      let status, theorem =
 125       GrafiteDisambiguate.disambiguate_nobj status ~baseuri
 126        (baseuri ^ name ^ ".def",0,
 127          NotationPt.Theorem
 128           (`Theorem,name,theorem,
 129             Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
 130      in
 131      let uri,height,nmenv,nsubst,nobj = theorem in
 132      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
 133      let status = status#set_obj theorem in
 134      let status = status#set_stack ninitial_stack in
 135      let status = subst_metasenv_and_fix_names status in
 136
 137      let cut_theorem =
 138        let rs = List.map (fun x -> mk_id x) rs in
 139          mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in
 140
 141      let cut = mk_appl [NotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
 142
 143 NotationPt.Implicit (`Tagged "end"));
 144                         NotationPt.Implicit (`Tagged "cut")] in
 145      let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
 146      let where =
 147       "",0,(None,[],
 148        Some (
 149         mk_arrows ~pattern:true
 150          (HExtlib.mk_list (NotationPt.Implicit `JustOne) (List.length ys))
 151          (HExtlib.mk_list NotationPt.UserInput (List.length ys))
 152          selection NotationPt.UserInput)) in
 153      let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in
 154      let status =
 155       NTactics.block_tac
 156        (NTactics.branch_tac ::
 157         NTactics.case_tac "inv" ::
 158         (intros @
 159          [NTactics.apply_tac ("",0,cut);
 160           NTactics.branch_tac;
 161           NTactics.case_tac "end";
 162           NTactics.apply_tac ("",0,mk_id "Hcut");
 163           NTactics.apply_tac ("",0,mk_id "refl");
 164           NTactics.shift_tac;
 165           elim_tac ~what:("",0,mk_id "Hterm") ~where;
 166           NTactics.branch_tac ~force:true] @
 167            HExtlib.list_concat ~sep:[NTactics.shift_tac]
 168             (List.map (fun id-> [NTactics.apply_tac ("",0,mk_id id)]) hyplist) @
 169          [NTactics.merge_tac;
 170           NTactics.merge_tac;
 171           NTactics.merge_tac;
 172           NTactics.skip_tac])) status in
 173      pp (lazy "inv 3");
 174      status,status#obj
 175 ;;
 176