Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

- Use oracle transparent state everywhere during unification, properly

honoring the [Opaque] flag.
- In btauto/Algebra, this breaks a script relying on unfolding of decide
during apply, where decide was declared opaque.
Same in QArith/Qcanon with Qed.
  • Loading branch information...
commit eabf7f599c7b73fe8bdbbad1570270d31c9bee12 1 parent 56d3576
@mattam82 mattam82 authored
View
29 plugins/btauto/Algebra.v
@@ -13,6 +13,30 @@ Hint Extern 5 => progress bool.
Ltac define t x H :=
set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x.
+Lemma Decidable_sound : forall P (H : Decidable P),
+ decide P = true -> P.
+Proof.
+intros P H Hp; apply -> Decidable_spec; assumption.
+Qed.
+
+Lemma Decidable_complete : forall P (H : Decidable P),
+ P -> decide P = true.
+Proof.
+intros P H Hp; apply <- Decidable_spec; assumption.
+Qed.
+
+Lemma Decidable_sound_alt : forall P (H : Decidable P),
+ ~ P -> decide P = false.
+Proof.
+intros P [wit spec] Hd; simpl; destruct wit; tauto.
+Qed.
+
+Lemma Decidable_complete_alt : forall P (H : Decidable P),
+ decide P = false -> ~ P.
+Proof.
+intros P [wit spec] Hd Hc; simpl in *; intuition congruence.
+Qed.
+
Ltac try_rewrite :=
repeat match goal with
| [ H : ?P |- _ ] => rewrite H
@@ -142,6 +166,7 @@ end.
Program Instance Decidable_eq_poly : forall (p q : poly), Decidable (eq p q) := {
Decidable_witness := beq_poly p q
}.
+
Next Obligation.
split.
revert q; induction p; intros [] ?; simpl in *; bool; try_decide;
@@ -185,8 +210,8 @@ Program Instance Decidable_valid : forall n p, Decidable (valid n p) := {
}.
Next Obligation.
split.
- revert n; induction p; simpl in *; intuition; bool; try_decide; auto.
- intros H; induction H; simpl in *; bool; try_decide; auto.
+ revert n; induction p; unfold valid_dec in *; intuition; bool; try_decide; auto.
+ intros H; induction H; unfold valid_dec in *; bool; try_decide; auto.
Qed.
(** Basic algebra *)
View
2  plugins/decl_mode/decl_proof_instr.ml
@@ -357,7 +357,7 @@ let find_subsubgoal c ctyp skip submetas gls =
try
let unifier =
Unification.w_unify env se.se_evd Reduction.CUMUL
- ~flags:Unification.elim_flags ctyp se.se_type in
+ ~flags:(Unification.elim_flags ()) ctyp se.se_type in
if n <= 0 then
{se with
se_evd=meta_assign se.se_meta
View
41 pretyping/unification.ml
@@ -251,11 +251,12 @@ type unify_flags = {
(* Default flag for unifying a type against a type (e.g. apply) *)
(* We set all conversion flags (no flag should be modified anymore) *)
-let default_unify_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
+let default_unify_flags () =
+ let ts = Conv_oracle.get_transp_state () in
+ { modulo_conv_on_closed_terms = Some ts;
use_metas_eagerly_in_conv_on_closed_terms = true;
- modulo_delta = full_transparent_state;
- modulo_delta_types = full_transparent_state;
+ modulo_delta = ts;
+ modulo_delta_types = ts;
modulo_delta_in_merge = None;
check_applied_meta_types = true;
resolve_evars = false;
@@ -279,7 +280,7 @@ let set_merge_flags flags =
(* type against a type (e.g. apply) *)
(* We set only the flags available at the time the new "apply" extends *)
(* out of "simple apply" *)
-let default_no_delta_unify_flags = { default_unify_flags with
+let default_no_delta_unify_flags () = { (default_unify_flags ()) with
modulo_delta = empty_transparent_state;
check_applied_meta_types = false;
use_pattern_unification = false;
@@ -292,13 +293,13 @@ let default_no_delta_unify_flags = { default_unify_flags with
(* allow_K) because only closed terms are involved in *)
(* induction/destruct/case/elim and w_unify_to_subterm_list does not *)
(* call w_unify for induction/destruct/case/elim (13/6/2011) *)
-let elim_flags = { default_unify_flags with
+let elim_flags () = { (default_unify_flags ()) with
restrict_conv_on_strict_subterms = false; (* ? *)
modulo_betaiota = false;
allow_K_in_toplevel_higher_order_unification = true
}
-let elim_no_delta_flags = { elim_flags with
+let elim_no_delta_flags () = { (elim_flags ()) with
modulo_delta = empty_transparent_state;
check_applied_meta_types = false;
use_pattern_unification = false;
@@ -326,11 +327,9 @@ let subterm_restriction is_subterm flags =
let key_of b flags f =
if subterm_restriction b flags then None else
match kind_of_term f with
- | Const (cst,u) when is_transparent (ConstKey cst) &&
- Cpred.mem cst (snd flags.modulo_delta) ->
+ | Const (cst,u) when Cpred.mem cst (snd flags.modulo_delta) ->
Some (ConstKey (cst,u))
- | Var id when is_transparent (VarKey id) &&
- Id.Pred.mem id (fst flags.modulo_delta) ->
+ | Var id when Id.Pred.mem id (fst flags.modulo_delta) ->
Some (VarKey id)
| _ -> None
@@ -338,7 +337,7 @@ let translate_key = function
| ConstKey (cst,u) -> ConstKey cst
| VarKey id -> VarKey id
| RelKey n -> RelKey n
-
+
let oracle_order env cf1 cf2 =
match cf1 with
| None ->
@@ -368,14 +367,14 @@ let isAllowedEvar flags c = match kind_of_term c with
| Evar (evk,_) -> not (ExistentialSet.mem evk flags.frozen_evars)
| _ -> false
-let check_compatibility env (sigma,metasubst,evarsubst) tyM tyN =
+let check_compatibility env flags (sigma,metasubst,evarsubst) tyM tyN =
match subst_defined_metas metasubst tyM with
| None -> ()
| Some m ->
match subst_defined_metas metasubst tyN with
| None -> ()
| Some n ->
- if not (is_trans_fconv CONV full_transparent_state env sigma m n)
+ if not (is_trans_fconv CONV flags.modulo_delta env sigma m n)
&& is_ground_term sigma m && is_ground_term sigma n
then
error_cannot_unify env sigma (m,n)
@@ -391,7 +390,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
if wt && flags.check_applied_meta_types then
(let tyM = Typing.meta_type sigma k1 in
let tyN = Typing.meta_type sigma k2 in
- check_compatibility curenv substn tyM tyN);
+ check_compatibility curenv flags substn tyM tyN);
if k2 < k1 then sigma,(k1,cN,stN)::metasubst,evarsubst
else sigma,(k2,cM,stM)::metasubst,evarsubst
| Meta k, _
@@ -399,7 +398,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
if wt && flags.check_applied_meta_types then
(let tyM = Typing.meta_type sigma k in
let tyN = get_type_of curenv sigma cN in
- check_compatibility curenv substn tyM tyN);
+ check_compatibility curenv flags substn tyM tyN);
(* Here we check that [cN] does not contain any local variables *)
if Int.equal nb 0 then
sigma,(k,cN,snd (extract_instance_status pb))::metasubst,evarsubst
@@ -413,7 +412,7 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
if wt && flags.check_applied_meta_types then
(let tyM = get_type_of curenv sigma cM in
let tyN = Typing.meta_type sigma k in
- check_compatibility curenv substn tyM tyN);
+ check_compatibility curenv flags substn tyM tyN);
(* Here we check that [cM] does not contain any local variables *)
if Int.equal nb 0 then
(sigma,(k,cM,fst (extract_instance_status pb))::metasubst,evarsubst)
@@ -969,7 +968,7 @@ let w_merge env with_types flags (evd,metas,evars) =
(* merge constraints *)
w_merge_rec evd (order_metas metas) evars []
-let w_unify_meta_types env ?(flags=default_unify_flags) evd =
+let w_unify_meta_types env ?(flags=default_unify_flags ()) evd =
let metas,evd = retract_coercible_metas evd in
w_merge env true flags (evd,metas,[])
@@ -1043,7 +1042,7 @@ let iter_fail f a =
(* Tries to find an instance of term [cl] in term [op].
Unifies [cl] to every subterm of [op] until it finds a match.
Fails if no match is found *)
-let w_unify_to_subterm env evd ?(flags=default_unify_flags) (op,cl) =
+let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
let rec matchrec cl =
let cl = strip_outer_cast cl in
(try
@@ -1103,7 +1102,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags) (op,cl) =
(* Tries to find all instances of term [cl] in term [op].
Unifies [cl] to every subterm of [op] and return all the matches.
Fails if no match is found *)
-let w_unify_to_subterm_all env evd ?(flags=default_unify_flags) (op,cl) =
+let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
let return a b =
let (evd,c as a) = a () in
if List.exists (fun (evd',c') -> eq_constr c c') b then b else a :: b
@@ -1248,7 +1247,7 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
Before, second-order was used if the type of Meta(1) and [x:A]t was
convertible and first-order otherwise. But if failed if e.g. the type of
Meta(1) had meta-variables in it. *)
-let w_unify env evd cv_pb ?(flags=default_unify_flags) ty1 ty2 =
+let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
let hd1,l1 = whd_nored_stack evd ty1 in
let hd2,l2 = whd_nored_stack evd ty2 in
let is_empty1 = match l1 with [] -> true | _ -> false in
View
8 pretyping/unification.mli
@@ -27,11 +27,11 @@ type unify_flags = {
allow_K_in_toplevel_higher_order_unification : bool
}
-val default_unify_flags : unify_flags
-val default_no_delta_unify_flags : unify_flags
+val default_unify_flags : unit -> unify_flags
+val default_no_delta_unify_flags : unit -> unify_flags
-val elim_flags : unify_flags
-val elim_no_delta_flags : unify_flags
+val elim_flags : unit -> unify_flags
+val elim_no_delta_flags : unit -> unify_flags
(** The "unique" unification fonction *)
val w_unify :
View
12 proofs/clenv.ml
@@ -278,14 +278,14 @@ let clenv_dependent ce = clenv_dependent_gen false ce
(******************************************************************)
-let clenv_unify ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
+let clenv_unify ?(flags=default_unify_flags ()) cv_pb t1 t2 clenv =
{ clenv with
evd = w_unify ~flags clenv.env clenv.evd cv_pb t1 t2 }
-let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
+let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
{ clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
-let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl =
+let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
let concl = Goal.V82.concl clenv.evd (sig_it gl) in
if isMeta (fst (whd_nored_stack clenv.evd clenv.templtyp.rebus)) then
clenv_unify CUMUL ~flags (clenv_type clenv) concl
@@ -370,11 +370,11 @@ let connect_clenv gls clenv =
In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
*)
-let fchain_flags =
- { default_unify_flags with
+let fchain_flags () =
+ { (default_unify_flags ()) with
allow_K_in_toplevel_higher_order_unification = true }
-let clenv_fchain ?(flags=fchain_flags) mv clenv nextclenv =
+let clenv_fchain ?(flags=fchain_flags ()) mv clenv nextclenv =
(* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
let clenv' =
{ templval = clenv.templval;
View
6 proofs/clenvtac.ml
@@ -76,14 +76,14 @@ open Unification
let dft = default_unify_flags
-let res_pf clenv ?(with_evars=false) ?(flags=dft) gls =
+let res_pf clenv ?(with_evars=false) ?(flags=dft ()) gls =
clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls
let elim_res_pf_THEN_i clenv tac gls =
- let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in
+ let clenv' = (clenv_unique_resolver ~flags:(elim_flags ()) clenv gls) in
tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
-let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
+let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:(dft ())
(* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
View
2  tactics/leminv.ml
@@ -270,7 +270,7 @@ let lemInv id c gls =
try
let clause = mk_clenv_type_of gls c in
let clause = clenv_constrain_last_binding (mkVar id) clause in
- Clenvtac.res_pf clause ~flags:Unification.elim_flags gls
+ Clenvtac.res_pf clause ~flags:(Unification.elim_flags ()) gls
with
| NoSuchBinding ->
errorlabstrm ""
View
5 tactics/rewrite.ml4
@@ -1076,7 +1076,8 @@ module Strategies =
error "fold: the term is not unfoldable !"
in
try
- let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
+ let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ())
+ unfolded t in
let c' = Evarutil.nf_evar sigma c in
Some (Some { rew_car = ty; rew_from = t; rew_to = c';
rew_prf = RewCast DEFAULTcast;
@@ -1093,7 +1094,7 @@ module Strategies =
error "fold: the term is not unfoldable !"
in
try
- let sigma = Unification.w_unify env sigma CONV ~flags:Unification.elim_flags unfolded t in
+ let sigma = Unification.w_unify env sigma CONV ~flags:(Unification.elim_flags ()) unfolded t in
let c' = Evarutil.nf_evar sigma c in
Some (Some { rew_car = ty; rew_from = t; rew_to = c';
rew_prf = RewCast DEFAULTcast;
View
2  tactics/tacticals.ml
@@ -285,7 +285,7 @@ let general_elim_then_using mk_elim
match predicate with
| None -> elimclause'
| Some p ->
- clenv_unify ~flags:Unification.elim_flags
+ clenv_unify ~flags:(Unification.elim_flags ())
Reduction.CONV (mkMeta pmv) p elimclause'
in
elim_res_pf_THEN_i elimclause' branchtacs gl
View
22 tactics/tactics.ml
@@ -757,7 +757,7 @@ let index_of_ind_arg t =
| None -> error "Could not find inductive argument of elimination scheme."
in aux None 0 t
-let elimination_clause_scheme with_evars ?(flags=elim_flags) i elimclause indclause gl =
+let elimination_clause_scheme with_evars ?(flags=elim_flags ()) i elimclause indclause gl =
let indmv =
(match kind_of_term (nth_arg i elimclause.templval.rebus) with
| Meta mv -> mv
@@ -875,13 +875,13 @@ let simplest_elim c = default_elim false (c,NoBindings)
(e.g. it could replace id:A->B->C by id:C, knowing A/\B)
*)
-let clenv_fchain_in id ?(flags=elim_flags) mv elimclause hypclause =
+let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
try clenv_fchain ~flags mv elimclause hypclause
with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
(* Set the hypothesis name in the message *)
raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
-let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause indclause gl =
+let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id i elimclause indclause gl =
let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
let hypmv =
try match List.remove indmv (clenv_independent elimclause) with
@@ -976,7 +976,7 @@ let descend_in_conjunctions tac exit c gl =
let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
let flags =
- if with_delta then default_unify_flags else default_no_delta_unify_flags in
+ if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
(* The actual type of the theorem. It will be matched against the
goal. If this fails, then the head constant will be unfolded step by
step. *)
@@ -1070,7 +1070,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
let apply_in_once sidecond_first with_delta with_destruct with_evars id
(loc,(d,lbind)) gl0 =
- let flags = if with_delta then elim_flags else elim_no_delta_flags in
+ let flags = if with_delta then elim_flags () else elim_no_delta_flags () in
let t' = pf_get_hyp_typ gl0 id in
let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
let rec aux with_destruct c gl =
@@ -1187,7 +1187,7 @@ let specialize mopt (c,lbind) g =
tclEVARS evd, nf_evar evd c
else
let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
- let flags = { default_unify_flags with resolve_evars = true } in
+ let flags = { (default_unify_flags ()) with resolve_evars = true } in
let clause = clenv_unify_meta_types ~flags clause in
let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
let nargs = List.length tstack in
@@ -2985,7 +2985,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
(* elimclause' is built from elimclause by instanciating all args and params. *)
let elimclause' = recolle_clenv nparams indvars elimclause gl in
(* one last resolution (useless?) *)
- let resolved = clenv_unique_resolver ~flags:elim_flags elimclause' gl in
+ let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in
clenv_refine with_evars resolved gl
(* Apply induction "in place" replacing the hypothesis on which
@@ -3319,9 +3319,9 @@ let elim_scheme_type elim t gl =
| Meta mv ->
let clause' =
(* t is inductive, then CUMUL or CONV is irrelevant *)
- clenv_unify ~flags:elim_flags Reduction.CUMUL t
+ clenv_unify ~flags:(elim_flags ()) Reduction.CUMUL t
(clenv_meta_type clause mv) clause in
- res_pf clause' ~flags:elim_flags gl
+ res_pf clause' ~flags:(elim_flags ()) gl
| _ -> anomaly (Pp.str "elim_scheme_type")
let elim_type t gl =
@@ -3639,10 +3639,10 @@ let admit_as_an_axiom gl =
List.rev (Array.to_list (instance_from_named_context sign)))))
gl
-let unify ?(state=full_transparent_state) x y gl =
+let unify ?(state=Conv_oracle.get_transp_state ()) x y gl =
try
let flags =
- {default_unify_flags with
+ {(default_unify_flags ()) with
modulo_delta = state;
modulo_conv_on_closed_terms = Some state}
in
View
4 theories/QArith/Qcanon.v
@@ -460,13 +460,13 @@ Proof.
induction n; simpl; auto with qarith.
rewrite IHn; auto with qarith.
Qed.
-
+Transparent Qred.
Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0.
Proof.
destruct n; simpl.
destruct 1; auto.
intros.
- now apply Qc_is_canon.
+ now apply Qc_is_canon.
Qed.
Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n.
Please sign in to comment.
Something went wrong with that request. Please try again.