From: Wilmer Ricciotti Date: Mon, 14 Nov 2011 15:09:07 +0000 (+0000) Subject: Added dependent inversion (default case for jmeq) X-Git-Tag: make_still_working~2119 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=085cf66f8385f8cbc269c38ca7c7572d09e4810e;p=helm.git Added dependent inversion (default case for jmeq) --- diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml index 397a443db..dbbf0da0f 100644 --- a/matita/components/ng_tactics/nInversion.ml +++ b/matita/components/ng_tactics/nInversion.ml @@ -109,6 +109,10 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st 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 in*) + let is_dependent = true in + pp (lazy ("nparams = " ^ string_of_int nparams)); if nparams = 0 then raise (Failure "inverter: the type must have at least one right parameter") @@ -118,24 +122,19 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st 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 ~jmeq id_rs id_ys selection pred in let hyplist = let rec hypaux k = function @@ -143,13 +142,13 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st | 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 @@ -172,7 +171,7 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st 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 (if jmeq then jmeqpatt selection @@ -203,6 +202,6 @@ NotationPt.Implicit (`Tagged "end")); 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 _ -> + with NTacStatus.Error (s,_) -> mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri ;; diff --git a/matita/components/ng_tactics/nTactics.ml b/matita/components/ng_tactics/nTactics.ml index 104a044f6..044f496f1 100644 --- a/matita/components/ng_tactics/nTactics.ml +++ b/matita/components/ng_tactics/nTactics.ml @@ -705,7 +705,7 @@ let inversion_tac ~what:(txt,len,what) ~where = in let eliminator = let _,_,w = what in - Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ] + Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ; Ast.Implicit `Vector] in exact_tac ("",0,eliminator) status) ]) ;;