diff options
| -rw-r--r-- | dev/README.md | 2 | ||||
| -rw-r--r-- | doc/changelog/10-standard-library/10895-master+weak-excluded-middle-de-morgan.rst | 1 | ||||
| -rw-r--r-- | kernel/environ.ml | 66 | ||||
| -rw-r--r-- | kernel/environ.mli | 16 | ||||
| -rw-r--r-- | theories/Logic/ClassicalFacts.v | 33 |
5 files changed, 78 insertions, 40 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/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/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/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 |