aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/README.md2
-rw-r--r--dev/doc/critical-bugs11
-rw-r--r--doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst3
-rw-r--r--doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst1
-rw-r--r--doc/sphinx/refman-preamble.rst4
-rw-r--r--engine/uState.ml4
-rw-r--r--engine/uState.mli5
-rw-r--r--kernel/environ.ml66
-rw-r--r--kernel/environ.mli16
-rw-r--r--kernel/retypeops.ml1
-rw-r--r--plugins/ltac/g_tactic.mlg6
-rw-r--r--plugins/ltac/tacsubst.ml10
-rw-r--r--pretyping/locusops.ml6
-rw-r--r--pretyping/locusops.mli4
-rw-r--r--test-suite/bugs/closed/bug_10904.v8
-rw-r--r--theories/Logic/ClassicalFacts.v33
16 files changed, 126 insertions, 54 deletions
diff --git a/dev/README.md b/dev/README.md
index 4cda60a703..0c6b8020f1 100644
--- a/dev/README.md
+++ b/dev/README.md
@@ -28,7 +28,7 @@
| [`dev/doc/econstr.md`](doc/econstr.md) | Describes `Econstr`, implementation of treatment of `evar` in the engine |
| [`dev/doc/primproj.md`](doc/primproj.md) | Describes primitive projections |
| [`dev/doc/proof-engine.md`](doc/proof-engine.md) | Tutorial on new proof engine |
-| [`dev/doc/xml-protocol.md`](doc/proof-engine.md) | XML protocol that coqtop and IDEs use to communicate |
+| [`dev/doc/xml-protocol.md`](doc/xml-protocol.md) | XML protocol that coqtop and IDEs use to communicate |
| [`dev/doc/MERGING.md`](doc/MERGING.md) | How pull requests should be merged into `master` |
| [`dev/doc/release-process.md`](doc/release-process.md) | Process of creating a new Coq release |
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 78d7061259..6d90ced12d 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -250,6 +250,17 @@ Conversion machines
exploit: test-suite/bugs/closed/bug_9684.v
GH issue number: #9684
+ component: lazy machine
+ summary: incorrect De Bruijn handling when inferring the relevance mark for a lambda
+ introduced: 2019-03-15, 23f84f37c674a07e925925b7e0d50d7ee8414093 and 71b9ad8526155020c8451dd326a52e391a9a8585, SkySkimmer
+ impacted released versions: 8.10.0
+ impacted coqchk versions: 8.10.0
+ found by: ppedrot investigating unexpected conversion failures with SProp
+ exploit: test-suite/bugs/closed/bug_10904.v
+ GH issue number: #10904
+ risk: none without using -allow-sprop (off by default in 8.10.0),
+ otherwise could be exploited by mistake
+
Conflicts with axioms in library
component: library of real numbers
diff --git a/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst b/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst
new file mode 100644
index 0000000000..6cab6a1c13
--- /dev/null
+++ b/doc/changelog/01-kernel/10904-fix-debruijn-sprop-rel.rst
@@ -0,0 +1,3 @@
+- Fix proof of False when using |SProp| (incorrect De Bruijn handling
+ when inferring the relevance mark of a function) (`#10904
+ <https://github.com/coq/coq/pull/10904>`_, by Pierre-Marie Pédrot).
diff --git a/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst
new file mode 100644
index 0000000000..6e87ff93c7
--- /dev/null
+++ b/doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst
@@ -0,0 +1 @@
+- ClassicalFacts: Adding the standard equivalence between weak excluded-middle and the classical instance of De Morgan's law (`#10895 <https://github.com/coq/coq/pull/10895>`_, by Hugo Herbelin).
diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst
index c662028773..de95eda989 100644
--- a/doc/sphinx/refman-preamble.rst
+++ b/doc/sphinx/refman-preamble.rst
@@ -70,7 +70,11 @@
.. |p_i| replace:: `p`\ :math:`_{i}`
.. |p_n| replace:: `p`\ :math:`_{n}`
.. |Program| replace:: :strong:`Program`
+.. |Prop| replace:: :math:`\Prop`
+.. |SProp| replace:: :math:`\SProp`
+.. |Set| replace:: :math:`\Set`
.. |SSR| replace:: :smallcaps:`SSReflect`
+.. |Type| replace:: :math:`\Type`
.. |t_1| replace:: `t`\ :math:`_{1}`
.. |t_i| replace:: `t`\ :math:`_{i}`
.. |t_m| replace:: `t`\ :math:`_{m}`
diff --git a/engine/uState.ml b/engine/uState.ml
index af714f6282..efced52990 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -520,7 +520,7 @@ let merge ?loc ~sideff rigid uctx ctx' =
let merge_subst uctx s =
{ uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s }
-let demote_seff_univs (univs,_) uctx =
+let demote_seff_univs univs uctx =
let seff = LSet.union uctx.uctx_seff_univs univs in
{ uctx with uctx_seff_univs = seff }
@@ -541,7 +541,7 @@ let merge_seff uctx ctx' =
let emit_side_effects eff u =
let uctxs = Safe_typing.universes_of_private eff in
List.fold_left (fun u uctx ->
- let u = demote_seff_univs uctx u in
+ let u = demote_seff_univs (fst uctx) u in
merge_seff u uctx)
u uctxs
diff --git a/engine/uState.mli b/engine/uState.mli
index 7cb2f49780..23ef84c55d 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -112,6 +112,11 @@ val merge : ?loc:Loc.t -> sideff:bool -> rigid -> t -> Univ.ContextSet.t -> t
val merge_subst : t -> UnivSubst.universe_opt_subst -> t
val emit_side_effects : Safe_typing.private_constants -> t -> t
+val demote_seff_univs : Univ.LSet.t -> t -> t
+(** Mark the universes as not local any more, because they have been
+ globally declared by some side effect. You should be using
+ emit_side_effects instead. *)
+
val new_univ_variable : ?loc:Loc.t -> rigid -> Id.t option -> t -> t * Univ.Level.t
val add_global_univ : t -> Univ.Level.t -> t
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 4a2aeea22d..98d66cafa1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -50,12 +50,19 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
type mind_key = mutual_inductive_body * link_info ref
-type globals = {
- env_constants : constant_key Cmap_env.t;
- env_inductives : mind_key Mindmap_env.t;
- env_modules : module_body MPmap.t;
- env_modtypes : module_type_body MPmap.t;
-}
+module Globals = struct
+
+ type view =
+ { constants : constant_key Cmap_env.t
+ ; inductives : mind_key Mindmap_env.t
+ ; modules : module_body MPmap.t
+ ; modtypes : module_type_body MPmap.t
+ }
+
+ type t = view
+
+ let view x = x
+end
type stratification = {
env_universes : UGraph.t;
@@ -88,7 +95,7 @@ type rel_context_val = {
}
type env = {
- env_globals : globals;
+ env_globals : Globals.t;
env_named_context : named_context_val; (* section variables *)
env_rel_context : rel_context_val;
env_nb_rel : int;
@@ -110,11 +117,12 @@ let empty_rel_context_val = {
}
let empty_env = {
- env_globals = {
- env_constants = Cmap_env.empty;
- env_inductives = Mindmap_env.empty;
- env_modules = MPmap.empty;
- env_modtypes = MPmap.empty};
+ env_globals =
+ { Globals.constants = Cmap_env.empty
+ ; inductives = Mindmap_env.empty
+ ; modules = MPmap.empty
+ ; modtypes = MPmap.empty
+ };
env_named_context = empty_named_context_val;
env_rel_context = empty_rel_context_val;
env_nb_rel = 0;
@@ -215,29 +223,29 @@ let lookup_named_ctxt id ctxt =
fst (Id.Map.find id ctxt.env_named_map)
let fold_constants f env acc =
- Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_constants acc
+ Cmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.constants acc
let fold_inductives f env acc =
- Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.env_inductives acc
+ Mindmap_env.fold (fun c (body,_) acc -> f c body acc) env.env_globals.Globals.inductives acc
(* Global constants *)
let lookup_constant_key kn env =
- Cmap_env.find kn env.env_globals.env_constants
+ Cmap_env.find kn env.env_globals.Globals.constants
let lookup_constant kn env =
- fst (Cmap_env.find kn env.env_globals.env_constants)
+ fst (Cmap_env.find kn env.env_globals.Globals.constants)
(* Mutual Inductives *)
let lookup_mind kn env =
- fst (Mindmap_env.find kn env.env_globals.env_inductives)
+ fst (Mindmap_env.find kn env.env_globals.Globals.inductives)
let mind_context env mind =
let mib = lookup_mind mind env in
Declareops.inductive_polymorphic_context mib
let lookup_mind_key kn env =
- Mindmap_env.find kn env.env_globals.env_inductives
+ Mindmap_env.find kn env.env_globals.Globals.inductives
let oracle env = env.env_typing_flags.conv_oracle
let set_oracle env o =
@@ -468,10 +476,10 @@ let no_link_info = NotLinked
let add_constant_key kn cb linkinfo env =
let new_constants =
- Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.env_constants in
+ Cmap_env.add kn (cb,(ref linkinfo, ref None)) env.env_globals.Globals.constants in
let new_globals =
{ env.env_globals with
- env_constants = new_constants } in
+ Globals.constants = new_constants } in
{ env with env_globals = new_globals }
let add_constant kn cb env =
@@ -598,10 +606,10 @@ let template_polymorphic_pind (ind,u) env =
else template_polymorphic_ind ind env
let add_mind_key kn (_mind, _ as mind_key) env =
- let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
+ let new_inds = Mindmap_env.add kn mind_key env.env_globals.Globals.inductives in
let new_globals =
{ env.env_globals with
- env_inductives = new_inds; } in
+ Globals.inductives = new_inds; } in
{ env with env_globals = new_globals }
let add_mind kn mib env =
@@ -688,22 +696,22 @@ let keep_hyps env needed =
let add_modtype mtb env =
let mp = mtb.mod_mp in
- let new_modtypes = MPmap.add mp mtb env.env_globals.env_modtypes in
- let new_globals = { env.env_globals with env_modtypes = new_modtypes } in
+ let new_modtypes = MPmap.add mp mtb env.env_globals.Globals.modtypes in
+ let new_globals = { env.env_globals with Globals.modtypes = new_modtypes } in
{ env with env_globals = new_globals }
let shallow_add_module mb env =
let mp = mb.mod_mp in
- let new_mods = MPmap.add mp mb env.env_globals.env_modules in
- let new_globals = { env.env_globals with env_modules = new_mods } in
+ let new_mods = MPmap.add mp mb env.env_globals.Globals.modules in
+ let new_globals = { env.env_globals with Globals.modules = new_mods } in
{ env with env_globals = new_globals }
let lookup_module mp env =
- MPmap.find mp env.env_globals.env_modules
+ MPmap.find mp env.env_globals.Globals.modules
-let lookup_modtype mp env =
- MPmap.find mp env.env_globals.env_modtypes
+let lookup_modtype mp env =
+ MPmap.find mp env.env_globals.Globals.modtypes
(*s Judgments. *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f7de98dcfb..5af2a7288b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -46,8 +46,18 @@ type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
type mind_key = mutual_inductive_body * link_info ref
-type globals
-(** globals = constants + projections + inductive types + modules + module-types *)
+module Globals : sig
+ type t
+
+ type view =
+ { constants : constant_key Cmap_env.t
+ ; inductives : mind_key Mindmap_env.t
+ ; modules : module_body MPmap.t
+ ; modtypes : module_type_body MPmap.t
+ }
+
+ val view : t -> view
+end
type stratification = {
env_universes : UGraph.t;
@@ -67,7 +77,7 @@ type rel_context_val = private {
}
type env = private {
- env_globals : globals;
+ env_globals : Globals.t;
env_named_context : named_context_val; (* section variables *)
env_rel_context : rel_context_val;
env_nb_rel : int;
diff --git a/kernel/retypeops.ml b/kernel/retypeops.ml
index a51b762f95..f398e6a5da 100644
--- a/kernel/retypeops.ml
+++ b/kernel/retypeops.ml
@@ -71,6 +71,7 @@ let rec relevance_of_fterm env extra lft f =
| FLambda (len, tys, bdy, e) ->
let extra = List.rev_append (List.map (fun (x,_) -> binder_relevance x) tys) extra in
let lft = Esubst.el_liftn len lft in
+ let e = Esubst.subs_liftn len e in
relevance_of_term_extra env extra lft e bdy
| FLetIn (x, _, _, bdy, e) ->
relevance_of_term_extra env (x.binder_relevance :: extra)
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 9b52b710c1..1b00a93834 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -182,10 +182,6 @@ let mkCLambdaN_simple bl c = match bl with
let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc
-let map_int_or_var f = function
- | ArgArg x -> ArgArg (f x)
- | ArgVar _ as y -> y
-
let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences }
let merge_occurrences loc cl = function
@@ -269,7 +265,7 @@ GRAMMAR EXTEND Gram
[ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl }
| "-"; n = nat_or_var; nl = LIST0 int_or_var ->
(* have used int_or_var instead of nat_or_var for compatibility *)
- { AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) } ] ]
+ { AllOccurrencesBut (List.map (Locusops.or_var_map abs) (n::nl)) } ] ]
;
occs:
[ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ]
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index b6e7dd64b0..bf5d49f678 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -76,25 +76,21 @@ let subst_and_short_name f (c,n) =
(* assert (n=None); *)(* since tacdef are strictly globalized *)
(f c,None)
-let subst_or_var f = let open Locus in function
- | ArgVar _ as x -> x
- | ArgArg x -> ArgArg (f x)
-
let subst_located f = Loc.map f
let subst_reference subst =
- subst_or_var (subst_located (subst_kn subst))
+ Locusops.or_var_map (subst_located (subst_kn subst))
(*CSC: subst_global_reference is used "only" for RefArgType, that propagates
to the syntactic non-terminals "global", used in commands such as
Print. It is also used for non-evaluable references. *)
let subst_global_reference subst =
- subst_or_var (subst_located (subst_global_reference subst))
+ Locusops.or_var_map (subst_located (subst_global_reference subst))
let subst_evaluable subst =
let subst_eval_ref = subst_evaluable_reference subst in
- subst_or_var (subst_and_short_name subst_eval_ref)
+ Locusops.or_var_map (subst_and_short_name subst_eval_ref)
let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 02c8f6a2a8..9c6cf090a2 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -10,6 +10,12 @@
open Locus
+(** Utilities on or_var *)
+
+let or_var_map f = function
+ | ArgArg x -> ArgArg (f x)
+ | ArgVar _ as y -> y
+
(** Utilities on occurrences *)
let occurrences_map f = function
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index 195dbec935..47d2ffe797 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -11,6 +11,10 @@
open Names
open Locus
+(** Utilities on or_var *)
+
+val or_var_map : ('a -> 'b) -> 'a or_var -> 'b or_var
+
(** Utilities on occurrences *)
val occurrences_map :
diff --git a/test-suite/bugs/closed/bug_10904.v b/test-suite/bugs/closed/bug_10904.v
new file mode 100644
index 0000000000..32b25ff726
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10904.v
@@ -0,0 +1,8 @@
+Definition a := fun (P:SProp) (p:P) => p.
+
+Lemma foo : (let k := a in let k' := a in fun (x:nat) y => x) = (let k := a in fun x y => y).
+Proof.
+ Fail reflexivity.
+ match goal with |- ?l = _ => exact_no_check (eq_refl l) end.
+Fail Qed.
+Abort.
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index 2a9e15ab37..8538b54c08 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -29,7 +29,7 @@ Table of contents:
3. Weak classical axioms
-3.1. Weak excluded middle
+3.1. Weak excluded middle and classical de Morgan law
3.2. Gödel-Dummett axiom and right distributivity of implication over
disjunction
@@ -514,7 +514,7 @@ End Weak_proof_irrelevance_CCI.
(** * Weak classical axioms *)
(** We show the following increasing in the strength of axioms:
- - weak excluded-middle
+ - weak excluded-middle and classical De Morgan's law
- right distributivity of implication over disjunction and Gödel-Dummett axiom
- independence of general premises and drinker's paradox
- excluded-middle
@@ -523,11 +523,15 @@ End Weak_proof_irrelevance_CCI.
(** ** Weak excluded-middle *)
(** The weak classical logic based on [~~A \/ ~A] is referred to with
- name KC in [[ChagrovZakharyaschev97]]
+ name KC in [[ChagrovZakharyaschev97]]. See [[SorbiTerwijn11]] for
+ a short survey.
[[ChagrovZakharyaschev97]] Alexander Chagrov and Michael
Zakharyaschev, "Modal Logic", Clarendon Press, 1997.
-*)
+
+ [[SorbiTerwijn11]] Andrea Sorbi and Sebastiaan A. Terwijn,
+ "Generalizations of the weak law of the excluded-middle", Notre
+ Dame J. Formal Logic, vol 56(2), pp 321-331, 2015. *)
Definition weak_excluded_middle :=
forall A:Prop, ~~A \/ ~A.
@@ -539,16 +543,21 @@ Definition weak_excluded_middle :=
Definition weak_generalized_excluded_middle :=
forall A B:Prop, ((A -> B) -> B) \/ (A -> B).
+(** Classical De Morgan's law *)
+
+Definition classical_de_morgan_law :=
+ forall A B:Prop, ~(A /\ B) -> ~A \/ ~B.
+
(** ** Gödel-Dummett axiom *)
(** [(A->B) \/ (B->A)] is studied in [[Dummett59]] and is based on [[Gödel33]].
[[Dummett59]] Michael A. E. Dummett. "A Propositional Calculus
- with a Denumerable Matrix", In the Journal of Symbolic Logic, Vol
- 24 No. 2(1959), pp 97-103.
+ with a Denumerable Matrix", In the Journal of Symbolic Logic, vol
+ 24(2), pp 97-103, 1959.
[[Gödel33]] Kurt Gödel. "Zum intuitionistischen Aussagenkalkül",
- Ergeb. Math. Koll. 4 (1933), pp. 34-38.
+ Ergeb. Math. Koll. 4, pp. 34-38, 1933.
*)
Definition GodelDummett := forall A B:Prop, (A -> B) \/ (B -> A).
@@ -590,6 +599,16 @@ Proof.
right; intro HA; apply (HAnotA HA HA).
Qed.
+(** The weak excluded middle is equivalent to the classical De Morgan's law *)
+
+Lemma weak_excluded_middle_iff_classical_de_morgan_law :
+ weak_excluded_middle <-> classical_de_morgan_law.
+Proof.
+ split; [intro WEM|intro CDML]; intros A *.
+ - destruct (WEM A); tauto.
+ - destruct (CDML A (~A)); tauto.
+Qed.
+
(** ** Independence of general premises and drinker's paradox *)
(** Independence of general premises is the unconstrained, non
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 12:36:00 +0000