aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/funind
diff options
context:
space:
mode:
authorGravatar Julien Forest <forest@ensiie.fr>2017-03-31 19:48:03 +0200
committerGravatar Julien Forest <forest@ensiie.fr>2017-04-04 17:41:32 +0200
commit043c3907f9ed23ae9b9642d2cbb651f6a29737bd (patch)
treecbfe95dd6ec16893db15da44c8bad1634b73e3f3 /plugins/funind
parent59f5391576aca91400f506adfc7f1a1965f79069 (diff)
Solving first problem in bug #4306. TO DO : solve the let in problem
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml11
-rw-r--r--plugins/funind/functional_principles_proofs.mli2
-rw-r--r--plugins/funind/indfun_common.ml6
-rw-r--r--plugins/funind/indfun_common.mli7
-rw-r--r--plugins/funind/recdef.ml8
-rw-r--r--plugins/funind/recdef.mli2
6 files changed, 25 insertions, 11 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 0bbe4bb4c..85084badd 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1388,8 +1388,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let prove_with_tcc tcc_lemma_constr eqs : tactic =
match !tcc_lemma_constr with
- | None -> anomaly (Pp.str "No tcc proof !!")
- | Some lemma ->
+ | Undefined -> anomaly (Pp.str "No tcc proof !!")
+ | Value lemma ->
fun gls ->
(* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *)
(* let ids = hid::pf_ids_of_hyps gls in *)
@@ -1407,7 +1407,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
Proofview.V82.of_tactic (Eauto.gen_eauto (false,5) [] (Some []))
]
gls
-
+ | Not_needed -> tclIDTAC
let backtrack_eqs_until_hrec hrec eqs : tactic =
fun gls ->
@@ -1586,8 +1586,9 @@ let prove_principle_for_gen
let args_ids = List.map (fun decl -> Nameops.out_name (get_name decl)) princ_info.args in
let lemma =
match !tcc_lemma_ref with
- | None -> error "No tcc proof !!"
- | Some lemma -> lemma
+ | Undefined -> error "No tcc proof !!"
+ | Value lemma -> lemma
+ | Not_needed -> Coqlib.build_coq_True ()
in
(* let rec list_diff del_list check_list = *)
(* match del_list with *)
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 34ce66967..e11cd9eac 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -9,7 +9,7 @@ val prove_princ_for_struct :
val prove_principle_for_gen :
constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *)
- constr option ref -> (* a pointer to the obligation proofs lemma *)
+ Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *)
bool -> (* is that function uses measure *)
int -> (* the number of recursive argument *)
types -> (* the type of the recursive argument *)
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f56e92414..8419f1d8f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -506,3 +506,9 @@ let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
(List.fold_right
(fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
(if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));;
+
+
+type tcc_lemma_value =
+ | Undefined
+ | Value of Constr.constr
+ | Not_needed
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e5c756f56..83cadf5f5 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -114,3 +114,10 @@ val acc_rel : Term.constr Util.delayed
val well_founded : Term.constr Util.delayed
val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic
+
+
+
+type tcc_lemma_value =
+ | Undefined
+ | Value of Constr.constr
+ | Not_needed
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index fa84e4ddf..7ff31f112 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -41,7 +41,7 @@ open Eauto
open Indfun_common
open Sigma.Notations
open Context.Rel.Declaration
-
+
(* Ugly things which should not be here *)
@@ -1296,7 +1296,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
| _ -> anomaly ~label:"equation_lemma" (Pp.str "not a constant")
in
let lemma = mkConst (Names.Constant.make1 (Lib.make_kn na)) in
- ref_ := Some lemma ;
+ ref_ := Value lemma ;
let lid = ref [] in
let h_num = ref (-1) in
let env = Global.env () in
@@ -1412,6 +1412,7 @@ let com_terminate
(new_goal_type);
with Failure "empty list of subgoals!" ->
(* a non recursive function declared with measure ! *)
+ tcc_lemma_ref := Not_needed;
defined ()
@@ -1484,7 +1485,6 @@ let (com_eqn : int -> Id.t ->
(* Pp.msgnl (str "eqn finished"); *)
);;
-
let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num eq
generate_induction_principle using_lemmas : unit =
let env = Global.env() in
@@ -1524,7 +1524,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
in
let evm = Evd.from_ctx evuctx in
let tcc_lemma_name = add_suffix function_name "_tcc" in
- let tcc_lemma_constr = ref None in
+ let tcc_lemma_constr = ref Undefined in
(* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
let hook _ _ =
let term_ref = Nametab.locate (qualid_of_ident term_id) in
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index f60eedbe6..c84c736b8 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -13,7 +13,7 @@ bool ->
Constrexpr.constr_expr ->
Constrexpr.constr_expr ->
int -> Constrexpr.constr_expr -> (Term.pconstant ->
- Term.constr option ref ->
+ Indfun_common.tcc_lemma_value ref ->
Term.pconstant ->
Term.pconstant -> int -> Term.types -> int -> Term.constr -> 'a) -> Constrexpr.constr_expr list -> unit