X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=627885cb743628ed01c7b8b2ec04d6122ed2f23f;hb=a90c31c1b53222bd6d57360c5ba5c2d0fe7d5207;hp=aebda4bce746e543ed9d0f102f3329fa22e1bcae;hpb=4377e950998c9c63937582952a79975947aa9a45;p=helm.git diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index aebda4bce..627885cb7 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -11,8 +11,8 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -(*let pp m = prerr_endline (Lazy.force m);;*) -let pp _ = ();; +let pp m = prerr_endline (Lazy.force m);; +(* let pp _ = ();; *) let fresh_name = let i = ref 0 in @@ -46,13 +46,19 @@ let rec mk_prods l t = | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t) ;; -let rec mk_arrows ?(pattern=false) xs ys selection target = +let rec mk_lambdas l t = + match l with + [] -> t + | hd::tl -> CicNotationPt.Binder (`Lambda, (mk_id hd, None), mk_lambdas tl t) +;; + +let rec mk_arrows xs ys selection target = match selection,xs,ys with [],[],[] -> target - | false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target + | false :: l,x::xs,y::ys -> mk_arrows xs ys l target | true :: l,x::xs,y::ys -> - CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then CicNotationPt.Implicit `JustOne else mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])), - mk_arrows ~pattern xs ys l target) + CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])), + mk_arrows xs ys l target) | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type") ;; @@ -65,30 +71,29 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) ;; -let mk_inverter name is_ind it leftno ?selection outsort status baseuri = +let mk_inverter name it leftno ?selection outsort status baseuri = pp (lazy ("leftno = " ^ string_of_int leftno)); let _,ind_name,ty,cl = it in pp (lazy ("arity: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] ty)); let ncons = List.length cl in - (**)let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in + (*let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in let params = List.rev_map (function name,_ -> mk_id name) params in - pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));(**) + pp (lazy ("lunghezza params = " ^ string_of_int (List.length params)));*) let args,sort= split_arity ~subst:[] [] ty in pp (lazy ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort)); - (**)let args = List.rev_map (function name,_ -> mk_id name) args in - pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));(**) + (*let args = List.rev_map (function name,_ -> mk_id name) args in + pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));*) let nparams = List.length args in - pp (lazy ("nparams = " ^ string_of_int nparams)); - if nparams = 0 + if nparams <= leftno then raise (Failure "inverter: the type must have at least one right parameter") else - let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+nparams+1)) in + let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (nparams+1)) in pp (lazy ("lunghezza xs = " ^ string_of_int (List.length xs))); let ls, rs = HExtlib.split_nth leftno xs in pp (lazy ("lunghezza ls = " ^ string_of_int (List.length ls))); pp (lazy ("lunghezza rs = " ^ string_of_int (List.length rs))); - let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (leftno+nparams+1)) in + let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (nparams+1)) in let _id_xs = List.map mk_id xs in let id_ls = List.map mk_id ls in @@ -107,6 +112,8 @@ let mk_inverter name is_ind it leftno ?selection outsort status baseuri = in let prods = mk_arrows id_rs id_ys selection pred in + let lambdas = mk_lambdas (ys@["p"]) prods in + let hyplist = let rec hypaux k = function 0 -> [] @@ -116,18 +123,19 @@ let mk_inverter name is_ind it leftno ?selection outsort status baseuri = pp (lazy ("lunghezza ys = " ^ string_of_int (List.length ys))); let outsort, suffix = NCicElim.ast_of_sort outsort in - let theorem = - mk_prods xs - (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))), - mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), mk_appl (mk_id "P"::id_rs))))) - in - let status, theorem = - GrafiteDisambiguate.disambiguate_nobj status ~baseuri - (baseuri ^ name ^ ".def",0, - CicNotationPt.Theorem - (`Theorem,name,theorem, - Some (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) + let theorem = mk_prods xs + (CicNotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (CicNotationPt.Sort outsort))), + mk_prods hyplist (CicNotationPt.Binder (`Forall, (mk_id "Hterm", (*Some (mk_appl (List.map mk_id (ind_name::xs)))) *) + Some (CicNotationPt.Implicit `JustOne)), + mk_appl (mk_id "P"::id_rs))))) in + let t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @ + List.map mk_id hyplist @ + CicNotationPt.Implicit `Vector::[mk_id "Hterm"] ) in + let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri + (baseuri ^ name ^ ".def", + 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some + (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) in let uri,height,nmenv,nsubst,nobj = theorem in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in let status = status#set_obj theorem in @@ -139,37 +147,24 @@ let mk_inverter name is_ind it leftno ?selection outsort status baseuri = mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in let cut = mk_appl [CicNotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem), - -CicNotationPt.Implicit (`Tagged "end")); + CicNotationPt.Implicit (`Tagged "end")); CicNotationPt.Implicit (`Tagged "cut")] in let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in - let where = - "",0,(None,[], - Some ( - mk_arrows ~pattern:true - (HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys)) - (HExtlib.mk_list CicNotationPt.UserInput (List.length ys)) - selection CicNotationPt.UserInput)) in - let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in - let status = - NTactics.block_tac - (NTactics.branch_tac :: - NTactics.case_tac "inv" :: - (intros @ - [NTactics.apply_tac ("",0,cut); - NTactics.branch_tac; - NTactics.case_tac "end"; - NTactics.apply_tac ("",0,mk_id "Hcut"); - NTactics.apply_tac ("",0,mk_id "refl"); - NTactics.shift_tac; - elim_tac ~what:("",0,mk_id "Hterm") ~where; - NTactics.branch_tac ~force:true] @ - HExtlib.list_concat ~sep:[NTactics.shift_tac] - (List.map (fun id-> [NTactics.apply_tac ("",0,mk_id id)]) hyplist) @ - [NTactics.merge_tac; - NTactics.merge_tac; - NTactics.merge_tac; - NTactics.skip_tac])) status in + let status = NTactics.block_tac + (NTactics.branch_tac :: + NTactics.case_tac "inv" :: + (intros @ + [NTactics.apply_tac ("",0,cut); + NTactics.branch_tac; + NTactics.case_tac "end"; + NTactics.apply_tac ("",0,mk_id "Hcut"); + NTactics.apply_tac ("",0,mk_id "refl_eq"); + NTactics.shift_tac; + (*NTactics.case_tac "cut";*) + NTactics.apply_tac ("",0,t); + NTactics.merge_tac; + NTactics.merge_tac; + NTactics.skip_tac])) status in pp (lazy "inv 3"); status,status#obj ;;