summaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/funind/functional_principles_proofs.ml6
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/invfun.ml51
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/recdef.ml4
6 files changed, 35 insertions, 32 deletions
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index b2955e90..51ede26e 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 48205019..b5876ffa 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -188,7 +188,7 @@ let prove_trivial_eq h_id context (constructor,type_of_term,term) =
let find_rectype env c =
- let (t, l) = decompose_app (Reduction.whd_betadeltaiota env c) in
+ let (t, l) = decompose_app (Reduction.whd_betaiotazeta c) in
match kind_of_term t with
| Ind ind -> (t, l)
| Construct _ -> (t,l)
@@ -576,7 +576,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
onLastHypId (fun heq_id -> tclTHENLIST [
(* Then the new hypothesis *)
tclMAP introduction_no_check dyn_infos.rec_hyps;
- (* observe_tac "after_introduction" *)(fun g' ->
+ observe_tac "after_introduction" (fun g' ->
(* We get infos on the equations introduced*)
let new_term_value_eq = pf_type_of g' (mkVar heq_id) in
(* compute the new value of the body *)
@@ -603,7 +603,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
}
in
clean_goal_with_heq ptes_infos continue_tac new_infos g'
- )])
+ )])
]
g
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 6b6e4838..ffaa2208 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 7b5dd763..c770c7ce 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -72,10 +72,14 @@ let do_observe_tac s tac g =
raise reraise;;
-let observe_tac s tac g =
- if do_observe ()
- then do_observe_tac (str s) tac g
+
+let observe_tac_msg s tac g =
+ if do_observe ()
+ then do_observe_tac s tac g
else tac g
+
+let observe_tac s tac g =
+ observe_tac_msg (str s) tac g
(* [nf_zeta] $\zeta$-normalization of a term *)
let nf_zeta =
@@ -287,33 +291,33 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
branches
in
(* before building the full intro pattern for the principle *)
- let pat = Some (dummy_loc,Genarg.IntroOrAndPattern intro_pats) in
let eq_ind = Coqlib.build_coq_eq () in
let eq_construct = mkConstruct((destInd eq_ind),1) in
(* The next to referencies will be used to find out which constructor to apply in each branch *)
let ind_number = ref 0
and min_constr_number = ref 0 in
(* The tactic to prove the ith branch of the principle *)
+ let this_branche_ids empty add i =
+ List.fold_right
+ (fun (_,pat) acc ->
+ match pat with
+ | Genarg.IntroIdentifier id -> add id acc
+ | _ -> anomaly "Not an identifier"
+ )
+ (List.nth intro_pats (pred i))
+ empty
+ in
let prove_branche i g =
(* We get the identifiers of this branch *)
- let this_branche_ids =
- List.fold_right
- (fun (_,pat) acc ->
- match pat with
- | Genarg.IntroIdentifier id -> Idset.add id acc
- | _ -> anomaly "Not an identifier"
- )
- (List.nth intro_pats (pred i))
- Idset.empty
- in
(* and get the real args of the branch by unfolding the defined constant *)
let pre_args,pre_tac =
List.fold_right
(fun (id,b,t) (pre_args,pre_tac) ->
- if Idset.mem id this_branche_ids
+ if Idset.mem id (this_branche_ids Idset.empty Idset.add i)
then
match b with
- | None -> (id::pre_args,pre_tac)
+ | None ->
+ (id::pre_args,pre_tac)
| Some b ->
(pre_args,
tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac
@@ -347,8 +351,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
when
(eq_constr eq eq_ind) &&
array_exists (eq_constr graph') graphs_constr ->
- ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
- ::args.(2)::acc)
+ ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
+ ::args.(2)::acc)
| _ -> mkVar hid :: acc
end
| _ -> mkVar hid :: acc
@@ -390,7 +394,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
| [res;hres] -> res,hres
| _ -> assert false
in
- observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor);
+ observe_tac_msg (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor)
(
tclTHENSEQ
[
@@ -455,11 +459,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
fun g ->
observe
(pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings));
- functional_induction false (applist(funs_constr.(i),List.map mkVar args_names))
- (Some (mkVar principle_id,bindings))
- pat g
+ h_apply false false [dummy_loc,(mkVar principle_id,bindings)] g
))
- (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
+ (fun i g -> observe_tac ("proving branche "^string_of_int i)
+ (tclTHEN (tclMAP h_intro (this_branche_ids [] (fun a b -> a::b) i)) (prove_branche i)) g )
]
g
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index bd1a1710..e1f10be2 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9853fd73..a33ae1d6 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -913,7 +913,7 @@ let build_and_l l =
| App(_,_) ->
let (f,_) = decompose_app t in
eq_constr f (well_founded ())
- | _ -> assert false
+ | _ -> false
in
let compare t1 t2 =
let b1,b2= is_well_founded t1,is_well_founded t2 in
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-13 23:52:36 +0000