X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=5be36d001756081487505f3d106da63b453d68fe;hb=17e81891da2a278891276e923d479e3834e22c07;hp=1ee47c74e97998dbfd552416ad7b12aec0589411;hpb=59d3cc13e07d1de296874544eed8dcb0f08c40c5;p=helm.git diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index 1ee47c74e..5be36d001 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -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,31 +65,32 @@ 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)); 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 <= leftno + if nparams = 0 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 (nparams+1)) in + let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+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) (nparams+1)) in + let ys = List.map (fun n -> "y" ^ (string_of_int n)) (HExtlib.list_seq (leftno+1) (leftno+nparams+1)) in - let id_xs = List.map mk_id xs in + let _id_xs = List.map mk_id xs in let id_ls = List.map mk_id ls in let id_rs = List.map mk_id rs in let id_ys = List.map mk_id ys in @@ -112,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 -> [] @@ -123,20 +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 status, theorem = + GrafiteDisambiguate.disambiguate_nobj status ~baseuri + (baseuri ^ name ^ ".def",0, + CicNotationPt.Theorem + (`Theorem,name,theorem, + Some (CicNotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) 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 @@ -148,26 +139,38 @@ let mk_inverter name 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 -> 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_eq"); - NTactics.shift_tac; - NTactics.case_tac "cut"; - NTactics.apply_tac ("",0,t) - (* ; - NTactics.merge_tac; - NTactics.merge_tac; - NTactics.skip_tac*)])) status 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] @ + 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 ;;