From 870b9b017da98021d9163bf45efe9c27b40bb33d Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Tue, 2 Feb 2010 13:39:54 +0000 Subject: [PATCH] Fixed a bug with indexed inductive types which sometimes prevented the inversion principles from being defined. --- .../components/ng_tactics/nInversion.ml | 22 +++++++++++-------- 1 file changed, 13 insertions(+), 9 deletions(-) diff --git a/helm/software/components/ng_tactics/nInversion.ml b/helm/software/components/ng_tactics/nInversion.ml index 8df07952f..89a1dd1af 100644 --- a/helm/software/components/ng_tactics/nInversion.ml +++ b/helm/software/components/ng_tactics/nInversion.ml @@ -76,24 +76,25 @@ let mk_inverter name it leftno ?selection outsort status baseuri = 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_ls = List.map mk_id ls in @@ -128,10 +129,12 @@ let mk_inverter name it leftno ?selection outsort status baseuri = 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))))) - in + in + pp (lazy ("and the theorem is: \n" ^ (CicNotationPp.pp_term theorem))); 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 + pp (lazy ("and t is: \n" ^ (CicNotationPp.pp_term t))); let status, theorem = GrafiteDisambiguate.disambiguate_nobj status ~baseuri (baseuri ^ name ^ ".def", 0,CicNotationPt.Theorem (`Theorem,name,theorem,Some @@ -147,7 +150,8 @@ 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 -> pp (lazy x); NTactics.intro_tac x) (xs@["P"]@hyplist@["Hterm"]) in let status = NTactics.block_tac -- 2.39.2