helm/software/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 fresh_name =
  15  let i = ref 0 in
  16  function () ->
  17   incr i;
  18   "z" ^ string_of_int !i
  19 ;;
  20
  21 let mk_id id =
  22  let id = if id = "_" then fresh_name () else id in
  23   CicNotationPt.Ident (id,None)
  24 ;;
  25
  26 let rec split_arity ~subst context te =
  27   match NCicReduction.whd ~subst context te with
  28    | NCic.Prod (name,so,ta) ->
  29        split_arity ~subst ((name, (NCic.Decl so))::context) ta
  30    | t -> context, t
  31 ;;
  32
  33 let mk_appl =
  34  function
  35     [] -> assert false
  36   | [x] -> x
  37   | l -> CicNotationPt.Appl l
  38 ;;
  39
  40 let rec mk_prods l t =
  41   match l with
  42     [] -> t
  43   | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t)
  44 ;;
  45
  46 let rec mk_lambdas l t =
  47   match l with
  48     [] -> t
  49   | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t)
  50 ;;
  51
  52 let rec mk_arrows xs ys selection target =
  53   match selection,xs,ys with
  54     [],[],[] -> target
  55   | false :: l,x::xs,y::ys -> mk_arrows xs ys l target
  56   | true :: l,x::xs,y::ys  ->
  57      CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])),
  58                            mk_arrows xs ys l target)
  59   | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type")
  60 ;;
  61
  62 let subst_metasenv_and_fix_names status =
  63   let u,h,metasenv, subst,o = status#obj in
  64   let o =
  65     NCicUntrusted.map_obj_kind ~skip_body:true
  66      (NCicUntrusted.apply_subst subst []) o
  67   in
  68    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o)
  69 ;;
  70
  71 let mk_inverter name it leftno ?selection outsort status baseuri =
  72  prerr_endline ("leftno = " ^ string_of_int leftno);
  73  let _,ind_name,ty,cl = it in
  74  prerr_endline ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty);
  75  let ncons = List.length cl in
  76  (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
  77  let params = List.rev_map (function name,_ -> mk_id name) params in
  78  prerr_endline ("lunghezza params = " ^ string_of_int (List.length params));*)
  79  let args,sort= split_arity ~subst:[] [] ty in
  80  prerr_endline ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort);
  81  (*let args = List.rev_map (function name,_ -> mk_id name) args in
  82  prerr_endline ("lunghezza args = " ^ string_of_int (List.length args));*)
  83  let nparams = List.length args in
  84  prerr_endline ("nparams = " ^ string_of_int nparams);
  85
  86  let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in
  87  prerr_endline ("lunghezza xs = " ^ string_of_int (List.length xs));
  88  let ls, rs = HExtlib.split_nth leftno xs in
  89  prerr_endline ("lunghezza ls = " ^ string_of_int (List.length ls));
  90  prerr_endline ("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) (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 lambdas = mk_lambdas (ys@["p"]) prods in
 111
 112  let hyplist =
 113    let rec hypaux k = function
 114        0 -> []
 115      | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1)
 116    in (hypaux 1 ncons)
 117  in
 118  prerr_endline ("lunghezza ys = " ^ string_of_int (List.length ys));
 119
 120  let outsort, suffix = NCicElim.ast_of_sort outsort in
 121  let theorem = mk_prods xs
 122                 (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))),
 123                 mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *)
 124                                   Some (CicNotationPt.Implicit `JustOne)),
 125                                   mk_appl (mk_id "P"::id_rs)))))
 126  in
 127  let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix); lambdas] @
 128                    List.map mk_id hyplist @
 129                    CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in
 130
 131  let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri
 132                          (baseuri ^ name ^ ".def",
 133                            0,CicNotationPt.Theorem (`Theorem,name,theorem,Some
 134                            (CicNotationPt.Implicit (`Tagged "inv")),`Regular)) in
 135  let uri,height,nmenv,nsubst,nobj = theorem in
 136  let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
 137  let status = status#set_obj theorem in
 138  let status = status#set_stack ninitial_stack in
 139  let status = subst_metasenv_and_fix_names status in
 140
 141  let cut_theorem =
 142    let rs = List.map (fun x -> mk_id x) rs in
 143      mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in
 144
 145  let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem),
 146                     CicNotationPt.Implicit (`Tagged "end"));
 147                     CicNotationPt.Implicit (`Tagged "cut")] in
 148
 149  let intros = List.map (fun x -> NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in
 150
 151  let status = NTactics.block_tac
 152                         (NTactics.branch_tac::
 153                          NTactics.case_tac "inv"::
 154                          (intros @
 155                           [NTactics.apply_tac ("",0,cut);
 156                            NTactics.branch_tac;
 157                            NTactics.case_tac "end";
 158                            NTactics.apply_tac ("",0,mk_id "Hcut");
 159                            NTactics.apply_tac ("",0,mk_id "refl_eq");
 160                            NTactics.shift_tac;
 161                            NTactics.case_tac "cut";
 162                            NTactics.apply_tac ("",0,t);
 163                            NTactics.merge_tac;
 164                            NTactics.merge_tac;
 165                            NTactics.skip_tac])) status in
 166  status,status#obj
 167 ;;