X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=397a443dbcf37a4a6970e618b6b95ffd888b9576;hb=8baa4aabe6cc848c6a3ecd7a08e1bab9edc8bee1;hp=904a221ffe396d72f8f72a2951c8a8f4e8a13eb6;hpb=8a660ee06d72cfee52c707bb1d8d8be3bab0d682;p=helm.git diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml index 904a221ff..397a443db 100644 --- a/matita/components/ng_tactics/nInversion.ml +++ b/matita/components/ng_tactics/nInversion.ml @@ -26,10 +26,12 @@ let mk_id id = NotationPt.Ident (id,None) ;; -let rec split_arity ~subst context te = - match NCicReduction.whd ~subst context te with +let mk_sym s = NotationPt.Symbol (s,0);; + +let rec split_arity status ~subst context te = + match NCicReduction.whd status ~subst context te with | NCic.Prod (name,so,ta) -> - split_arity ~subst ((name, (NCic.Decl so))::context) ta + split_arity status ~subst ((name, (NCic.Decl so))::context) ta | t -> context, t ;; @@ -46,13 +48,41 @@ let rec mk_prods l t = | hd::tl -> NotationPt.Binder (`Forall, (mk_id hd, None), mk_prods tl t) ;; -let rec mk_arrows ?(pattern=false) xs ys selection target = +let rec leibpatt = function + | [] -> NotationPt.UserInput + | false::sel -> leibpatt sel + | true::sel -> NotationPt.Binder (`Forall, (mk_id "_", + Some (mk_appl [NotationPt.Implicit `JustOne + ;NotationPt.Implicit `JustOne + ;NotationPt.Implicit `JustOne + ;NotationPt.UserInput])), + leibpatt sel);; +let rec jmeqpatt = function + | [] -> NotationPt.UserInput + | false::sel -> jmeqpatt sel + | true::sel -> NotationPt.Binder (`Forall, (mk_id "_", + Some (mk_appl [NotationPt.Implicit `JustOne + ;NotationPt.Implicit `JustOne + ;NotationPt.Implicit `JustOne + ;NotationPt.UserInput + ;NotationPt.UserInput])), + jmeqpatt sel);; + +let rec mk_arrows ~jmeq xs ys selection target = match selection,xs,ys with [],[],[] -> target - | false :: l,x::xs,y::ys -> mk_arrows ~pattern xs ys l target - | true :: l,x::xs,y::ys -> - NotationPt.Binder (`Forall, (mk_id "_", Some (mk_appl [if pattern then NotationPt.Implicit `JustOne else mk_id "eq" ; NotationPt.Implicit `JustOne;x;y])), - mk_arrows ~pattern xs ys l target) + | false :: l,x::xs,y::ys -> mk_arrows ~jmeq xs ys l target + | true :: l,x::xs,y::ys when jmeq -> + NotationPt.Binder (`Forall, (mk_id "_", + Some (mk_appl [mk_sym "jmsimeq" ; + NotationPt.Implicit `JustOne;x; + NotationPt.Implicit `JustOne;y])), + mk_arrows ~jmeq xs ys l target) + | true :: l,x::xs,y::ys -> + NotationPt.Binder (`Forall, (mk_id "_", + Some (mk_appl [mk_sym "eq" ; + NotationPt.Implicit `JustOne;x;y])), + mk_arrows ~jmeq xs ys l target) | _ -> raise (Invalid_argument "ninverter: the selection doesn't match the arity of the specified inductive type") ;; @@ -60,21 +90,21 @@ let subst_metasenv_and_fix_names status = let u,h,metasenv, subst,o = status#obj in let o = NCicUntrusted.map_obj_kind ~skip_body:true - (NCicUntrusted.apply_subst subst []) o + (NCicUntrusted.apply_subst status subst []) o in - status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv subst metasenv,subst,o) + status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o) ;; -let mk_inverter name is_ind it leftno ?selection outsort status baseuri = +let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.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)); + pp (lazy ("arity: " ^ status#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 status ~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)));(**) - let args,sort= split_arity ~subst:[] [] ty in - pp (lazy ("arity sort: " ^ NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:args sort)); + let args,sort= split_arity status ~subst:[] [] ty in + pp (lazy ("arity sort: " ^ status#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 nparams = List.length args in @@ -105,7 +135,7 @@ let mk_inverter name is_ind it leftno ?selection outsort status baseuri = None -> HExtlib.mk_list true (List.length ys) | Some s -> s in - let prods = mk_arrows id_rs id_ys selection pred in + let prods = mk_arrows ~jmeq id_rs id_ys selection pred in let hyplist = let rec hypaux k = function @@ -136,7 +166,7 @@ let mk_inverter name is_ind it leftno ?selection outsort status baseuri = let cut_theorem = let rs = List.map (fun x -> mk_id x) rs in - mk_arrows rs rs selection (mk_appl (mk_id "P"::rs)) in + mk_arrows ~jmeq rs rs selection (mk_appl (mk_id "P"::rs)) in let cut = mk_appl [NotationPt.Binder (`Lambda, (mk_id "Hcut", Some cut_theorem), @@ -145,11 +175,8 @@ NotationPt.Implicit (`Tagged "end")); 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 (NotationPt.Implicit `JustOne) (List.length ys)) - (HExtlib.mk_list NotationPt.UserInput (List.length ys)) - selection NotationPt.UserInput)) in + Some (if jmeq then jmeqpatt selection + else leibpatt selection)) in let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in let status = NTactics.block_tac @@ -160,7 +187,7 @@ NotationPt.Implicit (`Tagged "end")); NTactics.branch_tac; NTactics.case_tac "end"; NTactics.apply_tac ("",0,mk_id "Hcut"); - NTactics.apply_tac ("",0,mk_id "refl"); + NTactics.apply_tac ("",0,mk_sym "refl"); NTactics.shift_tac; elim_tac ~what:("",0,mk_id "Hterm") ~where; NTactics.branch_tac ~force:true] @ @@ -174,3 +201,8 @@ NotationPt.Implicit (`Tagged "end")); status,status#obj ;; +let mk_inverter name is_ind it leftno ?selection outsort status baseuri = + try mk_inverter ~jmeq:true name is_ind it leftno ?selection outsort status baseuri + with NTacStatus.Error _ -> + mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri +;;