From d0e97750e19af9286400a3e7b161a1c658684848 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 31 Mar 2010 13:49:43 +0000 Subject: [PATCH 1/1] - inversion principles are now generated also for co-inductive types - we use uniformly the cases_tac/elim_tac in the inversion principle From: sacerdot --- .../grafite_engine/grafiteEngine.ml | 122 ++++++++---------- .../components/ng_tactics/nInversion.ml | 85 ++++++------ .../components/ng_tactics/nInversion.mli | 5 +- 3 files changed, 102 insertions(+), 110 deletions(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index 4d7b8ce4e..89673e7d7 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -531,68 +531,54 @@ let record_index_obj = ;; let compute_keys uri height kind = - let mk_item orig_ty spec = - let ty,_,_ = NCicMetaSubst.saturate ~delta:max_int [] [] [] orig_ty 0 in - let keys = - match ty with - | NCic.Const (NReference.Ref (_,NReference.Def h)) - | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Def h))::_) - when h > 0 -> - let ty',_,_= - NCicMetaSubst.saturate ~delta:(h-1) [] [] [] orig_ty 0 in - [ty;ty'] - | _ -> [ty] - in - keys,NCic.Const(NReference.reference_of_spec uri spec) - in - let data = - match kind with - | NCic.Fixpoint (ind,ifl,_) -> - HExtlib.list_mapi - (fun (_,_,rno,ty,_) i -> - if ind then mk_item ty (NReference.Fix (i,rno,height)) - else mk_item ty (NReference.CoFix height)) ifl - | NCic.Inductive (b,lno,itl,_) -> - HExtlib.list_mapi - (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl - @ - List.map - (fun ((_,_,ty),i,j) -> - mk_item ty (NReference.Con (i,j+1,lno))) - (List.flatten - (HExtlib.list_mapi - (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl) - itl)) - | NCic.Constant (_,_,Some _, ty, _) -> - [ mk_item ty (NReference.Def height) ] - | NCic.Constant (_,_,None, ty, _) -> - [ mk_item ty NReference.Decl ] - in - let data = HExtlib.filter_map - (fun (keys, t) -> - let keys = List.filter - (function - | (NCic.Meta _) - | (NCic.Appl (NCic.Meta _::_)) -> false - | _ -> true) - keys - in - if keys <> [] then - begin - HLog.debug ("Indexing:" ^ - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); - HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t -> - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys)); - Some (keys,t) - end - else - begin - HLog.debug ("Not indexing:" ^ - NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); - None - end) - data - in data + let mk_item orig_ty spec = + let keys = NnAuto.keys_of_cic_term [] [] [] orig_ty in + keys,NCic.Const(NReference.reference_of_spec uri spec) + in + let data = + match kind with + | NCic.Fixpoint (ind,ifl,_) -> + HExtlib.list_mapi + (fun (_,_,rno,ty,_) i -> + if ind then mk_item ty (NReference.Fix (i,rno,height)) + else mk_item ty (NReference.CoFix height)) ifl + | NCic.Inductive (b,lno,itl,_) -> + HExtlib.list_mapi + (fun (_,_,ty,_) i -> mk_item ty (NReference.Ind (b,i,lno))) itl + @ + List.map (fun ((_,_,ty),i,j) -> mk_item ty (NReference.Con (i,j+1,lno))) + (List.flatten (HExtlib.list_mapi + (fun (_,_,_,cl) i -> HExtlib.list_mapi (fun x j-> x,i,j) cl) + itl)) + | NCic.Constant (_,_,Some _, ty, _) -> + [ mk_item ty (NReference.Def height) ] + | NCic.Constant (_,_,None, ty, _) -> + [ mk_item ty NReference.Decl ] + in + HExtlib.filter_map + (fun (keys, t) -> + let keys = List.filter + (function + | (NCic.Meta _) + | (NCic.Appl (NCic.Meta _::_)) -> false + | _ -> true) + keys + in + if keys <> [] then + begin + HLog.debug ("Indexing:" ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); + HLog.debug ("With keys:" ^ String.concat "\n" (List.map (fun t -> + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t) keys)); + Some (keys,t) + end + else + begin + HLog.debug ("Not indexing:" ^ + NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t); + None + end) + data ;; let index_obj_for_auto status (uri, height, _, _, kind) = @@ -954,15 +940,17 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = ) (status,`New [] (* uris *)) boxml in let _,_,_,_,nobj = obj in let status = match nobj with - NCic.Inductive (true,leftno,[it],_) -> + NCic.Inductive (is_ind,leftno,[it],_) -> let _,ind_name,ty,cl = it in List.fold_left (fun status outsort -> let status = status#set_ng_mode `ProofMode in try - (let status,invobj = NInversion.mk_inverter - (ind_name ^ "_inv_" ^ (snd (NCicElim.ast_of_sort outsort))) - it leftno outsort status status#baseuri in + (let status,invobj = + NInversion.mk_inverter + (ind_name ^ "_inv_" ^ + (snd (NCicElim.ast_of_sort outsort))) + is_ind it leftno outsort status status#baseuri in let _,_,menv,_,_ = invobj in fst (match menv with [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc) @@ -1099,7 +1087,7 @@ let rec eval_ncommand opts status (text,prefix_len,cmd) = indtyno, NCicEnvironment.get_checked_indtys r | _ -> prerr_endline ("engine: indty =" ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] indty) ; assert false in let it = List.nth tys indtyno in - let status,obj = NInversion.mk_inverter name it leftno ?selection sort + let status,obj = NInversion.mk_inverter name true it leftno ?selection sort status status#baseuri in let _,_,menv,_,_ = obj in (match menv with diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index 4b4b7246d..5be36d001 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -11,7 +11,7 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -(* let pp m = prerr_endline (Lazy.force m);;*) +(*let pp m = prerr_endline (Lazy.force m);;*) let pp _ = ();; let fresh_name = @@ -46,19 +46,13 @@ let rec mk_prods l t = | hd::tl -> CicNotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t) ;; -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 = +let rec mk_arrows ?(pattern=false) xs ys selection target = match selection,xs,ys with [],[],[] -> target - | false :: l,x::xs,y::ys -> mk_arrows xs ys l target + | false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target | true :: l,x::xs,y::ys -> - CicNotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [mk_id "eq" ; CicNotationPt.Implicit `JustOne;x;y])), - mk_arrows xs ys l target) + 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) | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type") ;; @@ -71,7 +65,7 @@ let subst_metasenv_and_fix_names status = status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) ;; -let mk_inverter name it leftno ?selection outsort status baseuri = +let mk_inverter name is_ind 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)); @@ -113,8 +107,6 @@ let mk_inverter name 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 -> [] @@ -124,19 +116,18 @@ let mk_inverter name 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)))) *) - Some (CicNotationPt.Implicit `JustOne)), - mk_appl (mk_id "P"::id_rs))))) + 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 t = mk_appl ( [mk_id (ind_name ^ "_" ^ suffix)]@ id_ls @ [lambdas] @ - List.map mk_id hyplist @ - HExtlib.mk_list (CicNotationPt.Implicit `JustOne) (List.length ys) @ [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 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 @@ -152,21 +143,33 @@ let mk_inverter name it leftno ?selection outsort status baseuri = 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 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; - (*NTactics.case_tac "cut";*) - NTactics.apply_tac ("",0,t); - NTactics.merge_tac; - NTactics.merge_tac; - NTactics.skip_tac])) status 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] @ + 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 pp (lazy "inv 3"); status,status#obj ;; diff --git a/helm/software/components/ng_tactics/nInversion.mli b/helm/software/components/ng_tactics/nInversion.mli index b5ca8597d..14d33eb1e 100644 --- a/helm/software/components/ng_tactics/nInversion.mli +++ b/helm/software/components/ng_tactics/nInversion.mli @@ -11,6 +11,7 @@ (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *) -val mk_inverter: string -> NCic.inductiveType -> int -> ?selection:bool list -> +val mk_inverter: + string -> bool -> NCic.inductiveType -> int -> ?selection:bool list -> NCic.sort -> (#NTacStatus.tac_status as 's) -> string -> - 's * NCic.obj + 's * NCic.obj -- 2.39.2