summaryrefslogtreecommitdiff
path: root/toplevel/auto_ind_decl.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
-rw-r--r--toplevel/auto_ind_decl.ml714
1 files changed, 392 insertions, 322 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 82709db4..0e66c43c 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -6,7 +6,10 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: auto_ind_decl.ml 11671 2008-12-12 12:43:03Z herbelin $ i*)
+(*i $Id$ i*)
+
+(* This file is about the automatic generation of schemes about
+ decidable equality, created by Vincent Siles, Oct 2007 *)
open Tacmach
open Util
@@ -28,9 +31,10 @@ open Tactics
open Tacticals
open Ind_tables
-(* boolean equality *)
+(**********************************************************************)
+(* Generic synthesis of boolean equality *)
-let quick_chop n l =
+let quick_chop n l =
let rec kick_last = function
| t::[] -> []
| t::q -> t::(kick_last q)
@@ -39,21 +43,21 @@ and aux = function
| (0,l') -> l'
| (n,h::t) -> aux (n-1,t)
| _ -> failwith "quick_chop"
- in
+ in
if n > (List.length l) then failwith "quick_chop args"
else kick_last (aux (n,l) )
-let rec deconstruct_type t =
+let rec deconstruct_type t =
let l,r = decompose_prod t in
(List.map (fun (_,b) -> b) (List.rev l))@[r]
-let subst_in_constr (_,subst,(ind,const)) =
- let ind' = (subst_kn subst (fst ind)),(snd ind)
- and const' = subst_mps subst const in
- ind',const'
-
-exception EqNotFound of string
+exception EqNotFound of inductive * inductive
exception EqUnknown of string
+exception UndefinedCst of string
+exception InductiveWithProduct
+exception InductiveWithSort
+exception ParameterWithoutEquality of constant
+exception NonSingletonProp of inductive
let dl = dummy_loc
@@ -62,70 +66,77 @@ let bb = constr_of_global Coqlib.glob_bool
let andb_prop = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb_prop
-let andb_true_intro = fun _ ->
- (Coqlib.build_bool_type()).Coqlib.andb_true_intro
+let andb_true_intro = fun _ ->
+ (Coqlib.build_bool_type()).Coqlib.andb_true_intro
-let tt = constr_of_global Coqlib.glob_true
+let tt = constr_of_global Coqlib.glob_true
let ff = constr_of_global Coqlib.glob_false
-let eq = constr_of_global Coqlib.glob_eq
+let eq = constr_of_global Coqlib.glob_eq
-let sumbool = Coqlib.build_coq_sumbool
+let sumbool = Coqlib.build_coq_sumbool
-let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
+let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
(* reconstruct the inductive with the correct deBruijn indexes *)
-let mkFullInd ind n =
+let mkFullInd ind n =
let mib = Global.lookup_mind (fst ind) in
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
(* params context divided *)
- let lnonparrec,lnamesparrec =
+ let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- if nparrec > 0
+ if nparrec > 0
then mkApp (mkInd ind,
Array.of_list(extended_rel_list (nparrec+n) lnamesparrec))
else mkInd ind
-let make_eq_scheme sp =
+let check_bool_is_defined () =
+ try let _ = Global.type_of_global Coqlib.glob_bool in ()
+ with _ -> raise (UndefinedCst "bool")
+
+let beq_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
+
+let build_beq_scheme kn =
+ check_bool_is_defined ();
(* fetching global env *)
let env = Global.env() in
(* fetching the mutual inductive body *)
- let mib = Global.lookup_mind sp in
+ let mib = Global.lookup_mind kn in
(* number of inductives in the mutual *)
let nb_ind = Array.length mib.mind_packets in
(* number of params in the type *)
let nparams = mib.mind_nparams in
let nparrec = mib.mind_nparams_rec in
(* params context divided *)
- let lnonparrec,lnamesparrec =
+ let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
(* predef coq's boolean type *)
(* rec name *)
let rec_name i =(string_of_id (Array.get mib.mind_packets i).mind_typename)^
- "_eqrec"
+ "_eqrec"
in
(* construct the "fun A B ... N, eqA eqB eqC ... N => fixpoint" part *)
let create_input c =
- let myArrow u v = mkArrow u (lift 1 v)
+ let myArrow u v = mkArrow u (lift 1 v)
and eqName = function
| Name s -> id_of_string ("eq_"^(string_of_id s))
- | Anonymous -> id_of_string "eq_A"
+ | Anonymous -> id_of_string "eq_A"
in
let ext_rel_list = extended_rel_list 0 lnamesparrec in
let lift_cnt = ref 0 in
- let eqs_typ = List.map (fun aa ->
- let a = lift !lift_cnt aa in
- incr lift_cnt;
- myArrow a (myArrow a bb)
+ let eqs_typ = List.map (fun aa ->
+ let a = lift !lift_cnt aa in
+ incr lift_cnt;
+ myArrow a (myArrow a bb)
) ext_rel_list in
let eq_input = List.fold_left2
( fun a b (n,_,_) -> (* mkLambda(n,b,a) ) *)
(* here I leave the Naming thingy so that the type of
the function is more readable for the user *)
- mkNamedLambda (eqName n) b a )
+ mkNamedLambda (eqName n) b a )
c (List.rev eqs_typ) lnamesparrec
in
List.fold_left (fun a (n,_,t) ->(* mkLambda(n,t,a)) eq_input rel_list *)
@@ -134,181 +145,170 @@ let make_eq_scheme sp =
(match n with Name s -> s | Anonymous -> id_of_string "A")
t a) eq_input lnamesparrec
in
- let make_one_eq cur =
- let ind = sp,cur in
+ let make_one_eq cur =
+ let ind = kn,cur in
(* current inductive we are working on *)
- let cur_packet = mib.mind_packets.(snd ind) in
+ let cur_packet = mib.mind_packets.(snd ind) in
(* Inductive toto : [rettyp] := *)
let rettyp = Inductive.type_of_inductive env (mib,cur_packet) in
- (* split rettyp in a list without the non rec params and the last ->
+ (* split rettyp in a list without the non rec params and the last ->
e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *)
let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in
(* give a type A, this function tries to find the equality on A declared
previously *)
(* nlist = the number of args (A , B , ... )
eqA = the deBruijn index of the first eq param
- ndx = how much to translate due to the 2nd Case
+ ndx = how much to translate due to the 2nd Case
*)
- let compute_A_equality rel_list nlist eqA ndx t =
+ let compute_A_equality rel_list nlist eqA ndx t =
let lifti = ndx in
- let rec aux c a = match c with
+ let rec aux c =
+ let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
+ match kind_of_term c with
| Rel x -> mkRel (x-nlist+ndx)
- | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x)))
- | Cast (x,_,_) -> aux (kind_of_term x) a
- | App (x,newa) -> aux (kind_of_term x) newa
- | Ind (sp',i) -> if sp=sp' then mkRel(eqA-nlist-i+nb_ind-1)
- else ( try
- let eq = find_eq_scheme (sp',i)
- and eqa = Array.map
- (fun x -> aux (kind_of_term x) [||] ) a
- in
- let args = Array.append
- (Array.map (fun x->lift lifti x) a) eqa
- in if args = [||] then eq
- else mkApp (eq,Array.append
+ | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x)))
+ | Cast (x,_,_) -> aux (applist (x,a))
+ | App _ -> assert false
+ | Ind (kn',i as ind') -> if eq_mind kn kn' then mkRel(eqA-nlist-i+nb_ind-1)
+ else ( try
+ let a = Array.of_list a in
+ let eq = mkConst (find_scheme (!beq_scheme_kind_aux()) (kn',i))
+ and eqa = Array.map aux a
+ in
+ let args = Array.append
+ (Array.map (fun x->lift lifti x) a) eqa
+ in if args = [||] then eq
+ else mkApp (eq,Array.append
(Array.map (fun x->lift lifti x) a) eqa)
- with Not_found -> raise(EqNotFound (string_of_kn sp'))
+ with Not_found -> raise(EqNotFound (ind',ind))
)
- | Sort _ -> raise (EqUnknown "Sort" )
- | Prod _ -> raise (EqUnknown "Prod" )
- | Lambda _-> raise (EqUnknown "Lambda")
+ | Sort _ -> raise InductiveWithSort
+ | Prod _ -> raise InductiveWithProduct
+ | Lambda _-> raise (EqUnknown "Lambda")
| LetIn _ -> raise (EqUnknown "LetIn")
- | Const kn -> let mp,dir,lbl= repr_con kn in
- mkConst (make_con mp dir (
- mk_label ("eq_"^(string_of_label lbl))))
+ | Const kn ->
+ (match Environ.constant_opt_value env kn with
+ | None -> raise (ParameterWithoutEquality kn)
+ | Some c -> aux (applist (c,a)))
| Construct _ -> raise (EqUnknown "Construct")
| Case _ -> raise (EqUnknown "Case")
| CoFix _ -> raise (EqUnknown "CoFix")
- | Fix _ -> raise (EqUnknown "Fix")
- | Meta _ -> raise (EqUnknown "Meta")
+ | Fix _ -> raise (EqUnknown "Fix")
+ | Meta _ -> raise (EqUnknown "Meta")
| Evar _ -> raise (EqUnknown "Evar")
in
- aux t [||]
+ aux t
in
(* construct the predicate for the Case part*)
- let do_predicate rel_list n =
- List.fold_left (fun a b -> mkLambda(Anonymous,b,a))
+ let do_predicate rel_list n =
+ List.fold_left (fun a b -> mkLambda(Anonymous,b,a))
(mkLambda (Anonymous,
mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1),
- bb))
- (List.rev rettyp_l) in
+ bb))
+ (List.rev rettyp_l) in
(* make_one_eq *)
- (* do the [| C1 ... => match Y with ... end
- ...
+ (* do the [| C1 ... => match Y with ... end
+ ...
Cn => match Y with ... end |] part *)
let ci = make_case_info env ind MatchStyle in
let constrs n = get_constructors env (make_ind_family (ind,
extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
- let ar = Array.create n ff in
+ let ar = Array.create n ff in
for i=0 to n-1 do
let nb_cstr_args = List.length constrsi.(i).cs_args in
let ar2 = Array.create n ff in
let constrsj = constrs (3+nparrec+nb_cstr_args) in
for j=0 to n-1 do
- if (i=j) then
+ if (i=j) then
ar2.(j) <- let cc = (match nb_cstr_args with
| 0 -> tt
- | _ -> let eqs = Array.make nb_cstr_args tt in
+ | _ -> let eqs = Array.make nb_cstr_args tt in
for ndx = 0 to nb_cstr_args-1 do
let _,_,cc = List.nth constrsi.(i).cs_args ndx in
let eqA = compute_A_equality rel_list
nparrec
(nparrec+3+2*nb_cstr_args)
(nb_cstr_args+ndx+1)
- (kind_of_term cc)
- in
- Array.set eqs ndx
+ cc
+ in
+ Array.set eqs ndx
(mkApp (eqA,
[|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|]
))
- done;
- Array.fold_left
- (fun a b -> mkApp (andb(),[|b;a|]))
- (eqs.(0))
+ done;
+ Array.fold_left
+ (fun a b -> mkApp (andb(),[|b;a|]))
+ (eqs.(0))
(Array.sub eqs 1 (nb_cstr_args - 1))
)
in
(List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) cc
- (constrsj.(j).cs_args)
- )
+ (constrsj.(j).cs_args)
+ )
else ar2.(j) <- (List.fold_left (fun a (p,q,r) ->
mkLambda (p,r,a)) ff (constrsj.(j).cs_args) )
done;
- ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a))
+ ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a))
(mkCase (ci,do_predicate rel_list nb_cstr_args,
mkVar (id_of_string "Y") ,ar2))
- (constrsi.(i).cs_args))
+ (constrsi.(i).cs_args))
done;
mkNamedLambda (id_of_string "X") (mkFullInd ind (nb_ind-1+1)) (
mkNamedLambda (id_of_string "Y") (mkFullInd ind (nb_ind-1+2)) (
- mkCase (ci, do_predicate rel_list 0,mkVar (id_of_string "X"),ar)))
- in (* make_eq_scheme *)
- try
- let names = Array.make nb_ind Anonymous and
- types = Array.make nb_ind mkSet and
- cores = Array.make nb_ind mkSet and
- res = Array.make nb_ind mkSet in
+ mkCase (ci, do_predicate rel_list 0,mkVar (id_of_string "X"),ar)))
+ in (* build_beq_scheme *)
+ let names = Array.make nb_ind Anonymous and
+ types = Array.make nb_ind mkSet and
+ cores = Array.make nb_ind mkSet in
for i=0 to (nb_ind-1) do
names.(i) <- Name (id_of_string (rec_name i));
- types.(i) <- mkArrow (mkFullInd (sp,i) 0)
- (mkArrow (mkFullInd (sp,i) 1) bb);
+ types.(i) <- mkArrow (mkFullInd (kn,i) 0)
+ (mkArrow (mkFullInd (kn,i) 1) bb);
cores.(i) <- make_one_eq i
- done;
- if (string_of_mp (modpath sp ))="Coq.Init.Logic"
- then print_string "Logic time, do nothing.\n"
- else (
- for i=0 to (nb_ind-1) do
- let cpack = Array.get mib.mind_packets i in
- if check_eq_scheme (sp,i)
- then message ("Boolean equality is already defined on "^
- (string_of_id cpack.mind_typename)^".")
- else (
+ done;
+ Array.init nb_ind (fun i ->
+ let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in
+ if not (List.mem InSet kelim) then
+ raise (NonSingletonProp (kn,i));
let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in
- res.(i) <- create_input fix
- )
- done;
- );
- res
- with
- | EqUnknown s -> error ("Type unexpected ("^s^
- ") during boolean eq computation, please report.")
- | EqNotFound s -> error ("Boolean equality on "^s^
- " is missing, equality will not be defined.")
- | _ -> error ("Unknown exception during boolean equality creation,"^
- " the equality will not be defined.")
+ create_input fix)
+
+let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
+
+let _ = beq_scheme_kind_aux := fun () -> beq_scheme_kind
(* This function tryies to get the [inductive] between a constr
the constr should be Ind i or App(Ind i,[|args|])
*)
-let destruct_ind c =
+let destruct_ind c =
try let u,v = destApp c in
let indc = destInd u in
indc,v
with _-> let indc = destInd c in
indc,[||]
-(*
- In the followind, avoid is the list of names to avoid.
+(*
+ In the following, avoid is the list of names to avoid.
If the args of the Inductive type are A1 ... An
- then avoid should be
+ then avoid should be
[| lb_An ... lb _A1 (resp. bl_An ... bl_A1)
eq_An .... eq_A1 An ... A1 |]
so from Ai we can find the the correct eq_Ai bl_ai or lb_ai
*)
(* used in the leib -> bool side*)
-let do_replace_lb aavoid narg gls p q =
+let do_replace_lb lb_scheme_key aavoid narg gls p q =
let avoid = Array.of_list aavoid in
- let do_arg v offset =
- try
+ let do_arg v offset =
+ try
let x = narg*offset in
- let s = destVar v in
+ let s = destVar v in
let n = Array.length avoid in
- let rec find i =
- if avoid.(n-i) = s then avoid.(n-i-x)
- else (if i<n then find (i+1)
+ let rec find i =
+ if avoid.(n-i) = s then avoid.(n-i-x)
+ else (if i<n then find (i+1)
else error ("Var "^(string_of_id s)^" seems unknown.")
)
in mkVar (find 1)
@@ -317,47 +317,46 @@ let do_replace_lb aavoid narg gls p q =
(
let mp,dir,lbl = repr_con (destConst v) in
mkConst (make_con mp dir (mk_label (
- if offset=1 then ("eq_"^(string_of_label lbl))
+ if offset=1 then ("eq_"^(string_of_label lbl))
else ((string_of_label lbl)^"_lb")
)))
)
in
let type_of_pq = pf_type_of gls p in
let u,v = destruct_ind type_of_pq
- in let lb_type_of_p =
- try find_lb_proof u
- with Not_found ->
+ in let lb_type_of_p =
+ try mkConst (find_scheme lb_scheme_key u)
+ with Not_found ->
(* spiwack: the format of this error message should probably
be improved. *)
- let err_msg = msg_with Format.str_formatter
+ let err_msg = msg_with Format.str_formatter
(str "Leibniz->boolean:" ++
- str "You have to declare the" ++
+ str "You have to declare the" ++
str "decidability over " ++
- Printer.pr_constr type_of_pq ++
+ Printer.pr_constr type_of_pq ++
str " first.");
Format.flush_str_formatter ()
in
error err_msg
- in let lb_args = Array.append (Array.append
+ in let lb_args = Array.append (Array.append
(Array.map (fun x -> x) v)
(Array.map (fun x -> do_arg x 1) v))
(Array.map (fun x -> do_arg x 2) v)
- in let app = if lb_args = [||]
- then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
+ in let app = if lb_args = [||]
+ then lb_type_of_p else mkApp (lb_type_of_p,lb_args)
in [Equality.replace p q ; apply app ; Auto.default_auto]
-
(* used in the bool -> leib side *)
-let do_replace_bl ind gls aavoid narg lft rgt =
- let avoid = Array.of_list aavoid in
- let do_arg v offset =
- try
+let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
+ let avoid = Array.of_list aavoid in
+ let do_arg v offset =
+ try
let x = narg*offset in
- let s = destVar v in
+ let s = destVar v in
let n = Array.length avoid in
- let rec find i =
- if avoid.(n-i) = s then avoid.(n-i-x)
- else (if i<n then find (i+1)
+ let rec find i =
+ if avoid.(n-i) = s then avoid.(n-i-x)
+ else (if i<n then find (i+1)
else error ("Var "^(string_of_id s)^" seems unknown.")
)
in mkVar (find 1)
@@ -366,60 +365,60 @@ let do_replace_bl ind gls aavoid narg lft rgt =
(
let mp,dir,lbl = repr_con (destConst v) in
mkConst (make_con mp dir (mk_label (
- if offset=1 then ("eq_"^(string_of_label lbl))
+ if offset=1 then ("eq_"^(string_of_label lbl))
else ((string_of_label lbl)^"_bl")
)))
)
in
- let rec aux l1 l2 =
+ let rec aux l1 l2 =
match (l1,l2) with
| (t1::q1,t2::q2) -> let tt1 = pf_type_of gls t1 in
if t1=t2 then aux q1 q2
else (
- let u,v = try destruct_ind tt1
+ let u,v = try destruct_ind tt1
(* trick so that the good sequence is returned*)
with _ -> ind,[||]
- in if u = ind
+ in if u = ind
then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2)
else (
- let bl_t1 =
- try find_bl_proof u
- with Not_found ->
+ let bl_t1 =
+ try mkConst (find_scheme bl_scheme_key u)
+ with Not_found ->
(* spiwack: the format of this error message should probably
be improved. *)
- let err_msg = msg_with Format.str_formatter
+ let err_msg = msg_with Format.str_formatter
(str "boolean->Leibniz:" ++
- str "You have to declare the" ++
+ str "You have to declare the" ++
str "decidability over " ++
- Printer.pr_constr tt1 ++
+ Printer.pr_constr tt1 ++
str " first.");
Format.flush_str_formatter ()
in
error err_msg
- in let bl_args =
- Array.append (Array.append
+ in let bl_args =
+ Array.append (Array.append
(Array.map (fun x -> x) v)
(Array.map (fun x -> do_arg x 1) v))
(Array.map (fun x -> do_arg x 2) v )
- in
- let app = if bl_args = [||]
- then bl_t1 else mkApp (bl_t1,bl_args)
- in
- (Equality.replace_by t1 t2
+ in
+ let app = if bl_args = [||]
+ then bl_t1 else mkApp (bl_t1,bl_args)
+ in
+ (Equality.replace_by t1 t2
(tclTHEN (apply app) (Auto.default_auto)))::(aux q1 q2)
)
)
| ([],[]) -> []
| _ -> error "Both side of the equality must have the same arity."
in
- let (ind1,ca1) = try destApp lft with
+ let (ind1,ca1) = try destApp lft with
_ -> error "replace failed."
and (ind2,ca2) = try destApp rgt with
_ -> error "replace failed."
in
let (sp1,i1) = try destInd ind1 with
- _ -> (try fst (destConstruct ind1) with _ ->
+ _ -> (try fst (destConstruct ind1) with _ ->
error "The expected type is an inductive one.")
and (sp2,i2) = try destInd ind2 with
_ -> (try fst (destConstruct ind2) with _ ->
@@ -427,14 +426,14 @@ let do_replace_bl ind gls aavoid narg lft rgt =
in
if (sp1 <> sp2) || (i1 <> i2)
then (error "Eq should be on the same type")
- else (aux (Array.to_list ca1) (Array.to_list ca2))
+ else (aux (Array.to_list ca1) (Array.to_list ca2))
-(*
+(*
create, from a list of ids [i1,i2,...,in] the list
[(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al )]
*)
-let list_id l = List.fold_left ( fun a (n,_,t) -> let s' =
- match n with
+let list_id l = List.fold_left ( fun a (n,_,t) -> let s' =
+ match n with
Name s -> string_of_id s
| Anonymous -> "A" in
(id_of_string s',id_of_string ("eq_"^s'),
@@ -445,72 +444,73 @@ let list_id l = List.fold_left ( fun a (n,_,t) -> let s' =
(*
build the right eq_I A B.. N eq_A .. eq_N
*)
-let eqI ind l =
+let eqI ind l =
let list_id = list_id l in
let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@
(List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
- and e = try find_eq_scheme ind with
- Not_found -> error
- ("The boolean equality on "^(string_of_kn (fst ind))^" is needed.");
+ and e = try mkConst (find_scheme beq_scheme_kind ind) with
+ Not_found -> error
+ ("The boolean equality on "^(string_of_mind (fst ind))^" is needed.");
in (if eA = [||] then e else mkApp(e,eA))
-let compute_bl_goal ind lnamesparrec nparrec =
+(**********************************************************************)
+(* Boolean->Leibniz *)
+
+let compute_bl_goal ind lnamesparrec nparrec =
let eqI = eqI ind lnamesparrec in
- let list_id = list_id lnamesparrec in
+ let list_id = list_id lnamesparrec in
let create_input c =
let x = id_of_string "x" and
y = id_of_string "y" in
let bl_typ = List.map (fun (s,seq,_,_) ->
mkNamedProd x (mkVar s) (
mkNamedProd y (mkVar s) (
- mkArrow
+ mkArrow
( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
))
- ) list_id in
+ ) list_id in
let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
mkNamedProd sbl b a
- ) c (List.rev list_id) (List.rev bl_typ) in
+ ) c (List.rev list_id) (List.rev bl_typ) in
let eqs_typ = List.map (fun (s,_,_,_) ->
mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb))
) list_id in
let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
mkNamedProd seq b a
- ) bl_input (List.rev list_id) (List.rev eqs_typ) in
+ ) bl_input (List.rev list_id) (List.rev eqs_typ) in
List.fold_left (fun a (n,_,t) -> mkNamedProd
(match n with Name s -> s | Anonymous -> id_of_string "A")
t a) eq_input lnamesparrec
- in
- let n = id_of_string "n" and
- m = id_of_string "m" in
+ in
+ let n = id_of_string "x" and
+ m = id_of_string "y" in
create_input (
mkNamedProd n (mkFullInd ind nparrec) (
mkNamedProd m (mkFullInd ind (nparrec+1)) (
- mkArrow
+ mkArrow
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
(mkApp(eq,[|mkFullInd ind (nparrec+3);mkVar n;mkVar m|]))
)))
-
-let compute_bl_tact ind lnamesparrec nparrec =
+
+let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig =
let list_id = list_id lnamesparrec in
let avoid = ref [] in
- let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in
- let first_intros =
+ let first_intros =
( List.map (fun (s,_,_,_) -> s ) list_id ) @
( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @
- ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
- in
+ ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
+ in
let fresh_first_intros = List.map ( fun s ->
let fresh = fresh_id (!avoid) s gsig in
avoid := fresh::(!avoid); fresh ) first_intros in
- let freshn = fresh_id (!avoid) (id_of_string "n") gsig in
+ let freshn = fresh_id (!avoid) (id_of_string "x") gsig in
let freshm = avoid := freshn::(!avoid);
- fresh_id (!avoid) (id_of_string "m") gsig in
+ fresh_id (!avoid) (id_of_string "y") gsig in
let freshz = avoid := freshm::(!avoid);
fresh_id (!avoid) (id_of_string "Z") gsig in
(* try with *)
avoid := freshz::(!avoid);
- Pfedit.by (
tclTHENSEQ [ intros_using fresh_first_intros;
intro_using freshn ;
new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn),
@@ -526,21 +526,20 @@ let compute_bl_tact ind lnamesparrec nparrec =
None;
intro_using freshz;
intros;
- tclTRY (
+ tclTRY (
tclORELSE reflexivity (Equality.discr_tac false None)
);
- simpl_in_hyp
- ((Rawterm.all_occurrences_expr,freshz),InHyp);
+ simpl_in_hyp (freshz,InHyp);
(*
repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
*)
tclREPEAT (
tclTHENSEQ [
- apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None;
+ simple_apply_in freshz (andb_prop());
fun gl ->
- let fresht = fresh_id (!avoid) (id_of_string "Z") gsig
+ let fresht = fresh_id (!avoid) (id_of_string "Z") gsig
in
- avoid := fresht::(!avoid);
+ avoid := fresht::(!avoid);
(new_destruct false [Tacexpr.ElimOnConstr
((mkVar freshz,Rawterm.NoBindings))]
None
@@ -549,30 +548,53 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
dl,Genarg.IntroIdentifier freshz]])) None) gl
]);
(*
- Ci a1 ... an = Ci b1 ... bn
+ Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
fun gls-> let gl = (gls.Evd.it).Evd.evar_concl in
match (kind_of_term gl) with
- | App (c,ca) -> (
+ | App (c,ca) -> (
match (kind_of_term c) with
- | Ind (i1,i2) ->
- if(string_of_label (label i1) = "eq")
+ | Ind indeq ->
+ if IndRef indeq = Coqlib.glob_eq
then (
- tclTHENSEQ ((do_replace_bl ind gls (!avoid)
+ tclTHENSEQ ((do_replace_bl bl_scheme_key ind gls
+ (!avoid)
nparrec (ca.(2))
(ca.(1)))@[Auto.default_auto]) gls
)
- else
+ else
(error "Failure while solving Boolean->Leibniz.")
| _ -> error "Failure while solving Boolean->Leibniz."
)
| _ -> error "Failure while solving Boolean->Leibniz."
-
- ]
- )
-let compute_lb_goal ind lnamesparrec nparrec =
+ ] gsig
+
+let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
+
+let make_bl_scheme mind =
+ let mib = Global.lookup_mind mind in
+ if Array.length mib.mind_packets <> 1 then
+ errorlabstrm ""
+ (str "Automatic building of boolean->Leibniz lemmas not supported");
+ let ind = (mind,0) in
+ let nparams = mib.mind_nparams in
+ let nparrec = mib.mind_nparams_rec in
+ let lnonparrec,lnamesparrec =
+ context_chop (nparams-nparrec) mib.mind_params_ctxt in
+ [|Pfedit.build_by_tactic
+ (compute_bl_goal ind lnamesparrec nparrec)
+ (compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|]
+
+let bl_scheme_kind = declare_mutual_scheme_object "_dec_bl" make_bl_scheme
+
+let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
+
+(**********************************************************************)
+(* Leibniz->Boolean *)
+
+let compute_lb_goal ind lnamesparrec nparrec =
let list_id = list_id lnamesparrec in
let eqI = eqI ind lnamesparrec in
let create_input c =
@@ -581,70 +603,68 @@ let compute_lb_goal ind lnamesparrec nparrec =
let lb_typ = List.map (fun (s,seq,_,_) ->
mkNamedProd x (mkVar s) (
mkNamedProd y (mkVar s) (
- mkArrow
+ mkArrow
( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
))
- ) list_id in
+ ) list_id in
let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b ->
mkNamedProd slb b a
- ) c (List.rev list_id) (List.rev lb_typ) in
+ ) c (List.rev list_id) (List.rev lb_typ) in
let eqs_typ = List.map (fun (s,_,_,_) ->
mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb))
) list_id in
let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
mkNamedProd seq b a
- ) lb_input (List.rev list_id) (List.rev eqs_typ) in
+ ) lb_input (List.rev list_id) (List.rev eqs_typ) in
List.fold_left (fun a (n,_,t) -> mkNamedProd
(match n with Name s -> s | Anonymous -> id_of_string "A")
t a) eq_input lnamesparrec
- in
- let n = id_of_string "n" and
- m = id_of_string "m" in
+ in
+ let n = id_of_string "x" and
+ m = id_of_string "y" in
create_input (
mkNamedProd n (mkFullInd ind nparrec) (
mkNamedProd m (mkFullInd ind (nparrec+1)) (
- mkArrow
+ mkArrow
(mkApp(eq,[|mkFullInd ind (nparrec+2);mkVar n;mkVar m|]))
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
)))
-let compute_lb_tact ind lnamesparrec nparrec =
+let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
let list_id = list_id lnamesparrec in
let avoid = ref [] in
- let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in
- let first_intros =
+ let first_intros =
( List.map (fun (s,_,_,_) -> s ) list_id ) @
( List.map (fun (_,seq,_,_) -> seq) list_id ) @
- ( List.map (fun (_,_,_,slb) -> slb) list_id )
- in
+ ( List.map (fun (_,_,_,slb) -> slb) list_id )
+ in
let fresh_first_intros = List.map ( fun s ->
let fresh = fresh_id (!avoid) s gsig in
avoid := fresh::(!avoid); fresh ) first_intros in
- let freshn = fresh_id (!avoid) (id_of_string "n") gsig in
+ let freshn = fresh_id (!avoid) (id_of_string "x") gsig in
let freshm = avoid := freshn::(!avoid);
- fresh_id (!avoid) (id_of_string "m") gsig in
+ fresh_id (!avoid) (id_of_string "y") gsig in
let freshz = avoid := freshm::(!avoid);
fresh_id (!avoid) (id_of_string "Z") gsig in
(* try with *)
avoid := freshz::(!avoid);
- Pfedit.by (
tclTHENSEQ [ intros_using fresh_first_intros;
intro_using freshn ;
- new_induct false [Tacexpr.ElimOnConstr
- ((mkVar freshn),Rawterm.NoBindings)]
+ new_induct false [Tacexpr.ElimOnConstr
+ ((mkVar freshn),Rawterm.NoBindings)]
None
(None,None)
None;
intro_using freshm;
- new_destruct false [Tacexpr.ElimOnConstr
+ new_destruct false [Tacexpr.ElimOnConstr
((mkVar freshm),Rawterm.NoBindings)]
None
(None,None)
None;
intro_using freshz;
intros;
- tclTRY (
+ tclTRY (
tclORELSE reflexivity (Equality.discr_tac false None)
);
Equality.inj [] false (mkVar freshz,Rawterm.NoBindings);
@@ -658,21 +678,48 @@ let compute_lb_tact ind lnamesparrec nparrec =
(* assume the goal to be eq (eq_type ...) = true *)
match (kind_of_term gl) with
| App(c,ca) -> (match (kind_of_term ca.(1)) with
- | App(c',ca') ->
+ | App(c',ca') ->
let n = Array.length ca' in
- tclTHENSEQ (do_replace_lb (!avoid)
- nparrec gls
+ tclTHENSEQ (do_replace_lb lb_scheme_key
+ (!avoid)
+ nparrec gls
ca'.(n-2) ca'.(n-1)) gls
- | _ -> error
- "Failure while solving Leibniz->Boolean."
+ | _ -> error
+ "Failure while solving Leibniz->Boolean."
)
- | _ -> error
- "Failure while solving Leibniz->Boolean."
- ]
- )
+ | _ -> error
+ "Failure while solving Leibniz->Boolean."
+ ] gsig
+
+let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
+
+let make_lb_scheme mind =
+ let mib = Global.lookup_mind mind in
+ if Array.length mib.mind_packets <> 1 then
+ errorlabstrm ""
+ (str "Automatic building of Leibniz->boolean lemmas not supported");
+ let ind = (mind,0) in
+ let nparams = mib.mind_nparams in
+ let nparrec = mib.mind_nparams_rec in
+ let lnonparrec,lnamesparrec =
+ context_chop (nparams-nparrec) mib.mind_params_ctxt in
+ [|Pfedit.build_by_tactic
+ (compute_lb_goal ind lnamesparrec nparrec)
+ (compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|]
+
+let lb_scheme_kind = declare_mutual_scheme_object "_dec_lb" make_lb_scheme
+
+let _ = lb_scheme_kind_aux := fun () -> lb_scheme_kind
+
+(**********************************************************************)
+(* Decidable equality *)
+
+let check_not_is_defined () =
+ try ignore (Coqlib.build_coq_not ()) with _ -> raise (UndefinedCst "not")
(* {n=m}+{n<>m} part *)
-let compute_dec_goal ind lnamesparrec nparrec =
+let compute_dec_goal ind lnamesparrec nparrec =
+ check_not_is_defined ();
let list_id = list_id lnamesparrec in
let create_input c =
let x = id_of_string "x" and
@@ -680,39 +727,39 @@ let compute_dec_goal ind lnamesparrec nparrec =
let lb_typ = List.map (fun (s,seq,_,_) ->
mkNamedProd x (mkVar s) (
mkNamedProd y (mkVar s) (
- mkArrow
+ mkArrow
( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
))
- ) list_id in
+ ) list_id in
let bl_typ = List.map (fun (s,seq,_,_) ->
mkNamedProd x (mkVar s) (
mkNamedProd y (mkVar s) (
- mkArrow
+ mkArrow
( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|]))
( mkApp(eq,[|mkVar s;mkVar x;mkVar y|]))
))
- ) list_id in
+ ) list_id in
let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b ->
mkNamedProd slb b a
- ) c (List.rev list_id) (List.rev lb_typ) in
+ ) c (List.rev list_id) (List.rev lb_typ) in
let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b ->
mkNamedProd sbl b a
- ) lb_input (List.rev list_id) (List.rev bl_typ) in
+ ) lb_input (List.rev list_id) (List.rev bl_typ) in
let eqs_typ = List.map (fun (s,_,_,_) ->
mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb))
) list_id in
let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b ->
mkNamedProd seq b a
- ) bl_input (List.rev list_id) (List.rev eqs_typ) in
+ ) bl_input (List.rev list_id) (List.rev eqs_typ) in
List.fold_left (fun a (n,_,t) -> mkNamedProd
(match n with Name s -> s | Anonymous -> id_of_string "A")
t a) eq_input lnamesparrec
- in
- let n = id_of_string "n" and
- m = id_of_string "m" in
+ in
+ let n = id_of_string "x" and
+ m = id_of_string "y" in
let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in
create_input (
mkNamedProd n (mkFullInd ind (2*nparrec)) (
@@ -722,93 +769,116 @@ let compute_dec_goal ind lnamesparrec nparrec =
)
)
-let compute_dec_tact ind lnamesparrec nparrec =
+let compute_dec_tact ind lnamesparrec nparrec gsig =
let list_id = list_id lnamesparrec in
let eqI = eqI ind lnamesparrec in
- let avoid = ref [] in
- let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in
- let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
- let eqfalse x = mkApp(eq,[|bb;x;ff|]) in
- let first_intros =
- ( List.map (fun (s,_,_,_) -> s ) list_id ) @
- ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
- ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @
- ( List.map (fun (_,_,_,slb) -> slb) list_id )
- in
- let fresh_first_intros = List.map ( fun s ->
- let fresh = fresh_id (!avoid) s gsig in
- avoid := fresh::(!avoid); fresh ) first_intros in
- let freshn = fresh_id (!avoid) (id_of_string "n") gsig in
- let freshm = avoid := freshn::(!avoid);
- fresh_id (!avoid) (id_of_string "m") gsig in
- let freshH = avoid := freshm::(!avoid);
- fresh_id (!avoid) (id_of_string "H") gsig in
- let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
- avoid := freshH::(!avoid);
- Pfedit.by ( tclTHENSEQ [
- intros_using fresh_first_intros;
- intros_using [freshn;freshm];
- assert_tac (Name freshH) (
- mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
- ) ]);
-(*we do this so we don't have to prove the same goal twice *)
- Pfedit.by ( tclTHEN
- (new_destruct false [Tacexpr.ElimOnConstr
- (eqbnm,Rawterm.NoBindings)]
- None
- (None,None)
- None)
- Auto.default_auto
- );
- Pfedit.by (
- let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in
- avoid := freshH2::(!avoid);
- new_destruct false [Tacexpr.ElimOnConstr
- ((mkVar freshH),Rawterm.NoBindings)]
- None
- (None,Some (dl,Genarg.IntroOrAndPattern [
- [dl,Genarg.IntroAnonymous];
- [dl,Genarg.IntroIdentifier freshH2]])) None
- );
- let arfresh = Array.of_list fresh_first_intros in
- let xargs = Array.sub arfresh 0 (2*nparrec) in
- let blI = try find_bl_proof ind with
+ let avoid = ref [] in
+ let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
+ let eqfalse x = mkApp(eq,[|bb;x;ff|]) in
+ let first_intros =
+ ( List.map (fun (s,_,_,_) -> s ) list_id ) @
+ ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
+ ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @
+ ( List.map (fun (_,_,_,slb) -> slb) list_id )
+ in
+ let fresh_first_intros = List.map ( fun s ->
+ let fresh = fresh_id (!avoid) s gsig in
+ avoid := fresh::(!avoid); fresh ) first_intros in
+ let freshn = fresh_id (!avoid) (id_of_string "x") gsig in
+ let freshm = avoid := freshn::(!avoid);
+ fresh_id (!avoid) (id_of_string "y") gsig in
+ let freshH = avoid := freshm::(!avoid);
+ fresh_id (!avoid) (id_of_string "H") gsig in
+ let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
+ avoid := freshH::(!avoid);
+ let arfresh = Array.of_list fresh_first_intros in
+ let xargs = Array.sub arfresh 0 (2*nparrec) in
+ let blI = try mkConst (find_scheme bl_scheme_kind ind) with
Not_found -> error (
"Error during the decidability part, boolean to leibniz"^
" equality is required.")
- in
- let lbI = try find_lb_proof ind with
+ in
+ let lbI = try mkConst (find_scheme lb_scheme_kind ind) with
Not_found -> error (
"Error during the decidability part, leibniz to boolean"^
" equality is required.")
- in
-
- (* left *)
- Pfedit.by ( tclTHENSEQ [ simplest_left;
- apply (mkApp(blI,Array.map(fun x->mkVar x) xargs));
- Auto.default_auto
- ]);
- (*right *)
- let freshH3 = fresh_id (!avoid) (id_of_string "H") gsig in
- avoid := freshH3::(!avoid);
- Pfedit.by (tclTHENSEQ [ simplest_right ;
- unfold_constr (Lazy.force Coqlib.coq_not_ref);
- intro;
- Equality.subst_all;
- assert_tac (Name freshH3)
- (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
- ]);
- Pfedit.by
- (tclTHENSEQ [apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
- Auto.default_auto
- ]);
- Pfedit.by (Equality.general_rewrite_bindings_in true
- all_occurrences
- (List.hd !avoid)
+ in
+ tclTHENSEQ [
+ intros_using fresh_first_intros;
+ intros_using [freshn;freshm];
+ (*we do this so we don't have to prove the same goal twice *)
+ assert_by (Name freshH) (
+ mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
+ )
+ (tclTHEN
+ (new_destruct false [Tacexpr.ElimOnConstr
+ (eqbnm,Rawterm.NoBindings)]
+ None
+ (None,None)
+ None)
+ Auto.default_auto);
+ (fun gsig ->
+ let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in
+ avoid := freshH2::(!avoid);
+ tclTHENS (
+ new_destruct false [Tacexpr.ElimOnConstr
+ ((mkVar freshH),Rawterm.NoBindings)]
+ None
+ (None,Some (dl,Genarg.IntroOrAndPattern [
+ [dl,Genarg.IntroAnonymous];
+ [dl,Genarg.IntroIdentifier freshH2]])) None
+ ) [
+ (* left *)
+ tclTHENSEQ [
+ simplest_left;
+ apply (mkApp(blI,Array.map(fun x->mkVar x) xargs));
+ Auto.default_auto
+ ];
+ (*right *)
+ (fun gsig ->
+ let freshH3 = fresh_id (!avoid) (id_of_string "H") gsig in
+ avoid := freshH3::(!avoid);
+ tclTHENSEQ [
+ simplest_right ;
+ unfold_constr (Lazy.force Coqlib.coq_not_ref);
+ intro;
+ Equality.subst_all;
+ assert_by (Name freshH3)
+ (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
+ (tclTHENSEQ [
+ apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs));
+ Auto.default_auto
+ ]);
+ Equality.general_rewrite_bindings_in true
+ all_occurrences false
+ (List.hd !avoid)
((mkVar (List.hd (List.tl !avoid))),
Rawterm.NoBindings
)
- true);
- Pfedit.by (Equality.discr_tac false None)
-
+ true;
+ Equality.discr_tac false None
+ ] gsig)
+ ] gsig)
+ ] gsig
+
+let make_eq_decidability mind =
+ let mib = Global.lookup_mind mind in
+ if Array.length mib.mind_packets <> 1 then
+ anomaly "Decidability lemma for mutual inductive types not supported";
+ let ind = (mind,0) in
+ let nparams = mib.mind_nparams in
+ let nparrec = mib.mind_nparams_rec in
+ let lnonparrec,lnamesparrec =
+ context_chop (nparams-nparrec) mib.mind_params_ctxt in
+ [|Pfedit.build_by_tactic
+ (compute_dec_goal ind lnamesparrec nparrec)
+ (compute_dec_tact ind lnamesparrec nparrec)|]
+
+let eq_dec_scheme_kind =
+ declare_mutual_scheme_object "_eq_dec" make_eq_decidability
+
+(* The eq_dec_scheme proofs depend on the equality and discr tactics
+ but the inj tactics, that comes with discr, depends on the
+ eq_dec_scheme... *)
+let _ = Equality.set_eq_dec_scheme_kind eq_dec_scheme_kind
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-19 07:50:58 +0000