summaryrefslogtreecommitdiff
path: root/contrib/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/subtac')
-rw-r--r--contrib/subtac/FixSub.v24
-rw-r--r--contrib/subtac/Utils.v10
-rw-r--r--contrib/subtac/eterm.ml56
-rw-r--r--contrib/subtac/subtac.ml6
-rw-r--r--contrib/subtac/subtac.mli11
-rw-r--r--contrib/subtac/subtac_coercion.ml18
-rw-r--r--contrib/subtac/subtac_command.ml271
-rw-r--r--contrib/subtac/subtac_command.mli1
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.ml3
-rw-r--r--contrib/subtac/subtac_interp_fixpoint.mli11
-rw-r--r--contrib/subtac/subtac_utils.ml130
-rw-r--r--contrib/subtac/subtac_utils.mli15
-rw-r--r--contrib/subtac/test/ListsTest.v8
-rw-r--r--contrib/subtac/test/Mutind.v14
-rw-r--r--contrib/subtac/test/euclid.v4
-rw-r--r--contrib/subtac/test/measure.v24
-rw-r--r--contrib/subtac/test/wf.v48
17 files changed, 499 insertions, 155 deletions
diff --git a/contrib/subtac/FixSub.v b/contrib/subtac/FixSub.v
index bbf722db..ded069bf 100644
--- a/contrib/subtac/FixSub.v
+++ b/contrib/subtac/FixSub.v
@@ -20,3 +20,27 @@ Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
End FixPoint.
End Well_founded.
+
+Require Import Wf_nat.
+Require Import Lt.
+
+Section Well_founded_measure.
+Variable A : Set.
+Variable f : A -> nat.
+Definition R := fun x y => f x < f y.
+
+Section FixPoint.
+
+Variable P : A -> Set.
+
+Variable F_sub : forall x:A, (forall y: { y : A | f y < f x }, P (proj1_sig y)) -> P x.
+
+Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (f x)) {struct r} : P x :=
+ F_sub x (fun y: { y : A | f y < f x} => Fix_measure_F_sub (proj1_sig y)
+ (Acc_inv r (f (proj1_sig y)) (proj2_sig y))).
+
+Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (f x)).
+
+End FixPoint.
+
+End Well_founded_measure.
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v
index db10cb2a..b1694d7c 100644
--- a/contrib/subtac/Utils.v
+++ b/contrib/subtac/Utils.v
@@ -34,3 +34,13 @@ induction t.
simpl ; auto.
Qed.
+Ltac destruct_one_pair :=
+ match goal with
+ | [H : (ex _) |- _] => destruct H
+ | [H : (ex2 _) |- _] => destruct H
+ | [H : (sig _) |- _] => destruct H
+ | [H : (_ /\ _) |- _] => destruct H
+end.
+
+Ltac destruct_exists := repeat (destruct_one_pair) .
+
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 382ae2d5..859f9013 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -16,7 +16,7 @@ let reverse_array arr =
Array.of_list (List.rev (Array.to_list arr))
let trace s =
- if !Options.debug then msgnl s
+ if !Options.debug then (msgnl s; msgerr s)
else ()
(** Utilities to find indices in lists *)
@@ -37,7 +37,9 @@ let list_assoc_index x l =
let subst_evars evs n t =
let evar_info id =
let rec aux i = function
- (k, h, v) :: tl -> if k = id then (i, h, v) else aux (succ i) tl
+ (k, h, v) :: tl ->
+ trace (str "Searching for " ++ int id ++ str " found: " ++ int k);
+ if k = id then (i, h, v) else aux (succ i) tl
| [] -> raise Not_found
in
let (idx, hyps, v) = aux 0 evs in
@@ -45,29 +47,29 @@ let subst_evars evs n t =
in
let rec substrec depth c = match kind_of_term c with
| Evar (k, args) ->
- (try
- let index, hyps = evar_info k in
- (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
- int (List.length hyps) ++ str " hypotheses"); with _ -> () );
-
- let ex = mkRel (index + depth) in
- (* Evar arguments are created in inverse order,
- and we must not apply to defined ones (i.e. LetIn's)
- *)
- let args =
- let rec aux hyps args acc =
- match hyps, args with
- ((_, None, _) :: tlh), (c :: tla) ->
- aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
- | ((_, Some _, _) :: tlh), (_ :: tla) ->
- aux tlh tla acc
- | [], [] -> acc
- | _, _ -> failwith "subst_evars: invalid argument"
- in aux hyps (Array.to_list args) []
- in
- mkApp (ex, Array.of_list args)
- with Not_found ->
- anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found"))
+ (let index, hyps =
+ try evar_info k
+ with Not_found ->
+ anomaly ("eterm: existential variable " ^ string_of_int k ^ " not found")
+ in
+ (try trace (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+ int (List.length hyps) ++ str " hypotheses"); with _ -> () );
+ let ex = mkRel (index + depth) in
+ (* Evar arguments are created in inverse order,
+ and we must not apply to defined ones (i.e. LetIn's)
+ *)
+ let args =
+ let rec aux hyps args acc =
+ match hyps, args with
+ ((_, None, _) :: tlh), (c :: tla) ->
+ aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
+ | ((_, Some _, _) :: tlh), (_ :: tla) ->
+ aux tlh tla acc
+ | [], [] -> acc
+ | _, _ -> failwith "subst_evars: invalid argument"
+ in aux hyps (Array.to_list args) []
+ in
+ mkApp (ex, Array.of_list args))
| _ -> map_constr_with_binders succ substrec depth c
in
substrec 0 t
@@ -106,11 +108,13 @@ open Tacticals
let eterm_term evm t tycon =
(* 'Serialize' the evars, we assume that the types of the existentials
refer to previous existentials in the list only *)
- let evl = to_list evm in
+ let evl = List.rev (to_list evm) in
+ trace (str "Eterm, transformed to list");
let evts =
(* Remove existential variables in types and build the corresponding products *)
fold_right
(fun (id, ev) l ->
+ trace (str "Eterm: " ++ str "treating evar: " ++ int id);
let hyps = Environ.named_context_of_val ev.evar_hyps in
let y' = (id, hyps, etype_of_evar l ev hyps) in
y' :: l)
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index cd2e7c43..ffb16a19 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
+(* $Id: subtac.ml 8964 2006-06-20 13:52:21Z msozeau $ *)
open Global
open Pp
@@ -43,7 +43,7 @@ open Eterm
let require_library dirpath =
let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in
Library.require_library [qualid] None
-
+(*
let subtac_one_fixpoint env isevars (f, decl) =
let ((id, n, bl, typ, body), decl) =
Subtac_interp_fixpoint.rewrite_fixpoint env [] (f, decl)
@@ -53,7 +53,7 @@ let subtac_one_fixpoint env isevars (f, decl) =
Ppconstr.pr_constr_expr body)
with _ -> ()
in ((id, n, bl, typ, body), decl)
-
+*)
let subtac_fixpoint isevars l =
(* TODO: Copy command.build_recursive *)
diff --git a/contrib/subtac/subtac.mli b/contrib/subtac/subtac.mli
index a0d2fb2b..25922782 100644
--- a/contrib/subtac/subtac.mli
+++ b/contrib/subtac/subtac.mli
@@ -1,14 +1,3 @@
val require_library : string -> unit
-val subtac_one_fixpoint :
- 'a ->
- 'b ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c
val subtac_fixpoint : 'a -> 'b -> unit
val subtac : Util.loc * Vernacexpr.vernac_expr -> unit
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 7428e1ed..78c3c70b 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -5,7 +5,7 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: subtac_coercion.ml 8889 2006-06-01 20:23:56Z msozeau $ *)
+(* $Id: subtac_coercion.ml 8964 2006-06-20 13:52:21Z msozeau $ *)
open Util
open Names
@@ -106,25 +106,25 @@ module Coercion = struct
: (Term.constr -> Term.constr) option
=
let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
- (try trace (str "Coerce called for " ++ (my_print_constr env x) ++
+ (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++
str " and "++ my_print_constr env y ++
str " with evars: " ++ spc () ++
my_print_evardefs !isevars);
with _ -> ());
let rec coerce_unify env x y =
- (try trace (str "coerce_unify from " ++ (my_print_constr env x) ++
+ (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++
str " to "++ my_print_constr env y)
with _ -> ());
try
isevars := the_conv_x_leq env x y !isevars;
- (try (trace (str "Unified " ++ (my_print_constr env x) ++
- str " and "++ my_print_constr env y));
+ (try debug 1 (str "Unified " ++ (my_print_constr env x) ++
+ str " and "++ my_print_constr env y);
with _ -> ());
None
with Reduction.NotConvertible -> coerce' env (hnf env isevars x) (hnf env isevars y)
and coerce' env x y : (Term.constr -> Term.constr) option =
let subco () = subset_coerce env isevars x y in
- (try trace (str "coerce' from " ++ (my_print_constr env x) ++
+ (try debug 1 (str "coerce' from " ++ (my_print_constr env x) ++
str " to "++ my_print_constr env y);
with _ -> ());
match (kind_of_term x, kind_of_term y) with
@@ -370,7 +370,7 @@ module Coercion = struct
let rec inh_conv_coerce_to_fail loc env isevars v t c1 =
(try
- trace (str "inh_conv_coerce_to_fail called for " ++
+ debug 1 (str "inh_conv_coerce_to_fail called for " ++
Termops.print_constr_env env t ++ str " and "++ spc () ++
Termops.print_constr_env env c1 ++ str " with evars: " ++ spc () ++
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -436,7 +436,7 @@ module Coercion = struct
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to loc env isevars cj ((n, t) as tycon) =
(try
- trace (str "Subtac_coercion.inh_conv_coerce_to called for " ++
+ debug 1 (str "Subtac_coercion.inh_conv_coerce_to called for " ++
Termops.print_constr_env env cj.uj_type ++ str " and "++ spc () ++
Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
@@ -461,7 +461,7 @@ module Coercion = struct
let inh_conv_coerces_to loc env isevars t ((abs, t') as tycon) =
(try
- trace (str "Subtac_coercion.inh_conv_coerces_to called for " ++
+ debug 1 (str "Subtac_coercion.inh_conv_coerces_to called for " ++
Termops.print_constr_env env t ++ str " and "++ spc () ++
Evarutil.pr_tycon_type env tycon ++ str " with evars: " ++ spc () ++
Evd.pr_evar_defs isevars ++ str " in env: " ++ spc () ++
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index b09228c0..c738d7a6 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -117,7 +117,8 @@ let interp_context sigma env params =
let list_chop_hd i l = match list_chop i l with
| (l1,x::l2) -> (l1,x,l2)
- | _ -> assert false
+ | (x :: [], l2) -> ([], x, [])
+ | _ -> assert(false)
let collect_non_rec env =
let rec searchrec lnonrec lnamerec ldefrec larrec nrec =
@@ -173,82 +174,189 @@ let list_of_local_binders l =
| [] -> List.rev acc
in aux [] l
-let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+let lift_binders k n l =
+ let rec aux n = function
+ | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
+ | [] -> []
+ in aux n l
+
+let rec gen_rels = function
+ 0 -> []
+ | n -> mkRel n :: gen_rels (pred n)
+
+let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
+ let sigma = Evd.empty in
+ let isevars = ref (Evd.create_evar_defs sigma) in
+ let env = Global.env() in
+ let pr c = my_print_constr env c in
+ let prr = Printer.pr_rel_context env in
+ let pr_rel env = Printer.pr_rel_context env in
+ let _ =
+ try debug 2 (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
+ Ppconstr.pr_binders bl ++ str " : " ++
+ Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
+ Ppconstr.pr_constr_expr body)
+ with _ -> ()
+ in
+ let env', binders_rel = interp_context isevars env bl in
+ let after, ((argname, _, argtyp) as arg), before = list_chop_hd (succ n) binders_rel in
+ let before_length, after_length = List.length before, List.length after in
+ let argid = match argname with Name n -> n | _ -> assert(false) in
+ let _liftafter = lift_binders 1 after_length after in
+ let envwf = push_rel_context before env in
+ let wf_rel, measure_fn =
+ let rconstr = interp_constr isevars envwf r in
+ if measure then
+ let lt_rel = constr_of_global (Lazy.force lt_ref) in
+ let name s = Name (id_of_string s) in
+ mkLambda (name "x", argtyp,
+ mkLambda (name "y", argtyp,
+ mkApp (lt_rel,
+ [| mkApp (rconstr, [| mkRel 2 |]) ;
+ mkApp (rconstr, [| mkRel 1 |]) |]))),
+ Some rconstr
+ else rconstr, None
+ in
+ let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
+ in
+ let argid' = id_of_string (string_of_id argid ^ "'") in
+ let wfarg len = (Name argid', None,
+ mkSubset (Name argid') argtyp
+ (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
+ in
+ let top_bl = after @ (arg :: before) in
+ let intern_bl = after @ (wfarg 1 :: arg :: before) in
+ let top_env = push_rel_context top_bl env in
+ let intern_env = push_rel_context intern_bl env in
+ let top_arity = interp_type isevars top_env arityc in
+ (try debug 2 (str "Intern bl: " ++ prr intern_bl) with _ -> ());
+ let proj = (Lazy.force sig_).Coqlib.proj1 in
+ let projection =
+ mkApp (proj, [| argtyp ;
+ (mkLambda (Name argid', argtyp,
+ (mkApp (wf_rel, [|mkRel 1; mkRel 3|])))) ;
+ mkRel 1
+ |])
+ in
+ (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
+ let intern_arity = substnl [projection] after_length top_arity in
+ (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
+ let intern_before_env = push_rel_context before env in
+ let intern_fun_bl = after @ [wfarg 1] in
+ (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ());
+ let intern_fun_arity = intern_arity in
+ (try debug 2 (str "Intern fun arity: " ++
+ my_print_constr intern_env intern_fun_arity) with _ -> ());
+ let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
+ let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
+ let fun_bl = after @ (intern_fun_binder :: [arg]) in
+ (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ());
+ let fun_env = push_rel_context fun_bl intern_before_env in
+ let fun_arity = interp_type isevars fun_env arityc in
+ let intern_body = interp_casted_constr isevars fun_env body fun_arity in
+ let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
+ let _ =
+ try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++
+ str "Intern bl" ++ prr intern_bl ++ spc () ++
+ str "Top bl" ++ prr top_bl ++ spc () ++
+ str "Intern arity: " ++ pr intern_arity ++
+ str "Top arity: " ++ pr top_arity ++ spc () ++
+ str "Intern body " ++ pr intern_body_lam)
+ with _ -> ()
+ in
+ let _impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits top_env top_arity
+ else []
+ in
+ let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
+ let fix_def =
+ match measure_fn with
+ None ->
+ mkApp (constr_of_reference (Lazy.force fix_sub_ref),
+ [| argtyp ;
+ wf_rel ;
+ make_existential dummy_loc intern_before_env isevars wf_proof ;
+ prop ;
+ intern_body_lam |])
+ | Some f ->
+ mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref),
+ [| argtyp ; f ; prop ;
+ intern_body_lam |])
+ in
+ let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
+ let def = it_mkLambda_or_LetIn def_appl binders_rel in
+ let typ = it_mkProd_or_LetIn top_arity binders_rel in
+ debug 2 (str "Constructed def");
+ debug 2 (my_print_constr intern_before_env def);
+ debug 2 (str "Type: " ++ my_print_constr env typ);
+ let fullcoqc = Evarutil.nf_isevar !isevars def in
+ let fullctyp = Evarutil.nf_isevar !isevars typ in
+ let _ = try trace (str "After evar normalization: " ++ spc () ++
+ str "Coq term: " ++ my_print_constr env fullcoqc ++ spc ()
+ ++ str "Coq type: " ++ my_print_constr env fullctyp)
+ with _ -> ()
+ in
+ let evm = non_instanciated_map env isevars in
+ let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in
+ let evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in
+ let evars_typ = out_some evars_typ in
+ (try trace (str "Building evars sum for : ");
+ List.iter
+ (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
+ evars;
+ with _ -> ());
+ let (sum_tac, sumg) = Subtac_utils.build_dependent_sum evars in
+ (try trace (str "Evars sum: " ++ my_print_constr env sumg);
+ trace (str "Evars type: " ++ my_print_constr env evars_typ);
+ with _ -> ());
+ let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in
+ Command.start_proof proofid goal_proof_kind sumg
+ (fun strength gr ->
+ debug 2 (str "Proof finished");
+ let def = constr_of_global gr in
+ let args = Subtac_utils.destruct_ex def sumg in
+ let _, newdef = decompose_lam_n (List.length args) evars_def in
+ let constr = Term.substl (List.rev args) newdef in
+ debug 2 (str "Applied existentials : " ++ my_print_constr env constr);
+ let ce =
+ { const_entry_body = constr;
+ const_entry_type = Some fullctyp;
+ const_entry_opaque = false;
+ const_entry_boxed = boxed}
+ in
+ let _constant = Declare.declare_constant
+ recname (DefinitionEntry ce,IsDefinition Definition)
+ in
+ definition_message recname);
+ trace (str "Started existentials proof");
+ Pfedit.by sum_tac;
+ trace (str "Applied sum tac")
+
+let build_mutrec l boxed =
let sigma = Evd.empty
and env0 = Global.env()
in
let lnameargsardef =
(*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
- lnameargsardef
+ l
in
let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef
and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
in
- (* Build the recursive context and notations for the recursive types *)
+ (* Build the recursive context and notations for the recursive types *)
let (rec_sign,rec_impls,arityl) =
List.fold_left
- (fun (env,impls,arl) ((recname,(n, ro),bl,arityc,body),_) ->
- let isevars = ref (Evd.create_evar_defs sigma) in
- match ro with
- CStructRec ->
- let arityc = Command.generalize_constr_expr arityc bl in
- let arity = interp_type isevars env0 arityc in
- let impl =
- if Impargs.is_implicit_args()
- then Impargs.compute_implicits env0 arity
- else [] in
- let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
- (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl)
- | CWfRec r ->
- let n = out_some n in
- let _ =
- try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++
- Ppconstr.pr_binders bl ++ str " : " ++
- Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++
- Ppconstr.pr_constr_expr body)
- with _ -> ()
- in
- let env', binders_rel = interp_context isevars env0 bl in
- let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in
- let argid = match argname with Name n -> n | _ -> assert(false) in
- let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in
- let envwf = push_rel_context before env0 in
- let wf_rel = interp_constr isevars envwf r in
- let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in
- let accarg = (Name accarg_id, None, mkApp (Lazy.force acc_inv, [| argtyp; wf_rel; mkRel 1 |])) in
- let argid' = id_of_string (string_of_id argid ^ "'") in
- let before_length, after_length = List.length before, List.length after in
- let full_length = before_length + 1 + after_length in
- let wfarg len = (Name argid, None,
- mkSubset (Name argid') argtyp
- (mkApp (wf_rel, [|mkRel 1; mkRel (len + 1)|])))
- in
- let new_bl = after' @ (accarg :: arg :: before)
- and intern_bl = after @ (wfarg (before_length + 1) :: before)
- in
- let intern_env = push_rel_context intern_bl env0 in
- let env' = push_rel_context new_bl env0 in
- let arity = interp_type isevars intern_env arityc in
- let intern_arity = it_mkProd_or_LetIn arity intern_bl in
- let arity' = interp_type isevars env' arityc in
- let arity' = it_mkProd_or_LetIn arity' new_bl in
- let fun_bl = after @ ((Name recname, None, intern_arity) :: arg :: before) in
- let _ =
- let pr c = my_print_constr env c in
- let prr = Printer.pr_rel_context env in
- try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++
- str "Intern bl" ++ prr intern_bl ++ spc () ++
- str "Extern bl" ++ prr new_bl ++ spc () ++
- str "Intern arity: " ++ pr intern_arity)
- with _ -> ()
- in
- let impl =
- if Impargs.is_implicit_args()
- then Impargs.compute_implicits intern_env arity'
- else [] in
- let impls' = (recname,([],impl,compute_arguments_scope arity'))::impls in
- (Environ.push_named (recname,None,arity') env, impls',
- (isevars, Some (full_length - n, argtyp, wf_rel, fun_bl, intern_bl, intern_arity), arity')::arl))
+ (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) ->
+ let isevars = ref (Evd.create_evar_defs sigma) in
+ let arityc = Command.generalize_constr_expr arityc bl in
+ let arity = interp_type isevars env0 arityc in
+ let impl =
+ if Impargs.is_implicit_args()
+ then Impargs.compute_implicits env0 arity
+ else [] in
+ let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
+ (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
(env0,[],[]) lnameargsardef in
let arityl = List.rev arityl in
let notations =
@@ -283,7 +391,6 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
let (lnonrec,(namerec,defrec,arrec,nvrec)) =
collect_non_rec env0 lrecnames recdef arityl nv in
- let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *)
let declare arrec defrec =
let recvec =
Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
@@ -293,7 +400,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
my_print_constr env0 (recvec.(i)));
with _ -> ());
let ce =
- { const_entry_body = mkFix ((nvrec',i),recdecls);
+ { const_entry_body = mkFix ((nvrec,i),recdecls);
const_entry_type = Some arrec.(i);
const_entry_opaque = false;
const_entry_boxed = boxed} in
@@ -384,6 +491,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None)
defs
in
+ match real_evars with
+ [] -> declare (List.rev_map (fun (id, c, _) ->
+ snd (decompose_lam_n recdefs c)) defs)
+ | l ->
+
Subtac_utils.and_tac real_evars
(fun f _ gr ->
let _ = trace (str "Got a proof of: " ++ pr_global gr ++
@@ -431,5 +543,28 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed
Environ.NoBody -> trace (str "Constant has no body")
| Environ.Opaque -> trace (str "Constant is opaque")
)
+
+let out_n = function
+ Some n -> n
+ | None -> 0
+
+let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
+ match lnameargsardef with
+ | ((id, (n, CWfRec r), bl, typ, body), no) :: [] ->
+ build_wellfounded (id, out_n n, bl, typ, body) r false no boxed
+ | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] ->
+ build_wellfounded (id, out_n n, bl, typ, body) r true no boxed
+ | l ->
+ let lnameargsardef =
+ List.map (fun ((id, (n, ro), bl, typ, body), no) ->
+ match ro with
+ CStructRec -> (id, out_n n, bl, typ, body), no
+ | CWfRec _ | CMeasureRec _ ->
+ errorlabstrm "Subtac_command.build_recursive"
+ (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
+ lnameargsardef
+ in
+ build_mutrec lnameargsardef boxed;
+ assert(false)
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index e1bbbbb5..90ffb892 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -38,5 +38,6 @@ val interp_constr_judgment :
constr_expr -> unsafe_judgment
val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
val recursive_message : global_reference array -> std_ppcmds
+
val build_recursive :
(fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index 858fad1a..bb35833f 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -60,7 +60,7 @@ let pr_binder_list b =
let rec rewrite_rec_calls l c = c
-
+(*
let rewrite_fixpoint env l (f, decl) =
let (id, (n, ro), bl, typ, body) = f in
let body = rewrite_rec_calls l body in
@@ -151,3 +151,4 @@ let rewrite_fixpoint env l (f, decl) =
Ppconstr.pr_constr_expr body')
in (id, (succ n, ro), bl', typ, body'), decl
+*)
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index fafbb2da..149e7580 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -15,14 +15,3 @@ val list_of_local_binders :
val pr_binder_list :
(('a * Names.name) * Topconstr.constr_expr) list -> Pp.std_ppcmds
val rewrite_rec_calls : 'a -> 'b -> 'b
-val rewrite_fixpoint :
- 'a ->
- 'b ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c ->
- (Names.identifier * (int * Topconstr.recursion_order_expr) *
- Topconstr.local_binder list * Topconstr.constr_expr *
- Topconstr.constr_expr) *
- 'c
diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml
index 59c858a6..d4db7c27 100644
--- a/contrib/subtac/subtac_utils.ml
+++ b/contrib/subtac/subtac_utils.ml
@@ -22,12 +22,16 @@ let fixsub = lazy (init_constant fixsub_module "Fix_sub")
let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
-let make_ref s = Qualid (dummy_loc, (qualid_of_string s))
-let well_founded_ref = make_ref "Init.Wf.Well_founded"
-let acc_ref = make_ref "Init.Wf.Acc"
-let acc_inv_ref = make_ref "Init.Wf.Acc_inv"
-let fix_sub_ref = make_ref "Coq.subtac.FixSub.Fix_sub"
-let lt_wf_ref = make_ref "Coq.Wf_nat.lt_wf"
+let make_ref l s = lazy (init_reference l s)
+let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
+let acc_ref = make_ref ["Init";"Wf"] "Acc"
+let acc_inv_ref = make_ref ["Init";"Wf"] "Acc_inv"
+let fix_sub_ref = make_ref ["subtac";"FixSub"] "Fix_sub"
+let fix_measure_sub_ref = make_ref ["subtac";"FixSub"] "Fix_measure_sub"
+let lt_ref = make_ref ["Init";"Peano"] "lt"
+let lt_wf_ref = make_ref ["Wf_nat"] "lt_wf"
+
+let make_ref s = Qualid (dummy_loc, qualid_of_string s)
let sig_ref = make_ref "Init.Specif.sig"
let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
@@ -82,18 +86,19 @@ let my_print_evardefs = Evd.pr_evar_defs
let my_print_tycon_type = Evarutil.pr_tycon_type
+let debug_level = 2
let debug n s =
- if !Options.debug then
+ if !Options.debug && n >= debug_level then
msgnl s
else ()
let debug_msg n s =
- if !Options.debug then s
+ if !Options.debug && n >= debug_level then s
else mt ()
let trace s =
- if !Options.debug then msgnl s
+ if !Options.debug && debug_level > 0 then msgnl s
else ()
let wf_relations = Hashtbl.create 10
@@ -153,6 +158,9 @@ let non_instanciated_map env evd =
let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
+let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
+
let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
@@ -164,7 +172,7 @@ let build_dependent_sum l =
(n, t) :: tl ->
let t' = mkLambda (Name n, t, typ) in
trace (spc () ++ str ("treating evar " ^ string_of_id n));
- (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
+ (try trace (str " assert: " ++ my_print_constr (Global.env ()) t)
with _ -> ());
let tac' =
tclTHENS (assert_tac true (Name n) t)
@@ -183,6 +191,39 @@ let build_dependent_sum l =
(_, hd) :: tl -> aux (intros, hd) tl
| [] -> raise (Invalid_argument "build_dependent_sum")
+let id x = x
+
+let build_dependent_sum l =
+ let rec aux names conttac conttype = function
+ (n, t) :: ((_ :: _) as tl) ->
+ let hyptype = substl names t in
+ trace (spc () ++ str ("treating evar " ^ string_of_id n));
+ (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype)
+ with _ -> ());
+ let tac = assert_tac true (Name n) hyptype in
+ let conttac =
+ (fun cont ->
+ conttac
+ (tclTHENS tac
+ ([intros;
+ (tclTHENSEQ
+ [constructor_tac (Some 1) 1
+ (Rawterm.ImplicitBindings [mkVar n]);
+ cont]);
+ ])))
+ in
+ let conttype =
+ (fun typ ->
+ let tex = mkLambda (Name n, t, typ) in
+ conttype
+ (mkApp (Lazy.force ex_ind, [| t; tex |])))
+ in
+ aux (mkVar n :: names) conttac conttype tl
+ | (n, t) :: [] ->
+ (conttac intros, conttype t)
+ | [] -> raise (Invalid_argument "build_dependent_sum")
+ in aux [] id id (List.rev l)
+
open Proof_type
open Tacexpr
@@ -251,6 +292,75 @@ let destruct_ex ext ex =
| _ -> [acc]
in aux ex ext
+open Rawterm
+
+
+let list_mapi f =
+ let rec aux i = function
+ hd :: tl -> f i hd :: aux (succ i) tl
+ | [] -> []
+ in aux 0
+
+let rewrite_cases_aux (loc, po, tml, eqns) =
+ let tml = list_mapi (fun i (c, (n, opt)) -> c,
+ ((match n with
+ Name id -> (match c with
+ | RVar (_, id') when id = id' ->
+ Name (id_of_string (string_of_id id ^ "'"))
+ | _ -> n)
+ | Anonymous -> Name (id_of_string ("x" ^ string_of_int i))),
+ opt)) tml
+ in
+ let mkHole = RHole (dummy_loc, InternalHole) in
+ let mkeq c n = RApp (dummy_loc, RRef (dummy_loc, (Lazy.force eqind_ref)),
+ [mkHole; c; n])
+ in
+ let eqs_types =
+ List.map
+ (fun (c, (n, _)) ->
+ let id = match n with Name id -> id | _ -> assert false in
+ let heqid = id_of_string ("Heq" ^ string_of_id id) in
+ Name heqid, mkeq c (RVar (dummy_loc, id)))
+ tml
+ in
+ let po =
+ List.fold_right
+ (fun (n,t) acc ->
+ RProd (dummy_loc, Anonymous, t, acc))
+ eqs_types (match po with
+ Some e -> e
+ | None -> mkHole)
+ in
+ let eqns =
+ List.map (fun (loc, idl, cpl, c) ->
+ let c' =
+ List.fold_left
+ (fun acc (n, t) ->
+ RLambda (dummy_loc, n, mkHole, acc))
+ c eqs_types
+ in (loc, idl, cpl, c'))
+ eqns
+ in
+ let mk_refl_equal c = RApp (dummy_loc, RRef (dummy_loc, Lazy.force refl_equal_ref),
+ [mkHole; c])
+ in
+ let refls = List.map (fun (c, _) -> mk_refl_equal c) tml in
+ let case = RCases (loc,Some po,tml,eqns) in
+ let app = RApp (dummy_loc, case, refls) in
+ app
+
+let rec rewrite_cases c =
+ match c with
+ RCases _ -> let c' = map_rawconstr rewrite_cases c in
+ (match c' with
+ | RCases (x, y, z, w) -> rewrite_cases_aux (x,y,z,w)
+ | _ -> assert(false))
+ | _ -> map_rawconstr rewrite_cases c
+
+let rewrite_cases env c =
+ let c' = rewrite_cases c in
+ let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
+ c'
let list_mapi f =
let rec aux i = function
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index a90f281f..4a7e8177 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -18,12 +18,13 @@ val fixsub_module : string list
val init_constant : string list -> string -> constr
val init_reference : string list -> string -> global_reference
val fixsub : constr lazy_t
-val make_ref : string -> reference
-val well_founded_ref : reference
-val acc_ref : reference
-val acc_inv_ref : reference
-val fix_sub_ref : reference
-val lt_wf_ref : reference
+val well_founded_ref : global_reference lazy_t
+val acc_ref : global_reference lazy_t
+val acc_inv_ref : global_reference lazy_t
+val fix_sub_ref : global_reference lazy_t
+val fix_measure_sub_ref : global_reference lazy_t
+val lt_ref : global_reference lazy_t
+val lt_wf_ref : global_reference lazy_t
val sig_ref : reference
val proj1_sig_ref : reference
val proj2_sig_ref : reference
@@ -69,6 +70,8 @@ val string_of_hole_kind : hole_kind -> string
val non_instanciated_map : env -> evar_defs ref -> evar_map
val global_kind : logical_kind
val goal_kind : locality_flag * goal_object_kind
+val global_proof_kind : logical_kind
+val goal_proof_kind : locality_flag * goal_object_kind
val global_fix_kind : logical_kind
val goal_fix_kind : locality_flag * goal_object_kind
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index a29cd039..8429c267 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -5,12 +5,13 @@ Variable A : Set.
Program Definition myhd : forall { l : list A | length l <> 0 }, A :=
fun l =>
- match l with
+ match `l with
| nil => _
| hd :: tl => hd
end.
Proof.
- destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+ destruct l ; simpl ; intro H.
+ rewrite H in n ; intuition.
Defined.
@@ -24,7 +25,7 @@ Program Definition mytail : forall { l : list A | length l <> 0 }, list A :=
| hd :: tl => tl
end.
Proof.
-destruct l ; simpl ; intro H ; rewrite <- H in n ; intuition.
+destruct l ; simpl ; intro H ; rewrite H in n ; intuition.
Defined.
Extraction mytail.
@@ -50,7 +51,6 @@ Program Fixpoint append (l : list A) (l' : list A) { struct l } :
| nil => l'
| hd :: tl => hd :: (append tl l')
end.
-simpl.
subst ; auto.
simpl ; rewrite (subset_simpl (append tl0 l')).
simpl ; subst.
diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v
index ab200354..0b40ef82 100644
--- a/contrib/subtac/test/Mutind.v
+++ b/contrib/subtac/test/Mutind.v
@@ -1,7 +1,13 @@
-Fixpoint f (a : nat) : nat := match a with 0 => 0
-| S a' => g a a'
+Program Fixpoint f (a : nat) : nat :=
+ match a with
+ | 0 => 0
+ | S a' => g a a'
end
with g (a b : nat) { struct b } : nat :=
- match b with 0 => 0
+ match b with
+ | 0 => 0
| S b' => f b'
- end. \ No newline at end of file
+ end.
+
+Check f.
+Check g. \ No newline at end of file
diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v
index 481b6708..ba5bdf23 100644
--- a/contrib/subtac/test/euclid.v
+++ b/contrib/subtac/test/euclid.v
@@ -12,8 +12,8 @@ reflexivity.
Defined.
Extraction testsig.
-Extraction sigS.
-Extract Inductive sigS => "" [ "" ].
+Extraction sig.
+Extract Inductive sig => "" [ "" ].
Extraction testsig.
Require Import Coq.Arith.Compare_dec.
diff --git a/contrib/subtac/test/measure.v b/contrib/subtac/test/measure.v
new file mode 100644
index 00000000..4764037d
--- /dev/null
+++ b/contrib/subtac/test/measure.v
@@ -0,0 +1,24 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Fixpoint size (a : nat) : nat :=
+ match a with
+ 0 => 1
+ | S n => S (size n)
+ end.
+
+Program Fixpoint test_measure (a : nat) {measure a size} : nat :=
+ match a with
+ | S (S n) => S (test_measure n)
+ | x => x
+ end.
+subst.
+unfold n0.
+auto with arith.
+Qed.
+
+Check test_measure.
+Print test_measure. \ No newline at end of file
diff --git a/contrib/subtac/test/wf.v b/contrib/subtac/test/wf.v
new file mode 100644
index 00000000..49fec2b8
--- /dev/null
+++ b/contrib/subtac/test/wf.v
@@ -0,0 +1,48 @@
+Notation "( x & y )" := (@existS _ _ x y) : core_scope.
+Unset Printing All.
+Require Import Coq.Arith.Compare_dec.
+
+Require Import Coq.subtac.Utils.
+
+Ltac one_simpl_hyp :=
+ match goal with
+ | [H : (`exist _ _ _) = _ |- _] => simpl in H
+ | [H : _ = (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) < _ |- _] => simpl in H
+ | [H : _ < (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) <= _ |- _] => simpl in H
+ | [H : _ <= (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) > _ |- _] => simpl in H
+ | [H : _ > (`exist _ _ _) |- _] => simpl in H
+ | [H : (`exist _ _ _) >= _ |- _] => simpl in H
+ | [H : _ >= (`exist _ _ _) |- _] => simpl in H
+ end.
+
+Ltac one_simpl_subtac :=
+ destruct_exists ;
+ repeat one_simpl_hyp ; simpl.
+
+Ltac simpl_subtac := do 3 one_simpl_subtac ; simpl.
+
+Require Import Omega.
+Require Import Wf_nat.
+
+Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} :
+ { q : nat & { r : nat | a = b * q + r /\ r < b } } :=
+ if le_lt_dec b a then let (q', r) := euclid (a - b) b in
+ (S q' & r)
+ else (O & a).
+destruct b ; simpl_subtac.
+omega.
+simpl_subtac.
+assert(x0 * S q' = x0 + x0 * q').
+rewrite <- mult_n_Sm.
+omega.
+rewrite H2 ; omega.
+simpl_subtac.
+split ; auto with arith.
+omega.
+apply lt_wf.
+Defined.
+
+Check euclid_evars_proof. \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 05:06:32 +0000