aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-01 14:14:04 +0000
committerGravatar jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-03-01 14:14:04 +0000
commitacb788d8cf5f85dc6e9aee659e60f9373523cd18 (patch)
tree35046018dfa86b6dfd8923abe5fd90c30ea9f9d6
parentffba1672aa7a47257e2547aad7198c10dc5dcaf4 (diff)
New version of recdef :
+ Allowing much more function to be defined. + Using completely new algorithm to define non structural fixpoints git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15009 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat
-rw-r--r--plugins/funind/functional_principles_proofs.ml101
-rw-r--r--plugins/funind/indfun.ml27
-rw-r--r--plugins/funind/indfun_common.ml30
-rw-r--r--plugins/funind/indfun_common.mli11
-rw-r--r--plugins/funind/recdef.ml1824
-rw-r--r--plugins/funind/recdef.mli20
6 files changed, 1096 insertions, 917 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 1d1e4a2a6..865074d6b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -17,7 +17,7 @@ open Libnames
let msgnl = Pp.msgnl
-
+(*
let observe strm =
if do_observe ()
then Pp.msgnl strm
@@ -46,12 +46,57 @@ let observe_tac_stream s tac g =
else tac g
let observe_tac s tac g = observe_tac_stream (str s) tac g
+ *)
+
-(* let tclTRYD tac = *)
-(* if !Flags.debug || do_observe () *)
-(* then (fun g -> try (\* do_observe_tac "" *\)tac g with _ -> tclIDTAC g) *)
-(* else tac *)
+let debug_queue = Stack.create ()
+let rec print_debug_queue b e =
+ if not (Stack.is_empty debug_queue)
+ then
+ begin
+ let lmsg,goal = Stack.pop debug_queue in
+ if b then
+ Pp.msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+ else
+ begin
+ Pp.msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal);
+ end;
+ print_debug_queue false e;
+ end
+
+let observe strm =
+ if do_observe ()
+ then Pp.msgnl strm
+ else ()
+
+let do_observe_tac s tac g =
+ let goal = Printer.pr_goal g in
+ let lmsg = (str "observation : ") ++ s in
+ Stack.push (lmsg,goal) debug_queue;
+ try
+ let v = tac g in
+ ignore(Stack.pop debug_queue);
+ v
+ with e ->
+ begin
+ if not (Stack.is_empty debug_queue)
+ then
+ begin
+ let e : exn = Cerrors.process_vernac_interp_error e in
+ print_debug_queue true e
+ end
+ ;
+ raise e
+ end
+
+let observe_tac_stream s tac g =
+ if do_observe ()
+ then do_observe_tac s tac g
+ else tac g
+
+let observe_tac s = observe_tac_stream (str s)
+
let list_chop ?(msg="") n l =
try
@@ -812,20 +857,20 @@ let build_proof
| Rel _ -> anomaly "Free var in goal conclusion !"
and build_proof do_finalize dyn_infos g =
(* observe (str "proving with "++Printer.pr_lconstr dyn_infos.info++ str " on goal " ++ pr_gls g); *)
- observe_tac "build_proof" (build_proof_aux do_finalize dyn_infos) g
+ observe_tac_stream (str "build_proof with " ++ Printer.pr_lconstr dyn_infos.info ) (build_proof_aux do_finalize dyn_infos) g
and build_proof_args do_finalize dyn_infos (* f_args' args *) :tactic =
fun g ->
let (f_args',args) = dyn_infos.info in
let tac : tactic =
fun g ->
- match args with
- | [] ->
+ match args with
+ | [] ->
do_finalize {dyn_infos with info = f_args'} g
- | arg::args ->
-(* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
-(* fnl () ++ *)
-(* pr_goal (Tacmach.sig_it g) *)
-(* ); *)
+ | arg::args ->
+ (* observe (str "build_proof_args with arg := "++ pr_lconstr_env (pf_env g) arg++ *)
+ (* fnl () ++ *)
+ (* pr_goal (Tacmach.sig_it g) *)
+ (* ); *)
let do_finalize dyn_infos =
let new_arg = dyn_infos.info in
(* tclTRYD *)
@@ -839,14 +884,14 @@ let build_proof
g
in
(* observe_tac "build_proof_args" *) (tac ) g
- in
- let do_finish_proof dyn_infos =
+ in
+ let do_finish_proof dyn_infos =
(* tclTRYD *) (clean_goal_with_heq
- ptes_infos
- finish_proof dyn_infos)
+ ptes_infos
+ finish_proof dyn_infos)
in
- (* observe_tac "build_proof" *)
- (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos)
+ (* observe_tac "build_proof" *)
+ (build_proof (clean_goal_with_heq ptes_infos do_finish_proof) dyn_infos)
@@ -1339,15 +1384,13 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
(* Proof of principles of general functions *)
-let h_id = Recdef.h_id
-and hrec_id = Recdef.hrec_id
-and acc_inv_id = Recdef.acc_inv_id
-and ltof_ref = Recdef.ltof_ref
-and acc_rel = Recdef.acc_rel
-and well_founded = Recdef.well_founded
-and h_intros = Recdef.h_intros
-and list_rewrite = Recdef.list_rewrite
-and evaluable_of_global_reference = Recdef.evaluable_of_global_reference
+(* let hrec_id =
+(* and acc_inv_id = Recdef.acc_inv_id *)
+(* and ltof_ref = Recdef.ltof_ref *)
+(* and acc_rel = Recdef.acc_rel *)
+(* and well_founded = Recdef.well_founded *)
+(* and list_rewrite = Recdef.list_rewrite *)
+(* and evaluable_of_global_reference = Recdef.evaluable_of_global_reference *)
@@ -1443,7 +1486,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
);
observe_tac "rew_and_finish"
(tclTHENLIST
- [tclTRY(Recdef.list_rewrite false (List.map mkVar eqs));
+ [tclTRY(list_rewrite false (List.map (fun v -> (mkVar v,true)) eqs));
observe_tac "rewrite_eqs_in_eqs" (rewrite_eqs_in_eqs eqs);
(observe_tac "finishing using"
(
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 4546ff08d..97a49d6f0 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -262,20 +262,27 @@ let warning_error names e =
let e = Cerrors.process_vernac_interp_error e in
let e_explain e =
match e with
- | ToShow e -> spc () ++ Errors.print e
- | _ -> if do_observe () then (spc () ++ Errors.print e) else mt ()
+ | ToShow e ->
+ let e = Cerrors.process_vernac_interp_error e in
+ spc () ++ Errors.print e
+ | _ ->
+ if do_observe ()
+ then
+ let e = Cerrors.process_vernac_interp_error e in
+ (spc () ++ Errors.print e)
+ else mt ()
in
match e with
| Building_graph e ->
- Pp.msg_warning
- (str "Cannot define graph(s) for " ++
- h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
- e_explain e)
+ Pp.msg_warning
+ (str "Cannot define graph(s) for " ++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ e_explain e)
| Defining_principle e ->
- Pp.msg_warning
- (str "Cannot define principle(s) for "++
- h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
- e_explain e)
+ Pp.msg_warning
+ (str "Cannot define principle(s) for "++
+ h 1 (prlist_with_sep (fun _ -> str","++spc ()) Ppconstr.pr_id names) ++
+ e_explain e)
| _ -> raise e
let error_error names e =
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index dd475315c..d6fb28ba5 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,8 +1,8 @@
open Names
open Pp
-
open Libnames
-
+open Refiner
+open Hiddentac
let mk_prefix pre id = id_of_string (pre^(string_of_id id))
let mk_rel_id = mk_prefix "R_"
let mk_correct_id id = Nameops.add_suffix (mk_rel_id id) "_correct"
@@ -475,8 +475,7 @@ let function_debug_sig =
let _ = declare_bool_option function_debug_sig
-let do_observe () =
- !function_debug = true
+let do_observe () = !function_debug
@@ -521,3 +520,26 @@ let jmeq_refl () =
Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
init_constant ["Logic";"JMeq"] "JMeq_refl"
with e -> raise (ToShow e)
+
+let h_intros l =
+ tclMAP h_intro l
+
+let h_id = id_of_string "h"
+let hrec_id = id_of_string "hrec"
+let well_founded = function () -> (coq_constant "well_founded")
+let acc_rel = function () -> (coq_constant "Acc")
+let acc_inv_id = function () -> (coq_constant "Acc_inv")
+let well_founded_ltof = function () -> (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
+let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
+
+let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (Global.env ()) *)
+ match r with
+ ConstRef sp -> EvalConstRef sp
+ | VarRef id -> EvalVarRef id
+ | _ -> assert false;;
+
+let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
+ tclREPEAT
+ (List.fold_right
+ (fun (eq,b) i -> tclORELSE ((if b then Equality.rewriteLR else Equality.rewriteRL) eq) i)
+ (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e0076735a..f6500f74d 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -112,3 +112,14 @@ exception Defining_principle of exn
exception ToShow of exn
val is_strict_tcc : unit -> bool
+
+val h_intros: Names.identifier list -> Proof_type.tactic
+val h_id : Names.identifier
+val hrec_id : Names.identifier
+val acc_inv_id : Term.constr Util.delayed
+val ltof_ref : Libnames.global_reference Util.delayed
+val well_founded_ltof : Term.constr Util.delayed
+val acc_rel : Term.constr Util.delayed
+val well_founded : Term.constr Util.delayed
+val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference
+val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 399784df3..5e0aac4c2 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -7,7 +7,7 @@
(************************************************************************)
(*i camlp4deps: "parsing/grammar.cma" i*)
-
+open Tacexpr
open Term
open Namegen
open Environ
@@ -45,14 +45,81 @@ open Auto
open Eauto
open Genarg
+open Indfun_common
-let compute_renamed_type gls c =
- rename_bound_vars_as_displayed [] (pf_type_of gls c)
-let qed () = Lemmas.save_named true
+(* Ugly things which should not be here *)
+
+let coq_base_constant s =
+ Coqlib.gen_constant_in_modules "RecursiveDefinition"
+ (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
+
+let coq_constant s =
+ Coqlib.gen_constant_in_modules "RecursiveDefinition"
+ (Coqlib.init_modules @ Coqlib.arith_modules) s;;
+
+let find_reference sl s =
+ (locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+
+
+let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
+ fun f_id kind value ->
+ let ce = {const_entry_body = value;
+ const_entry_secctx = None;
+ const_entry_type = None;
+ const_entry_opaque = false } in
+ ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
+
let defined () = Lemmas.save_named false
+let def_of_const t =
+ match (kind_of_term t) with
+ Const sp ->
+ (try (match body_of_constant (Global.lookup_constant sp) with
+ | Some c -> Declarations.force c
+ | _ -> assert false)
+ with _ ->
+ anomaly ("Cannot find definition of constant "^
+ (string_of_id (id_of_label (con_label sp))))
+ )
+ |_ -> assert false
+
+let type_of_const t =
+ match (kind_of_term t) with
+ Const sp -> Typeops.type_of_constant (Global.env()) sp
+ |_ -> assert false
+
+
+let constant sl s =
+ constr_of_global
+ (locate (make_qualid(Names.make_dirpath
+ (List.map id_of_string (List.rev sl)))
+ (id_of_string s)));;
+let const_of_ref = function
+ ConstRef kn -> kn
+ | _ -> anomaly "ConstRef expected"
+
+
+let nf_zeta env =
+ Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+ env
+ Evd.empty
+
+
+let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
+ let clos_norm_flags flgs env sigma t =
+ Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
+ clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty
+
+
+
+
+
+
+(* Generic values *)
let pf_get_new_ids idl g =
let ids = pf_ids_of_hyps g in
List.fold_right
@@ -60,34 +127,130 @@ let pf_get_new_ids idl g =
idl
[]
-let pf_get_new_id id g =
- List.hd (pf_get_new_ids [id] g)
+let compute_renamed_type gls c =
+ rename_bound_vars_as_displayed [] (pf_type_of gls c)
+let h'_id = id_of_string "h'"
+let heq_id = id_of_string "Heq"
+let teq_id = id_of_string "teq"
+let ano_id = id_of_string "anonymous"
+let x_id = id_of_string "x"
+let k_id = id_of_string "k"
+let v_id = id_of_string "v"
+let def_id = id_of_string "def"
+let p_id = id_of_string "p"
+let rec_res_id = id_of_string "rec_res";;
+let lt = function () -> (coq_base_constant "lt")
+let le = function () -> (coq_base_constant "le")
+let ex = function () -> (coq_base_constant "ex")
+let nat = function () -> (coq_base_constant "nat")
+let coq_sig = function () -> (coq_base_constant "sig")
+let iter_ref () =
+ try find_reference ["Recdef"] "iter"
+ with Not_found -> error "module Recdef not loaded"
+let iter = function () -> (constr_of_global (delayed_force iter_ref))
+let eq = function () -> (coq_base_constant "eq")
+let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
+let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm")
+let le_trans = function () -> (coq_base_constant "le_trans")
+let le_lt_trans = function () -> (coq_base_constant "le_lt_trans")
+let lt_S_n = function () -> (coq_base_constant "lt_S_n")
+let le_n = function () -> (coq_base_constant "le_n")
+let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
+let coq_O = function () -> (coq_base_constant "O")
+let coq_S = function () -> (coq_base_constant "S")
+let gt_antirefl = function () -> (coq_constant "gt_irrefl")
+let lt_n_O = function () -> (coq_base_constant "lt_n_O")
+let lt_n_Sn = function () -> (coq_base_constant "lt_n_Sn")
+let f_equal = function () -> (coq_constant "f_equal")
+let well_founded_induction = function () -> (coq_constant "well_founded_induction")
+let max_ref = function () -> (find_reference ["Recdef"] "max")
+let max_constr = function () -> (constr_of_global (delayed_force max_ref))
+let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
+
+let f_S t = mkApp(delayed_force coq_S, [|t|]);;
+let make_refl_eq constructor type_of_t t =
+ mkApp(constructor,[|type_of_t;t|])
-let h_intros l =
- tclMAP h_intro l
+let rec n_x_id ids n =
+ if n = 0 then []
+ else let x = next_ident_away_in_goal x_id ids in
+ x::n_x_id (x::ids) (n-1);;
-let debug_queue = Stack.create ()
+
+let simpl_iter clause =
+ reduce
+ (Lazy
+ {rBeta=true;rIota=true;rZeta= true; rDelta=false;
+ rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]})
+ clause
+
+(* Others ugly things ... *)
+let (value_f:constr list -> global_reference -> constr) =
+ fun al fterm ->
+ let d0 = dummy_loc in
+ let rev_x_id_l =
+ (
+ List.fold_left
+ (fun x_id_l _ ->
+ let x_id = next_ident_away_in_goal x_id x_id_l in
+ x_id::x_id_l
+ )
+ []
+ al
+ )
+ in
+ let context = List.map
+ (fun (x, c) -> Name x, None, c) (List.combine rev_x_id_l (List.rev al))
+ in
+ let env = Environ.push_rel_context context (Global.env ()) in
+ let glob_body =
+ GCases
+ (d0,RegularStyle,None,
+ [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
+ (Anonymous,None)],
+ [d0, [v_id], [PatCstr(d0,(destIndRef
+ (delayed_force coq_sig_ref),1),
+ [PatVar(d0, Name v_id);
+ PatVar(d0, Anonymous)],
+ Anonymous)],
+ GVar(d0,v_id)])
+ in
+ let body = understand Evd.empty env glob_body in
+ it_mkLambda_or_LetIn body context
+
+let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) =
+ fun f_id kind input_type fterm_ref ->
+ declare_fun f_id kind (value_f input_type fterm_ref);;
+
+(* Debuging mechanism *)
+let debug_queue = Stack.create ()
+
let rec print_debug_queue b e =
if not (Stack.is_empty debug_queue)
then
begin
let lmsg,goal = Stack.pop debug_queue in
if b then
- msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
+ Pp.msgnl (lmsg ++ (str " raised exception " ++ Errors.print e) ++ str " on goal " ++ goal)
else
begin
- msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal);
+ Pp.msgnl (str " from " ++ lmsg ++ str " on goal " ++ goal);
end;
print_debug_queue false e;
end
-
+let observe strm =
+ if do_observe ()
+ then Pp.msgnl strm
+ else ()
+
let do_observe_tac s tac g =
let goal = Printer.pr_goal g in
- let lmsg = (str "recdef : ") ++ (str s) in
+ let lmsg = (str "recdef : ") ++ s in
+ observe (s++fnl());
Stack.push (lmsg,goal) debug_queue;
try
let v = tac g in
@@ -96,246 +259,407 @@ let do_observe_tac s tac g =
with e ->
if not (Stack.is_empty debug_queue)
then
- print_debug_queue true e;
+ begin
+ let e : exn = Cerrors.process_vernac_interp_error e in
+ print_debug_queue true e
+ end
+ ;
raise e
let observe_tac s tac g =
- if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+ if do_observe ()
then do_observe_tac s tac g
else tac g
-let hyp_ids = List.map id_of_string
- ["x";"v";"k";"def";"p";"h";"n";"h'"; "anonymous"; "teq"; "rec_res";
- "hspec";"heq"; "hrec"; "hex"; "teq"; "pmax";"hle"];;
-
-let rec nthtl = function
- l, 0 -> l | _::tl, n -> nthtl (tl, n-1) | [], _ -> [];;
-
-let hyp_id n l = List.nth l n;;
-
-let (x_id:identifier) = hyp_id 0 hyp_ids;;
-let (v_id:identifier) = hyp_id 1 hyp_ids;;
-let (k_id:identifier) = hyp_id 2 hyp_ids;;
-let (def_id:identifier) = hyp_id 3 hyp_ids;;
-let (p_id:identifier) = hyp_id 4 hyp_ids;;
-let (h_id:identifier) = hyp_id 5 hyp_ids;;
-let (n_id:identifier) = hyp_id 6 hyp_ids;;
-let (h'_id:identifier) = hyp_id 7 hyp_ids;;
-let (ano_id:identifier) = hyp_id 8 hyp_ids;;
-let (rec_res_id:identifier) = hyp_id 10 hyp_ids;;
-let (hspec_id:identifier) = hyp_id 11 hyp_ids;;
-let (heq_id:identifier) = hyp_id 12 hyp_ids;;
-let (hrec_id:identifier) = hyp_id 13 hyp_ids;;
-let (hex_id:identifier) = hyp_id 14 hyp_ids;;
-let (teq_id:identifier) = hyp_id 15 hyp_ids;;
-let (pmax_id:identifier) = hyp_id 16 hyp_ids;;
-let (hle_id:identifier) = hyp_id 17 hyp_ids;;
-
-let message s = if Flags.is_verbose () then msgnl(str s);;
+(* Conclusion tactics *)
-let def_of_const t =
- match (kind_of_term t) with
- Const sp ->
- (try (match body_of_constant (Global.lookup_constant sp) with
- | Some c -> Declarations.force c
- | _ -> assert false)
- with _ ->
- anomaly ("Cannot find definition of constant "^
- (string_of_id (id_of_label (con_label sp))))
- )
- |_ -> assert false
-
-let type_of_const t =
- match (kind_of_term t) with
- Const sp -> Typeops.type_of_constant (Global.env()) sp
- |_ -> assert false
-
-let arg_type t =
- match kind_of_term (def_of_const t) with
- Lambda(a,b,c) -> b
- | _ -> assert false;;
-
-let evaluable_of_global_reference r =
- match r with
- ConstRef sp -> EvalConstRef sp
- | VarRef id -> EvalVarRef id
- | _ -> assert false;;
-
-
-let rank_for_arg_list h =
- let predicate a b =
- try List.for_all2 eq_constr a b with
- Invalid_argument _ -> false in
- let rec rank_aux i = function
- | [] -> None
- | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in
- rank_aux 0;;
-
-let rec check_not_nested f t =
- match kind_of_term t with
- | App(g, _) when eq_constr f g ->
- errorlabstrm "recdef" (str "Nested recursive function are not allowed with Function")
- | Var(_) when eq_constr t f -> errorlabstrm "recdef" (str "Nested recursive function are not allowed with Function")
- | _ -> iter_constr (check_not_nested f) t
-
-
-
-
-let rec (find_call_occs : int -> int -> constr -> constr ->
- (constr list -> constr) * constr list list) =
- fun nb_arg nb_lam f expr ->
- match (kind_of_term expr) with
- App (g, args) when eq_constr g f ->
- if Array.length args <> nb_arg then errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function");
- Array.iter (check_not_nested f) args;
- (fun l -> List.hd l), [Array.to_list args]
- | App (g, args) ->
- let (largs: constr list) = Array.to_list args in
- let rec find_aux = function
- [] -> (fun x -> []), []
- | a::upper_tl ->
- (match find_aux upper_tl with
- (cf, ((arg1::args) as args_for_upper_tl)) ->
- (match find_call_occs nb_arg nb_lam f a with
- cf2, (_ :: _ as other_args) ->
- let rec avoid_duplicates args =
- match args with
- | [] -> (fun _ -> []), []
- | h::tl ->
- let recomb_tl, args_for_tl =
- avoid_duplicates tl in
- match rank_for_arg_list h args_for_upper_tl with
- | None ->
- (fun l -> List.hd l::recomb_tl(List.tl l)),
- h::args_for_tl
- | Some i ->
- (fun l -> List.nth l (i+List.length args_for_tl)::
- recomb_tl l),
- args_for_tl
- in
- let recombine, other_args' =
- avoid_duplicates other_args in
- let len1 = List.length other_args' in
- (fun l -> cf2 (recombine l)::cf(nthtl(l,len1))),
- other_args'@args_for_upper_tl
- | _, [] -> (fun x -> a::cf x), args_for_upper_tl)
- | _, [] ->
- (match find_call_occs nb_arg nb_lam f a with
- cf, (arg1::args) -> (fun l -> cf l::upper_tl), (arg1::args)
- | _, [] -> (fun x -> a::upper_tl), [])) in
- begin
- match (find_aux largs) with
- cf, [] -> (fun l -> mkApp(g, args)), []
- | cf, args ->
- (fun l -> mkApp (g, Array.of_list (cf l))), args
- end
- | Rel(v) -> if v > nb_lam then error "find_call_occs : Rel" else ((fun l -> expr),[])
- | Var(_) when eq_constr expr f -> errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function")
- | Var(id) -> (fun l -> expr), []
- | Meta(_) -> error "Found a metavariable. Can not treat such a term"
- | Evar(_) -> error "Found an evar. Can not treat such a term"
- | Sort(_) -> (fun l -> expr), []
- | Cast(b,_,_) -> find_call_occs nb_arg nb_lam f b
- | Prod(na,t,b) ->
- error "Found a product. Can not treat such a term"
- | Lambda(na,t,b) ->
- begin
- match find_call_occs nb_arg (succ nb_lam) f b with
- | _, [] -> (* Lambda are authorized as long as they do not contain
- recursives calls *)
- (fun l -> expr),[]
- | _ -> error "Found a lambda which body contains a recursive call. Such terms are not allowed"
- end
- | LetIn(na,v,t,b) ->
- begin
- match find_call_occs nb_arg nb_lam f v, find_call_occs nb_arg (succ nb_lam) f b with
- | (_,[]),(_,[]) ->
- ((fun l -> expr), [])
- | (_,[]),(cf,(_::_ as l)) ->
- ((fun l -> mkLetIn(na,v,t,cf l)),l)
- | (cf,(_::_ as l)),(_,[]) ->
- ((fun l -> mkLetIn(na,cf l,t,b)), l)
- | _ -> error "Found a letin with recursive calls in both variable value and body. Such terms are not allowed."
- end
- | Const(_) -> (fun l -> expr), []
- | Ind(_) -> (fun l -> expr), []
- | Construct (_, _) -> (fun l -> expr), []
- | Case(i,t,a,r) ->
- (match find_call_occs nb_arg nb_lam f a with
- cf, (arg1::args) -> (fun l -> mkCase(i, t, (cf l), r)),(arg1::args)
- | _ -> (fun l -> expr),[])
- | Fix(_) -> error "Found a local fixpoint. Can not treat such a term"
- | CoFix(_) -> error "Found a local cofixpoint : CoFix";;
+(* The boolean value is_mes expresses that the termination is expressed
+ using a measure function instead of a well-founded relation. *)
+let tclUSER tac is_mes l g =
+ let clear_tac =
+ match l with
+ | None -> h_clear false []
+ | Some l -> tclMAP (fun id -> tclTRY (h_clear false [id])) (List.rev l)
+ in
+ tclTHENSEQ
+ [
+ clear_tac;
+ if is_mes
+ then tclTHENLIST
+ [
+ unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference
+ (delayed_force Indfun_common.ltof_ref))];
+ tac
+ ]
+ else tac
+ ]
+ g
-let coq_constant s =
- Coqlib.gen_constant_in_modules "RecursiveDefinition"
- (Coqlib.init_modules @ Coqlib.arith_modules) s;;
+let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
+ if is_mes
+ then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof))
+ else tclUSER concl_tac is_mes names_to_suppress
-let coq_base_constant s =
- Coqlib.gen_constant_in_modules "RecursiveDefinition"
- (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
-let constant sl s =
- constr_of_global
- (locate (make_qualid(Names.make_dirpath
- (List.map id_of_string (List.rev sl)))
- (id_of_string s)));;
-let find_reference sl s =
- (locate (make_qualid(Names.make_dirpath
- (List.map id_of_string (List.rev sl)))
- (id_of_string s)));;
+
-let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
-let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm")
+(* Travelling term.
+ Both definitions of [f_terminate] and [f_equation] use the same generic
+ travelling mechanism.
+*)
+
+(* [check_not_nested forbidden e] checks that [e] does not contains any variable
+ of [forbidden]
+*)
+let check_not_nested forbidden e =
+ let rec check_not_nested e =
+ match kind_of_term e with
+ | Rel _ -> ()
+ | Var x -> if List.mem x (forbidden) then error ("check_not_nested : failure "^string_of_id x)
+ | Meta _ | Evar _ | Sort _ -> ()
+ | Cast(e,_,t) -> check_not_nested e;check_not_nested t
+ | Prod(_,t,b) -> check_not_nested t;check_not_nested b
+ | Lambda(_,t,b) -> check_not_nested t;check_not_nested b
+ | LetIn(_,v,t,b) -> check_not_nested t;check_not_nested b;check_not_nested v
+ | App(f,l) -> check_not_nested f;Array.iter check_not_nested l
+ | Const _ -> ()
+ | Ind _ -> ()
+ | Construct _ -> ()
+ | Case(_,t,e,a) ->
+ check_not_nested t;check_not_nested e;Array.iter check_not_nested a
+ | Fix _ -> error "check_not_nested : Fix"
+ | CoFix _ -> error "check_not_nested : Fix"
+ in
+ try
+ check_not_nested e
+ with UserError(_,p) ->
+ errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
+
+(* ['a info] contains the local information for travelling *)
+type 'a infos =
+ { nb_arg : int; (* function number of arguments *)
+ concl_tac : tactic; (* final tactic to finish proofs *)
+ rec_arg_id : identifier; (*name of the declared recursive argument *)
+ is_mes : bool; (* type of recursion *)
+ ih : identifier; (* induction hypothesis name *)
+ f_id : identifier; (* function name *)
+ f_constr : constr; (* function term *)
+ f_terminate : constr; (* termination proof term *)
+ func : global_reference; (* functionnal reference *)
+ info : 'a;
+ is_main_branch : bool; (* on the main branch or on a matched expression *)
+ is_final : bool; (* final first order term or not *)
+ values_and_bounds : (identifier*identifier) list;
+ eqs : identifier list;
+ forbidden_ids : identifier list;
+ acc_inv : constr lazy_t;
+ acc_id : identifier;
+ args_assoc : ((constr list)*constr) list;
+ }
+
+
+type ('a,'b) journey_info_tac =
+ 'a -> (* the arguments of the constructor *)
+ 'b infos -> (* infos of the caller *)
+ ('b infos -> tactic) -> (* the continuation tactic of the caller *)
+ 'b infos -> (* argument of the tactic *)
+ tactic
+
+(* journey_info : specifies the actions to do on the different term constructors during the travelling of the term
+*)
+type journey_info =
+ { letiN : ((name*constr*types*constr),constr) journey_info_tac;
+ lambdA : ((name*types*constr),constr) journey_info_tac;
+ casE : ((constr infos -> tactic) -> constr infos -> tactic) ->
+ ((case_info * constr * constr * constr array),constr) journey_info_tac;
+ otherS : (unit,constr) journey_info_tac;
+ apP : (constr*(constr list),constr) journey_info_tac;
+ app_reC : (constr*(constr list),constr) journey_info_tac;
+ message : string
+ }
+
+
+
+let rec add_vars forbidden e =
+ match kind_of_term e with
+ | Var x -> x::forbidden
+ | _ -> fold_constr add_vars forbidden e
+
+
+let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
+ fun g ->
+ let rev_context,b = decompose_lam_n nb_lam e in
+ let ids = List.fold_left (fun acc (na,_) ->
+ let pre_id =
+ match na with
+ | Name x -> x
+ | Anonymous -> ano_id
+ in
+ pre_id::acc
+ ) [] rev_context in
+ let rev_ids = pf_get_new_ids (List.rev ids) g in
+ let new_b = substl (List.map mkVar rev_ids) b in
+ tclTHENSEQ
+ [
+ h_intros (List.rev rev_ids);
+ intro_using teq_id;
+ onLastHypId (fun heq ->
+ tclTHENSEQ[
+ thin to_intros;
+ h_intros to_intros;
+ (fun g' ->
+ let ty_teq = pf_type_of g' (mkVar heq) in
+ let teq_lhs,teq_rhs =
+ let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g' ++ fnl () ++ pr_id heq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
+ args.(1),args.(2)
+ in
+ let new_b' = Termops.replace_term teq_lhs teq_rhs new_b in
+ let new_infos = {
+ infos with
+ info = new_b';
+ eqs = heq::infos.eqs;
+ forbidden_ids =
+ if forbid_new_ids
+ then add_vars infos.forbidden_ids new_b'
+ else infos.forbidden_ids
+ } in
+ finalize_tac new_infos g'
+ )
+ ]
+ )
+ ] g
-let le_trans = function () -> (coq_base_constant "le_trans")
-let le_lt_trans = function () -> (coq_base_constant "le_lt_trans")
-let lt_S_n = function () -> (coq_base_constant "lt_S_n")
-let le_n = function () -> (coq_base_constant "le_n")
-let refl_equal = function () -> (coq_base_constant "eq_refl")
-let eq = function () -> (coq_base_constant "eq")
-let ex = function () -> (coq_base_constant "ex")
-let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
-let coq_sig = function () -> (coq_base_constant "sig")
-let coq_O = function () -> (coq_base_constant "O")
-let coq_S = function () -> (coq_base_constant "S")
+let rec travel_aux jinfo continuation_tac (expr_info:constr infos) =
+ match kind_of_term expr_info.info with
+ | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint"
+ | LetIn(na,b,t,e) ->
+ begin
+ let new_continuation_tac =
+ jinfo.letiN (na,b,t,e) expr_info continuation_tac
+ in
+ travel jinfo new_continuation_tac
+ {expr_info with info = b; is_final=false}
+ end
+ | Rel _ -> anomaly "Free var in goal conclusion !"
+ | Prod _ ->
+ begin
+ try
+ check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+ jinfo.otherS () expr_info continuation_tac expr_info
+ with _ ->
+ errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+ end
+ | Lambda(n,t,b) ->
+ begin
+ try
+ check_not_nested (expr_info.f_id::expr_info.forbidden_ids) expr_info.info;
+ jinfo.otherS () expr_info continuation_tac expr_info
+ with _ ->
+ errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id)
+ end
+ | Case(ci,t,a,l) ->
+ begin
+ let continuation_tac_a =
+ jinfo.casE
+ (travel jinfo) (ci,t,a,l)
+ expr_info continuation_tac in
+ travel
+ jinfo continuation_tac_a
+ {expr_info with info = a; is_main_branch = false;
+ is_final = false}
+ end
+ | App _ ->
+ let f,args = decompose_app expr_info.info in
+ if eq_constr f (expr_info.f_constr)
+ then jinfo.app_reC (f,args) expr_info continuation_tac expr_info
+ else
+ begin
+ match kind_of_term f with
+ | App _ -> assert false (* f is coming from a decompose_app *)
+ | Const _ | Construct _ | Rel _ | Evar _ | Meta _ | Ind _
+ | Sort _ | Prod _ | Var _ ->
+ let new_infos = {expr_info with info=(f,args)} in
+ let new_continuation_tac =
+ jinfo.apP (f,args) expr_info continuation_tac in
+ travel_args jinfo
+ expr_info.is_main_branch new_continuation_tac new_infos
+ | _ -> assert false
+ end
+ | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t}
+ | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ ->
+ let new_continuation_tac =
+ jinfo.otherS () expr_info continuation_tac in
+ new_continuation_tac expr_info
+and travel_args jinfo is_final continuation_tac infos =
+ let (f_args',args) = infos.info in
+ match args with
+ | [] ->
+ continuation_tac {infos with info = f_args'; is_final = is_final}
+ | arg::args' ->
+ let new_continuation_tac new_infos =
+ let new_arg = new_infos.info in
+ travel_args jinfo is_final
+ continuation_tac
+ {new_infos with info = (mkApp(f_args',[|new_arg|]),args')}
+ in
+ travel jinfo new_continuation_tac
+ {infos with info=arg;is_final=false}
+and travel jinfo continuation_tac expr_info =
+ observe_tac
+ (str jinfo.message ++ Printer.pr_lconstr expr_info.info)
+ (travel_aux jinfo continuation_tac expr_info)
-let gt_antirefl = function () -> (coq_constant "gt_irrefl")
-let lt_n_O = function () -> (coq_base_constant "lt_n_O")
-let lt_n_Sn = function () -> (coq_base_constant "lt_n_Sn")
+(* Termination proof *)
-let f_equal = function () -> (coq_constant "f_equal")
-let well_founded_induction = function () -> (coq_constant "well_founded_induction")
-let well_founded = function () -> (coq_constant "well_founded")
-let acc_rel = function () -> (coq_constant "Acc")
-let acc_inv_id = function () -> (coq_constant "Acc_inv")
-let well_founded_ltof = function () -> (Coqlib.coq_constant "" ["Arith";"Wf_nat"] "well_founded_ltof")
-let iter_ref = function () -> (try find_reference ["Recdef"] "iter" with Not_found -> error "module Recdef not loaded")
-let max_ref = function () -> (find_reference ["Recdef"] "max")
-let iter = function () -> (constr_of_global (delayed_force iter_ref))
-let max_constr = function () -> (constr_of_global (delayed_force max_ref))
+let rec prove_lt hyple g =
+ begin
+ try
+ let (_,args) = decompose_app (pf_concl g) in
+ let x = try destVar (List.hd args) with _ -> assert false in
+ let z = try destVar (List.hd (List.tl args)) with _ -> assert false in
+ let h =
+ List.find (fun id ->
+ let _,args' = decompose_app (pf_type_of g (mkVar id)) in
+ try x = destVar (List.hd args')
+ with _ -> false
+ ) hyple
+ in
+ let y =
+ List.hd (List.tl (snd (decompose_app (pf_type_of g (mkVar h))))) in
+ tclTHENLIST[
+ apply (mkApp(le_lt_trans (),[|mkVar x;y;mkVar z;mkVar h|]));
+ observe_tac (str "prove_lt") (prove_lt hyple)
+ ]
+ with Not_found ->
+ (
+ (
+ tclTHENLIST[
+ apply (delayed_force lt_S_n);
+ (observe_tac (str "assumption: " ++ Printer.pr_goal g) (h_assumption))
+ ])
+ )
+ end
+ g
-let ltof_ref = function () -> (find_reference ["Coq";"Arith";"Wf_nat"] "ltof")
-let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
+let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
+ match lbounds with
+ | [] ->
+ let ids = pf_ids_of_hyps g in
+ let s_max = mkApp(delayed_force coq_S, [|bound|]) in
+ let k = next_ident_away_in_goal k_id ids in
+ let ids = k::ids in
+ let h' = next_ident_away_in_goal (h'_id) ids in
+ let ids = h'::ids in
+ let def = next_ident_away_in_goal def_id ids in
+ tclTHENLIST[
+ split (ImplicitBindings [s_max]);
+ intro_then
+ (fun id ->
+ observe_tac (str "destruct_bounds_aux")
+ (tclTHENS (simplest_case (mkVar id))
+ [
+ tclTHENLIST[intro_using h_id;
+ simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]));
+ default_full_auto];
+ tclTHENLIST[
+ observe_tac (str "clearing k ") (clear [id]);
+ h_intros [k;h';def];
+ observe_tac (str "simple_iter") (simpl_iter onConcl);
+ observe_tac (str "unfold functional")
+ (unfold_in_concl[((true,[1]),
+ evaluable_of_global_reference infos.func)]);
+ observe_tac (str "test" ) (
+ tclTHENLIST[
+ list_rewrite true
+ (List.fold_right
+ (fun e acc -> (mkVar e,true)::acc)
+ infos.eqs
+ (List.map (fun e -> (e,true)) rechyps)
+ );
+ (* list_rewrite true *)
+ (* (List.map (fun e -> (mkVar e,true)) infos.eqs) *)
+ (* ; *)
+
+ (observe_tac (str "finishing")
+ (tclORELSE
+ h_reflexivity
+ (observe_tac (str "calling prove_lt") (prove_lt hyple))))])
+ ]
+ ]
+ ))
+ ] g
+ | (_,v_bound)::l ->
+ tclTHENLIST[
+ simplest_elim (mkVar v_bound);
+ h_clear false [v_bound];
+ tclDO 2 intro;
+ onNthHypId 1
+ (fun p_hyp ->
+ (onNthHypId 2
+ (fun p ->
+ tclTHENLIST[
+ simplest_elim
+ (mkApp(delayed_force max_constr, [| bound; mkVar p|]));
+ tclDO 3 intro;
+ onNLastHypsId 3 (fun lids ->
+ match lids with
+ [hle2;hle1;pmax] ->
+ destruct_bounds_aux infos
+ ((mkVar pmax),
+ hle1::hle2::hyple,(mkVar p_hyp)::rechyps)
+ l
+ | _ -> assert false) ;
+ ]
+ )
+ )
+ )
+ ] g
+
+let destruct_bounds infos =
+ destruct_bounds_aux infos (delayed_force coq_O,[],[]) infos.values_and_bounds
+
+let terminate_app f_and_args expr_info continuation_tac infos =
+ if expr_info.is_final && expr_info.is_main_branch
+ then
+ tclTHENLIST[
+ continuation_tac infos;
+ observe_tac (str "first split")
+ (split (ImplicitBindings [infos.info]));
+ observe_tac (str "destruct_bounds (1)") (destruct_bounds infos)
+ ]
+ else continuation_tac infos
+
+let terminate_others _ expr_info continuation_tac infos =
+ if expr_info.is_final && expr_info.is_main_branch
+ then
+ tclTHENLIST[
+ continuation_tac infos;
+ observe_tac (str "first split")
+ (split (ImplicitBindings [infos.info]));
+ observe_tac (str "destruct_bounds") (destruct_bounds infos)
+ ]
+ else continuation_tac infos
+
+let terminate_letin (na,b,t,e) expr_info continuation_tac info =
+ let new_e = subst1 info.info e in
+ let new_forbidden =
+ let forbid =
+ try
+ check_not_nested (expr_info.f_id::expr_info.forbidden_ids) b;
+ true
+ with _ -> false
+ in
+ if forbid
+ then
+ match na with
+ | Anonymous -> info.forbidden_ids
+ | Name id -> id::info.forbidden_ids
+ else info.forbidden_ids
+ in
+ continuation_tac {info with info = new_e; forbidden_ids = new_forbidden}
-(* These are specific to experiments in nat with lt as well_founded_relation, *)
-(* but this should be made more general. *)
-let nat = function () -> (coq_base_constant "nat")
-let lt = function () -> (coq_base_constant "lt")
-(* This is simply an implementation of the case_eq tactic. this code
- should be replaced with the tactic defined in Ltac in Init/Tactics.v *)
-let mkCaseEq a : tactic =
- (fun g ->
- let type_of_a = pf_type_of g a in
- tclTHENLIST
- [h_generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])];
- (fun g2 ->
- change_in_concl None
- (pattern_occs [((false,[1]), a)] (pf_env g2) Evd.empty (pf_concl g2))
- g2);
- simplest_case a] g);;
(* This is like the previous one except that it also rewrite on all
hypotheses except the ones given in the first argument. All the
@@ -354,7 +678,7 @@ let mkDestructEq :
id) hyps in
let to_revert_constr = List.rev_map mkVar to_revert in
let type_of_expr = pf_type_of g expr in
- let new_hyps = mkApp(delayed_force refl_equal, [|type_of_expr; expr|])::
+ let new_hyps = mkApp(Lazy.force refl_equal, [|type_of_expr; expr|])::
to_revert_constr in
tclTHENLIST
[h_generalize new_hyps;
@@ -363,354 +687,330 @@ let mkDestructEq :
(pattern_occs [((false,[1]), expr)] (pf_env g2) Evd.empty (pf_concl g2)) g2);
simplest_case expr], to_revert
-let rec mk_intros_and_continue thin_intros (extra_eqn:bool)
- cont_function (eqs:constr list) nb_lam (expr:constr) g =
- observe_tac "mk_intros_and_continue" (
- let finalize () = if extra_eqn then
- let teq = pf_get_new_id teq_id g in
- tclTHENLIST
- [ h_intro teq;
- thin thin_intros;
- h_intros thin_intros;
-
- tclMAP
- (fun eq -> tclTRY (Equality.general_rewrite_in true Termops.all_occurrences true (* deps proofs also: *) true teq eq false))
- (List.rev eqs);
- (fun g1 ->
- let ty_teq = pf_type_of g1 (mkVar teq) in
- let teq_lhs,teq_rhs =
- let _,args = try destApp ty_teq with _ -> Pp.msgnl (Printer.pr_goal g1 ++ fnl () ++ pr_id teq ++ str ":" ++ Printer.pr_lconstr ty_teq); assert false in
- args.(1),args.(2)
- in
- cont_function (mkVar teq::eqs) (Termops.replace_term teq_lhs teq_rhs expr) g1
- )
- ]
-
- else
- tclTHENSEQ[
- thin thin_intros;
- h_intros thin_intros;
- cont_function eqs expr
- ]
- in
- if nb_lam = 0
- then finalize ()
- else
- match kind_of_term expr with
- | Lambda (n, _, b) ->
- let n1 =
- match n with
- Name x -> x
- | Anonymous -> ano_id
- in
- let new_n = pf_get_new_id n1 g in
- tclTHEN (h_intro new_n)
- (mk_intros_and_continue thin_intros extra_eqn cont_function eqs
- (pred nb_lam) (subst1 (mkVar new_n) b))
- | _ ->
- assert false) g
-(* finalize () *)
-let const_of_ref = function
- ConstRef kn -> kn
- | _ -> anomaly "ConstRef expected"
-
-let simpl_iter clause =
- reduce
- (Lazy
- {rBeta=true;rIota=true;rZeta= true; rDelta=false;
- rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]})
-(* (Simpl (Some ([],mkConst (const_of_ref (delayed_force iter_ref))))) *)
- clause
-(* The boolean value is_mes expresses that the termination is expressed
- using a measure function instead of a well-founded relation. *)
-let tclUSER tac is_mes l g =
- let clear_tac =
- match l with
- | None -> h_clear true []
- | Some l -> tclMAP (fun id -> tclTRY (h_clear false [id])) (List.rev l)
+let terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos g =
+ let b =
+ try
+ check_not_nested (expr_info.f_id::expr_info.forbidden_ids) a;
+ false
+ with _ ->
+ true
in
- tclTHENSEQ
- [
- clear_tac;
- if is_mes
- then tclTHEN
- (unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference
- (delayed_force ltof_ref))])
- tac
- else tac
- ]
+ let a' = infos.info in
+ let new_info =
+ {infos with
+ info = mkCase(ci,t,a',l);
+ is_main_branch = expr_info.is_main_branch;
+ is_final = expr_info.is_final} in
+ let destruct_tac,rev_to_thin_intro =
+ mkDestructEq [expr_info.rec_arg_id] a' g in
+ let to_thin_intro = List.rev rev_to_thin_intro in
+ observe_tac (str "treating case " ++ int (Array.length l) ++ spc () ++ Printer.pr_lconstr a')
+ (try
+ (tclTHENS
+ destruct_tac
+ (list_map_i (fun i e -> observe_tac (str "do treat case") (treat_case b to_thin_intro (next_step continuation_tac) ci.ci_cstr_ndecls.(i) e new_info)) 0 (Array.to_list l)
+ ))
+ with
+ | UserError("Refiner.thensn_tac3",_)
+ | UserError("Refiner.tclFAIL_s",_) ->
+ (observe_tac (str "is computable " ++ Printer.pr_lconstr new_info.info) (next_step continuation_tac {new_info with info = nf_betaiotazeta new_info.info} )
+ ))
g
+
+let terminate_app_rec (f,args) expr_info continuation_tac _ =
+ List.iter (check_not_nested (expr_info.f_id::expr_info.forbidden_ids))
+ args;
+ begin
+ try
+ let v = List.assoc args expr_info.args_assoc in
+ let new_infos = {expr_info with info = v} in
+ tclTHENLIST[
+ continuation_tac new_infos;
+ if expr_info.is_final && expr_info.is_main_branch
+ then
+ tclTHENLIST[
+ observe_tac (str "first split")
+ (split (ImplicitBindings [new_infos.info]));
+ observe_tac (str "destruct_bounds (3)")
+ (destruct_bounds new_infos)
+ ]
+ else
+ tclIDTAC
+ ]
+ with Not_found ->
+ observe_tac (str "terminate_app_rec not found") (tclTHENS
+ (simplest_elim (mkApp(mkVar expr_info.ih,Array.of_list args)))
+ [
+ tclTHENLIST[
+ intro_using rec_res_id;
+ intro;
+ onNthHypId 1
+ (fun v_bound ->
+ (onNthHypId 2
+ (fun v ->
+ let new_infos = { expr_info with
+ info = (mkVar v);
+ values_and_bounds =
+ (v,v_bound)::expr_info.values_and_bounds;
+ args_assoc=(args,mkVar v)::expr_info.args_assoc
+ } in
+ tclTHENLIST[
+ continuation_tac new_infos;
+ if expr_info.is_final && expr_info.is_main_branch
+ then
+ tclTHENLIST[
+ observe_tac (str "first split")
+ (split (ImplicitBindings [new_infos.info]));
+ observe_tac (str "destruct_bounds (2)")
+ (destruct_bounds new_infos)
+ ]
+ else
+ tclIDTAC
+ ]
+ )
+ )
+ )
+ ];
+ observe_tac (str "proving decreasing") (
+ tclTHENS (* proof of args < formal args *)
+ (apply (Lazy.force expr_info.acc_inv))
+ [
+ observe_tac (str "h_assumption") h_assumption;
+ tclTHENLIST
+ [
+ tclTRY(list_rewrite true
+ (List.map
+ (fun e -> mkVar e,true)
+ expr_info.eqs
+ )
+ );
+ tclUSER expr_info.concl_tac true
+ (Some (
+ expr_info.ih::expr_info.acc_id::
+ (fun (x,y) -> y)
+ (List.split expr_info.values_and_bounds)
+ )
+ );
+ ]
+ ])
+ ])
+ end
+let terminate_info =
+ { message = "prove_terminate with term ";
+ letiN = terminate_letin;
+ lambdA = (fun _ _ _ _ -> assert false);
+ casE = terminate_case;
+ otherS = terminate_others;
+ apP = terminate_app;
+ app_reC = terminate_app_rec;
+ }
-let list_rewrite (rev:bool) (eqs: constr list) =
- tclREPEAT
- (List.fold_right
- (fun eq i -> tclORELSE (rewriteLR eq) i)
- (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
-
-let base_leaf_terminate (func:global_reference) eqs expr =
-(* let _ = msgnl (str "entering base_leaf") in *)
- (fun g ->
- let k',h =
- match pf_get_new_ids [k_id;h_id] g with
- [k';h] -> k',h
- | _ -> assert false
- in
- tclTHENLIST
- [observe_tac "first split" (split (ImplicitBindings [expr]));
- observe_tac "second split"
- (split (ImplicitBindings [delayed_force coq_O]));
- observe_tac "intro k" (h_intro k');
- observe_tac "case on k"
- (tclTHENS (simplest_case (mkVar k'))
- [(tclTHEN (h_intro h)
- (tclTHEN (simplest_elim (mkApp (delayed_force gt_antirefl,
- [| delayed_force coq_O |])))
- default_auto)); tclIDTAC ]);
- intros;
- simpl_iter onConcl;
- unfold_constr func;
- list_rewrite true eqs;
- default_auto] g);;
-
-(* La fonction est donnee en premier argument a la
- fonctionnelle suivie d'autres Lambdas et de Case ...
- Pour recuperer la fonction f a partir de la
- fonctionnelle *)
-
-let get_f foncl =
- match (kind_of_term (def_of_const foncl)) with
- Lambda (Name f, _, _) -> f
- |_ -> error "la fonctionnelle est mal definie";;
-
-
-let rec compute_le_proofs = function
- [] -> assumption
- | a::tl ->
- tclORELSE assumption
- (tclTHENS
- (fun g ->
- let le_trans = delayed_force le_trans in
- let t_le_trans = compute_renamed_type g le_trans in
- let m_id =
- let _,_,t = destProd t_le_trans in
- let na,_,_ = destProd t in
- Nameops.out_name na
- in
- apply_with_bindings
- (le_trans,
- ExplicitBindings[dummy_loc,NamedHyp m_id,a])
- g)
- [compute_le_proofs tl;
- tclORELSE (apply (delayed_force le_n)) assumption])
-
-let make_lt_proof pmax le_proof =
- tclTHENS
- (fun g ->
- let le_lt_trans = delayed_force le_lt_trans in
- let t_le_lt_trans = compute_renamed_type g le_lt_trans in
- let m_id =
- let _,_,t = destProd t_le_lt_trans in
- let na,_,_ = destProd t in
- Nameops.out_name na
- in
- apply_with_bindings
- (le_lt_trans,
- ExplicitBindings[dummy_loc,NamedHyp m_id, pmax]) g)
- [observe_tac "compute_le_proofs" (compute_le_proofs le_proof);
- tclTHENLIST[observe_tac "lt_S_n" (apply (delayed_force lt_S_n)); default_full_auto]];;
-
-let rec list_cond_rewrite k def pmax cond_eqs le_proofs =
- match cond_eqs with
- [] -> tclIDTAC
- | eq::eqs ->
- (fun g ->
- let t_eq = compute_renamed_type g (mkVar eq) in
- let k_id,def_id =
- let k_na,_,t = destProd t_eq in
- let _,_,t = destProd t in
- let def_na,_,_ = destProd t in
- Nameops.out_name k_na,Nameops.out_name def_na
- in
- tclTHENS
- (general_rewrite_bindings false Termops.all_occurrences
- (* dep proofs also: *) true true
- (mkVar eq,
- ExplicitBindings[dummy_loc, NamedHyp k_id, mkVar k;
- dummy_loc, NamedHyp def_id, mkVar def]) false)
- [list_cond_rewrite k def pmax eqs le_proofs;
- observe_tac "make_lt_proof" (make_lt_proof pmax le_proofs)] g
- )
+let prove_terminate = travel terminate_info
-let rec introduce_all_equalities func eqs values specs bound le_proofs
- cond_eqs =
- match specs with
- [] ->
- fun g ->
- let ids = pf_ids_of_hyps g in
- let s_max = mkApp(delayed_force coq_S, [|bound|]) in
- let k = next_ident_away_in_goal k_id ids in
- let ids = k::ids in
- let h' = next_ident_away_in_goal (h'_id) ids in
- let ids = h'::ids in
- let def = next_ident_away_in_goal def_id ids in
- tclTHENLIST
- [observe_tac "introduce_all_equalities_final split" (split (ImplicitBindings [s_max]));
- observe_tac "introduce_all_equalities_final intro k" (h_intro k);
- tclTHENS
- (observe_tac "introduce_all_equalities_final case k" (simplest_case (mkVar k)))
- [
- tclTHENLIST[h_intro h';
- simplest_elim(mkApp(delayed_force lt_n_O,[|s_max|]));
- default_full_auto];
- tclIDTAC
- ];
- observe_tac "clearing k " (clear [k]);
- observe_tac "intros k h' def" (h_intros [k;h';def]);
- observe_tac "simple_iter" (simpl_iter onConcl);
- observe_tac "unfold functional"
- (unfold_in_concl[((true,[1]),evaluable_of_global_reference func)]);
- observe_tac "rewriting equations"
- (list_rewrite true eqs);
- observe_tac ("cond rewrite "^(string_of_id k)) (list_cond_rewrite k def bound cond_eqs le_proofs);
- observe_tac "refl equal" (apply (delayed_force refl_equal))] g
- | spec1::specs ->
- fun g ->
- let ids = Termops.ids_of_named_context (pf_hyps g) in
- let p = next_ident_away_in_goal p_id ids in
- let ids = p::ids in
- let pmax = next_ident_away_in_goal pmax_id ids in
- let ids = pmax::ids in
- let hle1 = next_ident_away_in_goal hle_id ids in
- let ids = hle1::ids in
- let hle2 = next_ident_away_in_goal hle_id ids in
- let ids = hle2::ids in
- let heq = next_ident_away_in_goal heq_id ids in
- tclTHENLIST
- [simplest_elim (mkVar spec1);
- list_rewrite true eqs;
- h_intros [p; heq];
- simplest_elim (mkApp(delayed_force max_constr, [| bound; mkVar p|]));
- h_intros [pmax; hle1; hle2];
- introduce_all_equalities func eqs values specs
- (mkVar pmax) ((mkVar pmax)::le_proofs)
- (heq::cond_eqs)] g;;
-
-let string_match s =
- if String.length s < 3 then failwith "string_match";
- try
- for i = 0 to 3 do
- if String.get s i <> String.get "Acc_" i then failwith "string_match"
- done;
- with Invalid_argument _ -> failwith "string_match"
-
-let retrieve_acc_var g =
- (* Julien: I don't like this version .... *)
- let hyps = pf_ids_of_hyps g in
- map_succeed
- (fun id -> string_match (string_of_id id);id)
- hyps
-
-let rec introduce_all_values concl_tac is_mes acc_inv func context_fn
- eqs hrec args values specs =
- (match args with
- [] ->
- tclTHENLIST
- [observe_tac "split" (split(ImplicitBindings
- [context_fn (List.map mkVar (List.rev values))]));
- observe_tac "introduce_all_equalities" (introduce_all_equalities func eqs
- (List.rev values) (List.rev specs) (delayed_force coq_O) [] [])]
- | arg::args ->
- (fun g ->
- let ids = Termops.ids_of_named_context (pf_hyps g) in
- let rec_res = next_ident_away_in_goal rec_res_id ids in
- let ids = rec_res::ids in
- let hspec = next_ident_away_in_goal hspec_id ids in
- let tac =
- observe_tac "introduce_all_values" (
- introduce_all_values concl_tac is_mes acc_inv func context_fn eqs
- hrec args
- (rec_res::values)(hspec::specs)) in
- (tclTHENS
- (observe_tac "elim h_rec"
- (simplest_elim (mkApp(mkVar hrec, Array.of_list arg)))
- )
- [tclTHENLIST [h_intros [rec_res; hspec];
- tac];
- (tclTHENS
- (observe_tac "acc_inv" (apply (Lazy.force acc_inv)))
- [(* tclTHEN (tclTRY(list_rewrite true eqs)) *)
- (observe_tac "h_assumption" h_assumption)
- ;
- tclTHENLIST
- [
- tclTRY(list_rewrite true eqs);
- observe_tac "user proof"
- (fun g ->
- tclUSER
- concl_tac
- is_mes
- (Some (hrec::hspec::(retrieve_acc_var g)@specs))
- g
- )
- ]
- ]
- )
- ]) g)
- )
+(* Equation proof *)
+let equation_case next_step (ci,a,t,l) expr_info continuation_tac infos =
+ terminate_case next_step (ci,a,t,l) expr_info continuation_tac infos
-let rec_leaf_terminate nb_arg f_constr concl_tac is_mes acc_inv hrec (func:global_reference) eqs expr =
- match find_call_occs nb_arg 0 f_constr expr with
- | context_fn, args ->
- observe_tac "introduce_all_values"
- (introduce_all_values concl_tac is_mes acc_inv func context_fn eqs hrec args [] [])
+let rec prove_le g =
+ let x,z =
+ let _,args = decompose_app (pf_concl g) in
+ (List.hd args,List.hd (List.tl args))
+ in
+ tclFIRST[
+ h_assumption;
+ apply (delayed_force le_n);
+ begin
+ try
+ let matching_fun =
+ pf_is_matching g
+ (Pattern.PApp(Pattern.PRef (reference_of_constr (le ())),[|Pattern.PVar (destVar x);Pattern.PMeta None|])) in
+ let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g)
+ in
+ let y =
+ let _,args = decompose_app t in
+ List.hd (List.tl args)
+ in
+ tclTHENLIST[
+ apply(mkApp(le_trans (),[|x;y;z;mkVar h|]));
+ observe_tac (str "prove_le (rec)") (prove_le)
+ ]
+ with Not_found -> tclFAIL 0 (mt())
+ end;
+ ]
+ g
-let proveterminate nb_arg rec_arg_id is_mes acc_inv (hrec:identifier)
- (f_constr:constr) (func:global_reference) base_leaf rec_leaf =
- let rec proveterminate (eqs:constr list) (expr:constr) =
+let rec make_rewrite_list expr_info max = function
+ | [] -> tclIDTAC
+ | (_,p,hp)::l ->
+ observe_tac (str "make_rewrite_list") (tclTHENS
+ (observe_tac (str "rewrite heq on " ++ pr_id p ) (
+ (fun g ->
+ let t_eq = compute_renamed_type g (mkVar hp) in
+ let k,def =
+ let k_na,_,t = destProd t_eq in
+ let _,_,t = destProd t in
+ let def_na,_,_ = destProd t in
+ Nameops.out_name k_na,Nameops.out_name def_na
+ in
+ general_rewrite_bindings false Termops.all_occurrences
+ true (* dep proofs also: *) true
+ (mkVar hp,
+ ExplicitBindings[dummy_loc,NamedHyp def,
+ expr_info.f_constr;dummy_loc,NamedHyp k,
+ (f_S max)]) false g) )
+ )
+ [make_rewrite_list expr_info max l;
+ tclTHENLIST[ (* x < S max proof *)
+ apply (delayed_force le_lt_n_Sm);
+ observe_tac (str "prove_le(2)") prove_le
+ ]
+ ] )
+
+let make_rewrite expr_info l hp max =
+ tclTHENFIRST
+ (observe_tac (str "make_rewrite") (make_rewrite_list expr_info max l))
+ (observe_tac (str "make_rewrite") (tclTHENS
+ (fun g ->
+ let t_eq = compute_renamed_type g (mkVar hp) in
+ let k,def =
+ let k_na,_,t = destProd t_eq in
+ let _,_,t = destProd t in
+ let def_na,_,_ = destProd t in
+ Nameops.out_name k_na,Nameops.out_name def_na
+ in
+ observe_tac (str "general_rewrite_bindings") (general_rewrite_bindings false Termops.all_occurrences
+ true (* dep proofs also: *) true
+ (mkVar hp,
+ ExplicitBindings[dummy_loc,NamedHyp def,
+ expr_info.f_constr;dummy_loc,NamedHyp k,
+ (f_S (f_S max))]) false) g)
+ [observe_tac(str "make_rewrite finalize") (
+ (* tclORELSE( h_reflexivity) *)
+ (tclTHENLIST[
+ simpl_iter onConcl;
+ observe_tac (str "unfold functional")
+ (unfold_in_concl[((true,[1]),
+ evaluable_of_global_reference expr_info.func)]);
+
+ (list_rewrite true
+ (List.map (fun e -> mkVar e,true) expr_info.eqs));
+ (observe_tac (str "h_reflexivity") h_reflexivity)]))
+ ;
+ tclTHENLIST[ (* x < S (S max) proof *)
+ apply (delayed_force le_lt_SS);
+ observe_tac (str "prove_le (3)") prove_le
+ ]
+ ])
+ )
+
+let rec compute_max rew_tac max l =
+ match l with
+ | [] -> rew_tac max
+ | (_,p,_)::l ->
+ tclTHENLIST[
+ simplest_elim
+ (mkApp(delayed_force max_constr, [| max; mkVar p|]));
+ tclDO 3 intro;
+ onNLastHypsId 3 (fun lids ->
+ match lids with
+ | [hle2;hle1;pmax] -> compute_max rew_tac (mkVar pmax) l
+ | _ -> assert false
+ )]
+
+let rec destruct_hex expr_info acc l =
+ match l with
+ | [] ->
+ begin
+ match List.rev acc with
+ | [] -> tclIDTAC
+ | (_,p,hp)::tl ->
+ observe_tac (str "compute max ") (compute_max (make_rewrite expr_info tl hp) (mkVar p) tl)
+ end
+ | (v,hex)::l ->
+ tclTHENLIST[
+ simplest_case (mkVar hex);
+ clear [hex];
+ tclDO 2 intro;
+ onNthHypId 1 (fun hp ->
+ onNthHypId 2 (fun p ->
+ observe_tac
+ (str "destruct_hex after " ++ pr_id hp ++ spc () ++ pr_id p)
+ (destruct_hex expr_info ((v,p,hp)::acc) l)
+ )
+ )
+ ]
+
+let rec intros_values_eq expr_info acc =
+ tclORELSE(
+ tclTHENLIST[
+ tclDO 2 intro;
+ onNthHypId 1 (fun hex ->
+ (onNthHypId 2 (fun v -> intros_values_eq expr_info ((v,hex)::acc)))
+ )
+ ])
+ (tclCOMPLETE (
+ destruct_hex expr_info [] acc
+ ))
+
+let equation_others _ expr_info continuation_tac infos =
+ if expr_info.is_final && expr_info.is_main_branch
+ then
+ tclTHEN
+ (continuation_tac infos)
+ (intros_values_eq expr_info [])
+ else continuation_tac infos
+
+let equation_letin (na,b,t,e) expr_info continuation_tac info =
+ let new_e = subst1 info.info e in
+ continuation_tac {info with info = new_e;}
+
+let equation_app f_and_args expr_info continuation_tac infos =
+ if expr_info.is_final && expr_info.is_main_branch
+ then intros_values_eq expr_info []
+ else continuation_tac infos
+
+let equation_app_rec (f,args) expr_info continuation_tac info =
+ begin
try
- (* let _ = msgnl (str "entering proveterminate") in *)
- let v =
- match (kind_of_term expr) with
- Case (ci, t, a, l) ->
- (match find_call_occs nb_arg 0 f_constr a with
- _,[] ->
- (fun g ->
- let destruct_tac, rev_to_thin_intro =
- mkDestructEq rec_arg_id a g in
- tclTHENS destruct_tac
- (list_map_i
- (fun i -> mk_intros_and_continue
- (List.rev rev_to_thin_intro)
- true
- proveterminate
- eqs
- ci.ci_cstr_ndecls.(i))
- 0 (Array.to_list l)) g)
- | _, _::_ ->
- (match find_call_occs nb_arg 0 f_constr expr with
- _,[] -> observe_tac "base_leaf" (base_leaf func eqs expr)
- | _, _:: _ ->
- observe_tac "rec_leaf"
- (rec_leaf is_mes acc_inv hrec func eqs expr)))
- | _ ->
- (match find_call_occs nb_arg 0 f_constr expr with
- _,[] ->
- (try observe_tac "base_leaf" (base_leaf func eqs expr)
- with e -> (msgerrnl (str "failure in base case");raise e ))
- | _, _::_ ->
- observe_tac "rec_leaf"
- (rec_leaf is_mes acc_inv hrec func eqs expr)) in
- v
- with e -> begin msgerrnl(str "failure in proveterminate"); raise e end
- in
- proveterminate
+ let v = List.assoc args expr_info.args_assoc in
+ let new_infos = {expr_info with info = v} in
+ observe_tac (str "app_rec found") (continuation_tac new_infos)
+ with Not_found ->
+ if expr_info.is_final && expr_info.is_main_branch
+ then
+ tclTHENLIST
+ [ simplest_case (mkApp (expr_info.f_terminate,Array.of_list args));
+ continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc};
+ observe_tac (str "app_rec intros_values_eq") (intros_values_eq expr_info [])
+ ]
+ else
+ tclTHENLIST[
+ simplest_case (mkApp (expr_info.f_terminate,Array.of_list args));
+ observe_tac (str "app_rec not_found") (continuation_tac {expr_info with args_assoc = (args,delayed_force coq_O)::expr_info.args_assoc})
+ ]
+ end
-let hyp_terminates nb_args func =
- let a_arrow_b = arg_type (constr_of_global func) in
+let equation_info =
+ {message = "prove_equation with term ";
+ letiN = (fun _ -> assert false);
+ lambdA = (fun _ _ _ _ -> assert false);
+ casE = equation_case;
+ otherS = equation_others;
+ apP = equation_app;
+ app_reC = equation_app_rec
+}
+
+let prove_eq = travel equation_info
+
+(* wrappers *)
+(* [compute_terminate_type] computes the type of the Definition f_terminate from the type of f_F
+*)
+let compute_terminate_type nb_args func =
+ let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in
let rev_args,b = decompose_prod_n nb_args a_arrow_b in
let left =
mkApp(delayed_force iter,
@@ -740,12 +1040,6 @@ let hyp_terminates nb_args func =
compose_prod rev_args value
-
-let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
- if is_mes
- then tclCOMPLETE (h_simplest_apply (delayed_force well_founded_ltof))
- else tclUSER concl_tac is_mes names_to_suppress
-
let termination_proof_header is_mes input_type ids args_id relation
rec_arg_num rec_arg_id tac wf_tac : tactic =
begin
@@ -777,7 +1071,7 @@ let termination_proof_header is_mes input_type ids args_id relation
(h_intros args_id)
(tclTHENS
(observe_tac
- "first assert"
+ (str "first assert")
(assert_tac
(Name wf_rec_arg)
(mkApp (delayed_force acc_rel,
@@ -789,7 +1083,7 @@ let termination_proof_header is_mes input_type ids args_id relation
(* accesibility proof *)
tclTHENS
(observe_tac
- "second assert"
+ (str "second assert")
(assert_tac
(Name wf_thm)
(mkApp (delayed_force well_founded,[|input_type;relation|]))
@@ -797,26 +1091,26 @@ let termination_proof_header is_mes input_type ids args_id relation
)
[
(* interactive proof that the relation is well_founded *)
- observe_tac "wf_tac" (wf_tac is_mes (Some args_id));
+ observe_tac (str "wf_tac") (wf_tac is_mes (Some args_id));
(* this gives the accessibility argument *)
observe_tac
- "apply wf_thm"
+ (str "apply wf_thm")
(h_simplest_apply (mkApp(mkVar wf_thm,[|mkVar rec_arg_id|]))
)
]
;
(* rest of the proof *)
tclTHENSEQ
- [observe_tac "generalize"
+ [observe_tac (str "generalize")
(onNLastHypsId (nargs+1)
(tclMAP (fun id ->
tclTHEN (h_generalize [mkVar id]) (h_clear false [id]))
))
;
- observe_tac "h_fix" (h_fix (Some hrec) (nargs+1));
+ observe_tac (str "h_fix") (h_fix (Some hrec) (nargs+1));
h_intros args_id;
h_intro wf_rec_arg;
- observe_tac "tac" (tac wf_rec_arg hrec acc_inv)
+ observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
]
]
) g
@@ -828,10 +1122,8 @@ let rec instantiate_lambda t l =
match l with
| [] -> t
| a::l ->
- let (bound_name, _, body) = destLambda t in
+ let (_, _, body) = destLambda t in
instantiate_lambda (subst1 a body) l
-;;
-
let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_arg_num : tactic =
begin
@@ -867,20 +1159,28 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
relation
rec_arg_num
rec_arg_id
- (fun rec_arg_id hrec acc_inv g ->
- (proveterminate
- nb_args
- [rec_arg_id]
- is_mes
- acc_inv
- hrec
- (mkVar f_id)
- func
- base_leaf_terminate
- (rec_leaf_terminate nb_args (mkVar f_id) concl_tac)
- []
- expr
- )
+ (fun rec_arg_id hrec acc_id acc_inv g ->
+ (prove_terminate (fun infos -> tclIDTAC)
+ { is_main_branch = true; (* we are on the main branche (i.e. still on a match ... with .... end *)
+ is_final = true; (* and on leaf (more or less) *)
+ f_terminate = delayed_force coq_O;
+ nb_arg = nb_args;
+ concl_tac = concl_tac;
+ rec_arg_id = rec_arg_id;
+ is_mes = is_mes;
+ ih = hrec;
+ f_id = f_id;
+ f_constr = mkVar f_id;
+ func = func;
+ info = expr;
+ acc_inv = acc_inv;
+ acc_id = acc_id;
+ values_and_bounds = [];
+ eqs = [];
+ forbidden_ids = [];
+ args_assoc = []
+ }
+ )
g
)
(tclUSER_if_not_mes concl_tac)
@@ -931,7 +1231,7 @@ let is_rec_res id =
try
String.sub id_name 0 (String.length rec_res_name) = rec_res_name
with _ -> false
-
+
let clear_goals =
let rec clear_goal t =
match kind_of_term t with
@@ -1013,7 +1313,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
Auto.h_auto None [] (Some []) g
| _ ->
incr h_num;
- (observe_tac "finishing using"
+ (observe_tac (str "finishing using")
(
tclCOMPLETE(
tclFIRST[
@@ -1023,7 +1323,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
Eauto.eauto_with_bases
false
(true,5)
- [Evd.empty,delayed_force refl_equal]
+ [Evd.empty,Lazy.force refl_equal]
[Auto.Hint_db.empty empty_transparent_state false]
]
)
@@ -1068,7 +1368,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
with UserError _ ->
defined ()
-;;
let com_terminate
@@ -1086,11 +1385,11 @@ let com_terminate
let (evmap, env) = Lemmas.get_current_context() in
start_proof thm_name
(Global, Proof Lemma) (Environ.named_context_val env)
- (hyp_terminates nb_args fonctional_ref) hook;
+ (compute_terminate_type nb_args fonctional_ref) hook;
- by (observe_tac "starting_tac" tac_start);
- by (observe_tac "whole_start" (whole_start tac_end nb_args is_mes fonctional_ref
- input_type relation rec_arg_num ))
+ by (observe_tac (str "starting_tac") tac_start);
+ by (observe_tac (str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
+ input_type relation rec_arg_num ))
in
start_proof tclIDTAC tclIDTAC;
try
@@ -1098,7 +1397,6 @@ let com_terminate
open_new_goal start_proof using_lemmas tcc_lemma_ref
(Some tcc_lemma_name)
(new_goal_type);
-
with Failure "empty list of subgoals!" ->
(* a non recursive function declared with measure ! *)
defined ()
@@ -1106,59 +1404,6 @@ let com_terminate
-let ind_of_ref = function
- | IndRef (ind,i) -> (ind,i)
- | _ -> anomaly "IndRef expected"
-
-let (value_f:constr list -> global_reference -> constr) =
- fun al fterm ->
- let d0 = dummy_loc in
- let rev_x_id_l =
- (
- List.fold_left
- (fun x_id_l _ ->
- let x_id = next_ident_away_in_goal x_id x_id_l in
- x_id::x_id_l
- )
- []
- al
- )
- in
- let context = List.map
- (fun (x, c) -> Name x, None, c) (List.combine rev_x_id_l (List.rev al))
- in
- let env = Environ.push_rel_context context (Global.env ()) in
- let glob_body =
- GCases
- (d0,RegularStyle,None,
- [GApp(d0, GRef(d0,fterm), List.rev_map (fun x_id -> GVar(d0, x_id)) rev_x_id_l),
- (Anonymous,None)],
- [d0, [v_id], [PatCstr(d0,(ind_of_ref
- (delayed_force coq_sig_ref),1),
- [PatVar(d0, Name v_id);
- PatVar(d0, Anonymous)],
- Anonymous)],
- GVar(d0,v_id)])
- in
- let body = understand Evd.empty env glob_body in
- it_mkLambda_or_LetIn body context
-
-let (declare_fun : identifier -> logical_kind -> constr -> global_reference) =
- fun f_id kind value ->
- let ce = {const_entry_body = value;
- const_entry_secctx = None;
- const_entry_type = None;
- const_entry_opaque = false } in
- ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
-
-let (declare_f : identifier -> logical_kind -> constr list -> global_reference -> global_reference) =
- fun f_id kind input_type fterm_ref ->
- declare_fun f_id kind (value_f input_type fterm_ref);;
-
-let rec n_x_id ids n =
- if n = 0 then []
- else let x = next_ident_away_in_goal x_id ids in
- x::n_x_id (x::ids) (n-1);;
let start_equation (f:global_reference) (term_f:global_reference)
(cont_tactic:identifier list -> tactic) g =
@@ -1169,181 +1414,10 @@ let start_equation (f:global_reference) (term_f:global_reference)
tclTHENLIST [
h_intros x;
unfold_in_concl [(Termops.all_occurrences, evaluable_of_global_reference f)];
- observe_tac "simplest_case"
+ observe_tac (str "simplest_case")
(simplest_case (mkApp (terminate_constr,
Array.of_list (List.map mkVar x))));
- observe_tac "prove_eq" (cont_tactic x)] g;;
-
-let base_leaf_eq func eqs f_id g =
- let ids = pf_ids_of_hyps g in
- let k = next_ident_away_in_goal k_id ids in
- let p = next_ident_away_in_goal p_id (k::ids) in
- let v = next_ident_away_in_goal v_id (p::k::ids) in
- let heq = next_ident_away_in_goal heq_id (v::p::k::ids) in
- let heq1 = next_ident_away_in_goal heq_id (heq::v::p::k::ids) in
- let hex = next_ident_away_in_goal hex_id (heq1::heq::v::p::k::ids) in
- tclTHENLIST [
- h_intros [v; hex];
- simplest_elim (mkVar hex);
- h_intros [p;heq1];
- tclTRY
- (rewriteRL
- (mkApp(mkVar heq1,
- [|mkApp (delayed_force coq_S, [|mkVar p|]);
- mkApp(delayed_force lt_n_Sn, [|mkVar p|]); f_id|])));
- simpl_iter onConcl;
- tclTRY (unfold_in_concl [((true,[1]), evaluable_of_global_reference func)]);
- observe_tac "list_revrite" (list_rewrite true eqs);
- apply (delayed_force refl_equal)] g;;
-
-let f_S t = mkApp(delayed_force coq_S, [|t|]);;
-
-
-let rec introduce_all_values_eq cont_tac functional termine
- f p heq1 pmax bounds le_proofs eqs ids =
- function
- [] ->
- let heq2 = next_ident_away_in_goal heq_id ids in
- tclTHENLIST
- [pose_proof (Name heq2)
- (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
- simpl_iter (onHyp heq2);
- unfold_in_hyp [((true,[1]), evaluable_of_global_reference
- (global_of_constr functional))]
- (heq2, Termops.InHyp);
- tclTHENS
- (fun gls ->
- let t_eq = compute_renamed_type gls (mkVar heq2) in
- let def_id =
- let _,_,t = destProd t_eq in let def_na,_,_ = destProd t in
- Nameops.out_name def_na
- in
- observe_tac "rewrite heq" (general_rewrite_bindings false Termops.all_occurrences
- true (* dep proofs also: *) true (mkVar heq2,
- ExplicitBindings[dummy_loc,NamedHyp def_id,
- f]) false) gls)
- [tclTHENLIST
- [observe_tac "list_rewrite" (list_rewrite true eqs);
- cont_tac pmax le_proofs];
- tclTHENLIST[apply (delayed_force le_lt_SS);
- compute_le_proofs le_proofs]]]
- | arg::args ->
- let v' = next_ident_away_in_goal v_id ids in
- let ids = v'::ids in
- let hex' = next_ident_away_in_goal hex_id ids in
- let ids = hex'::ids in
- let p' = next_ident_away_in_goal p_id ids in
- let ids = p'::ids in
- let new_pmax = next_ident_away_in_goal pmax_id ids in
- let ids = pmax::ids in
- let hle1 = next_ident_away_in_goal hle_id ids in
- let ids = hle1::ids in
- let hle2 = next_ident_away_in_goal hle_id ids in
- let ids = hle2::ids in
- let heq = next_ident_away_in_goal heq_id ids in
- let ids = heq::ids in
- let heq2 = next_ident_away_in_goal heq_id ids in
- let ids = heq2::ids in
- tclTHENLIST
- [mkCaseEq(mkApp(termine, Array.of_list arg));
- h_intros [v'; hex'];
- simplest_elim(mkVar hex');
- h_intros [p'];
- simplest_elim(mkApp(delayed_force max_constr, [|mkVar pmax;
- mkVar p'|]));
- h_intros [new_pmax;hle1;hle2];
- introduce_all_values_eq
- (fun pmax' le_proofs'->
- tclTHENLIST
- [cont_tac pmax' le_proofs';
- h_intros [heq;heq2];
- observe_tac ("rewriteRL " ^ (string_of_id heq2))
- (tclTRY (rewriteLR (mkVar heq2)));
- tclTRY (tclTHENS
- ( fun g ->
- let t_eq = compute_renamed_type g (mkVar heq) in
- let k_id,def_id =
- let k_na,_,t = destProd t_eq in
- let _,_,t = destProd t in
- let def_na,_,_ = destProd t in
- Nameops.out_name k_na,Nameops.out_name def_na
- in
- let c_b = (mkVar heq,
- ExplicitBindings
- [dummy_loc, NamedHyp k_id,
- f_S(mkVar pmax');
- dummy_loc, NamedHyp def_id, f])
- in
- observe_tac "general_rewrite_bindings" ( (general_rewrite_bindings false Termops.all_occurrences true (* dep proofs also: *) true
- c_b false))
- g
- )
- [tclIDTAC;
- tclTHENLIST
- [apply (delayed_force le_lt_n_Sm);
- compute_le_proofs le_proofs']])])
- functional termine f p heq1 new_pmax
- (p'::bounds)((mkVar pmax)::le_proofs) eqs
- (heq2::heq::hle2::hle1::new_pmax::p'::hex'::v'::ids) args]
-
-
-let rec_leaf_eq termine f ids functional eqs expr fn args =
- let p = next_ident_away_in_goal p_id ids in
- let ids = p::ids in
- let v = next_ident_away_in_goal v_id ids in
- let ids = v::ids in
- let hex = next_ident_away_in_goal hex_id ids in
- let ids = hex::ids in
- let heq1 = next_ident_away_in_goal heq_id ids in
- let ids = heq1::ids in
- let hle1 = next_ident_away_in_goal hle_id ids in
- let ids = hle1::ids in
- tclTHENLIST
- [observe_tac "intros v hex" (h_intros [v;hex]);
- simplest_elim (mkVar hex);
- h_intros [p;heq1];
- h_generalize [mkApp(delayed_force le_n,[|mkVar p|])];
- h_intros [hle1];
- observe_tac "introduce_all_values_eq" (introduce_all_values_eq
- (fun _ _ -> tclIDTAC)
- functional termine f p heq1 p [] [] eqs ids args);
- observe_tac "failing here" (apply (delayed_force refl_equal))]
-
-let rec prove_eq nb_arg (termine:constr) (f:constr)(functional:global_reference)
- (eqs:constr list) (expr:constr) =
-(* tclTRY *)
- observe_tac "prove_eq" (match kind_of_term expr with
- Case(ci,t,a,l) ->
- (match find_call_occs nb_arg 0 f a with
- _,[] ->
- (fun g ->
- let destruct_tac,rev_to_thin_intro = mkDestructEq [] a g in
- tclTHENS
- destruct_tac
- (list_map_i
- (fun i -> mk_intros_and_continue
- (List.rev rev_to_thin_intro) true
- (prove_eq nb_arg termine f functional)
- eqs ci.ci_cstr_ndecls.(i))
- 0 (Array.to_list l)) g)
- | _,_::_ ->
- (match find_call_occs nb_arg 0 f expr with
- _,[] -> observe_tac "base_leaf_eq(1)" (base_leaf_eq functional eqs f)
- | fn,args ->
- fun g ->
- let ids = Termops.ids_of_named_context (pf_hyps g) in
- observe_tac "rec_leaf_eq" (rec_leaf_eq termine f ids
- (constr_of_global functional)
- eqs expr fn args) g))
- | _ ->
- (match find_call_occs nb_arg 0 f expr with
- _,[] -> observe_tac "base_leaf_eq(2)" ( base_leaf_eq functional eqs f)
- | fn,args ->
- fun g ->
- let ids = Termops.ids_of_named_context (pf_hyps g) in
- observe_tac "rec_leaf_eq" (rec_leaf_eq
- termine f ids (constr_of_global functional)
- eqs expr fn args) g));;
+ observe_tac (str "prove_eq") (cont_tactic x)] g;;
let (com_eqn : int -> identifier ->
global_reference -> global_reference -> global_reference
@@ -1355,41 +1429,44 @@ let (com_eqn : int -> identifier ->
| _ -> anomaly "terminate_lemma: not a constant"
in
let (evmap, env) = Lemmas.get_current_context() in
- let f_constr = (constr_of_global f_ref) in
+ let f_constr = constr_of_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
(start_proof eq_name (Global, Proof Lemma)
(Environ.named_context_val env) equation_lemma_type (fun _ _ -> ());
by
(start_equation f_ref terminate_ref
(fun x ->
- prove_eq nb_arg
- (constr_of_global terminate_ref)
- f_constr
- functional_ref
- []
- (instantiate_lambda
- (def_of_const (constr_of_global functional_ref))
- (f_constr::List.map mkVar x)
- )
+ prove_eq (fun _ -> tclIDTAC)
+ {nb_arg=nb_arg;
+ f_terminate = constr_of_global terminate_ref;
+ f_constr = f_constr;
+ concl_tac = tclIDTAC;
+ func=functional_ref;
+ info=(instantiate_lambda
+ (def_of_const (constr_of_global functional_ref))
+ (f_constr::List.map mkVar x)
+ );
+ is_main_branch = true;
+ is_final = true;
+ values_and_bounds = [];
+ eqs = [];
+ forbidden_ids = [];
+ acc_inv = lazy (assert false);
+ acc_id = id_of_string "____";
+ args_assoc = [];
+ f_id = id_of_string "______";
+ rec_arg_id = id_of_string "______";
+ is_mes = false;
+ ih = id_of_string "______";
+ }
)
- );
-(* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
+ );
+ (* (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
(* Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
- Flags.silently (fun () -> Lemmas.save_named opacity) () ;
+ Flags.silently (fun () -> Lemmas.save_named opacity) () ;
(* Pp.msgnl (str "eqn finished"); *)
-
);;
-let nf_zeta env =
- Reductionops.clos_norm_flags (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
- env
- Evd.empty
-
-let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- let clos_norm_flags flgs env sigma t =
- Closure.norm_val (Closure.create_clos_infos flgs env) (Closure.inject (Reductionops.nf_evar sigma t)) in
- clos_norm_flags Closure.betaiotazeta Environ.empty_env Evd.empty
-
let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
generate_induction_principle using_lemmas : unit =
@@ -1430,25 +1507,25 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
let tcc_lemma_name = add_suffix function_name "_tcc" in
let tcc_lemma_constr = ref None in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
- let hook _ _ =
+ let hook _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
let f_ref = declare_f function_name (IsProof Lemma) arg_types term_ref in
let _ = Table.extraction_inline true [Ident (dummy_loc,term_id)] in
-(* message "start second proof"; *)
- let stop = ref false in
- begin
- try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type)
+ (* message "start second proof"; *)
+ let stop =
+ try com_eqn (List.length res_vars) equation_id functional_ref f_ref term_ref (subst_var function_name equation_lemma_type);
+ false
with e ->
begin
- if Tacinterp.get_debug () <> Tactic_debug.DebugOff
+ if do_observe ()
then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
else anomaly "Cannot create equation Lemma"
;
(* ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ()); *)
- stop := true;
+ true
end
- end;
- if not !stop
+ in
+ if not stop
then
let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in
let f_ref = destConst (constr_of_global f_ref)
@@ -1461,9 +1538,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
spc () ++ str"is defined" )++ fnl () ++
h 1 (Ppconstr.pr_id equation_id ++
spc () ++ str"is defined" )
- )
+ )
in
- try
+ try
com_terminate
tcc_lemma_name
tcc_lemma_constr
@@ -1473,7 +1550,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
term_id
using_lemmas
(List.length res_vars)
- hook
+ hook
with e ->
begin
ignore(try Vernacentries.vernac_reset_name (Util.dummy_loc,functional_id) with _ -> ());
@@ -1482,4 +1559,3 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
end
-
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
new file mode 100644
index 000000000..aa4493821
--- /dev/null
+++ b/plugins/funind/recdef.mli
@@ -0,0 +1,20 @@
+
+
+(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
+val tclUSER_if_not_mes :
+ Proof_type.tactic ->
+ bool ->
+ Names.identifier list option ->
+ Proof_type.tactic
+val recursive_definition :
+bool ->
+ Names.identifier ->
+ Constrintern.internalization_env ->
+ Topconstr.constr_expr ->
+ Topconstr.constr_expr ->
+ int -> Topconstr.constr_expr -> (Names.constant ->
+ Term.constr option ref ->
+ Names.constant ->
+ Names.constant -> int -> Term.types -> int -> Term.constr -> 'a) -> Topconstr.constr_expr list -> unit
+
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 19:42:20 +0000