X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=8267fd87774e00398ea654d17ba0a6ff4111c1ae;hb=f7da48c844105a52a705872dfa0d4104de010c82;hp=cf4711db51f25320bcd6664822399e307f0b8662;hpb=894d518aa760c9f816ddb0dc2b3fa88e1fe20a94;p=helm.git diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml index cf4711db5..8267fd877 100644 --- a/matita/components/ng_tactics/nInversion.ml +++ b/matita/components/ng_tactics/nInversion.ml @@ -26,6 +26,8 @@ let mk_id id = NotationPt.Ident (id,None) ;; +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) -> @@ -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") ;; @@ -65,7 +95,7 @@ let subst_metasenv_and_fix_names status = 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: #NCic.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: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty)); @@ -79,8 +109,11 @@ let mk_inverter name is_ind it leftno ?selection outsort (status: #NCic.status) pp (lazy ("lunghezza args = " ^ string_of_int (List.length args)));(**) let nparams = List.length args in + (* the default is a dependent inversion *) + let is_dependent = (selection = None && (jmeq || nparams = 0)) in + pp (lazy ("nparams = " ^ string_of_int nparams)); - if nparams = 0 + if (nparams = 0 && not is_dependent) 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 @@ -88,24 +121,19 @@ let mk_inverter name is_ind it leftno ?selection outsort (status: #NCic.status) 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 + + (* dependent -> add Hterm to rs *) + let rs = if is_dependent then (rs@["Hterm"]) else rs 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 - (* pseudocode let t = Lambda y1 ... yr. xs_ = ys_ -> pred *) - (* check: assuming we have more than one right parameter *) - (* pred := P yr- *) - let pred = mk_appl ((mk_id "P")::id_ys) in - - let selection = match selection with - None -> HExtlib.mk_list true (List.length ys) + let selection = + match selection with + None -> HExtlib.mk_list true (List.length rs) | Some s -> s in - let prods = mk_arrows id_rs id_ys selection pred in let hyplist = let rec hypaux k = function @@ -113,20 +141,20 @@ let mk_inverter name is_ind it leftno ?selection outsort (status: #NCic.status) | n -> ("H" ^ string_of_int k) :: hypaux (k+1) (n-1) in (hypaux 1 ncons) in - pp (lazy ("lunghezza ys = " ^ string_of_int (List.length ys))); let outsort, suffix = NCicElim.ast_of_sort outsort in let theorem = mk_prods xs - (NotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length ys)) (NotationPt.Sort outsort))), - mk_prods hyplist (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), mk_appl (mk_id "P"::id_rs))))) + (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))), + (NotationPt.Binder (`Forall, (mk_id "P", Some (mk_prods (HExtlib.mk_list "_" (List.length rs)) (NotationPt.Sort outsort))), + mk_prods hyplist (mk_appl (mk_id "P"::id_rs)))))) in let status, theorem = - GrafiteDisambiguate.disambiguate_nobj status ~baseuri + let attrs = `Generated, `Theorem, `InversionPrinciple in + GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def",0, NotationPt.Theorem - (`Theorem,name,theorem, - Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple)) + (name,theorem, Some (NotationPt.Implicit (`Tagged "inv")), attrs)) in let uri,height,nmenv,nsubst,nobj = theorem in let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in @@ -136,21 +164,22 @@ let mk_inverter name is_ind it leftno ?selection outsort (status: #NCic.status) 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), NotationPt.Implicit (`Tagged "end")); NotationPt.Implicit (`Tagged "cut")] in - let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in + let intros = List.map (fun x -> pp (lazy x); NTactics.intro_tac x) (xs@["Hterm";"P"]@hyplist) 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 - let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac 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 elim_tac ~what ~where s = + try NTactics.elim_tac ~what ~where s + with NTacStatus.Error _ -> NTactics.cases_tac ~what ~where s + in let status = NTactics.block_tac (NTactics.branch_tac :: @@ -160,7 +189,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 +203,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 (s,_) -> + mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri +;;