Merge remote-tracking branch 'kirst/coq-8.20' into rocq-9.0

merges #9

Author: JoJoDeveloping

README.md

@@ -12,6 +12,7 @@ The FOL library currently extends this core with the following content:
 - [Incompleteness](theories/Incompleteness): An abstract and synthetic version of the first incompleteness theorem, instantiated to Robinson's Q, as well as a proof of the first incompleteness theorem and Tarski's theorem via Carnap's diagonal lemma.
 - [Tennenbaum](theories/Tennenbaum): Tennenbaum's theorem stating that the natural numbers are the only computable model of PA, constructivised.
 - [ArithmeticalHierachy](theories/ArithmeticalHierarchy): Semantic and syntactic characterisations of the arithmetical hierarchy and an equivalence proof.
+- [ModelTheory](theories/ModelTheory): Results on model theory, so far focused on the (downwards) Löwenheim-Skolem theorem
 - [Proofmode](theories/Proofmode): A tool easing derivations in a deduction system, including a HOAS input language hiding de Bruijn encoded syntax.
 - [Reification](theories/Reification): A tactic automating representability proofs of Coq predicates as first-order formulas.
 - [Utils](theories/Utils): A collection of additional results needed in various projects.
@@ -24,6 +25,7 @@ The FOL library currently extends this core with the following content:
 This library is available in opam. To install it, you can use the following commands:
 
 ```
+<<<<<<< HEAD
 opam switch create coq-library-fol --packages=ocaml-variants.4.14.1+options,ocaml-option-flambda
 eval $(opam env)
 opam repo add coq-released https://coq.inria.fr/opam/released
@@ -63,6 +65,7 @@ We are open to contributions! To contribute, fork the project on GitHub, add a n
 - Gert Smolka
 - Dominik Wehr
 - Janis Bailitis
+- Haoyi Zeng
 
 ## Publications
 
@@ -78,10 +81,14 @@ We are open to contributions! To contribute, fork the project on GitHub, add a n
 - An Analysis of Tennenbaum's Theorem in Constructive Type Theory. Marc Hermes, Dominik Kirst. FSCD'22.
 - Gödel's Theorem Without Tears: Essential Incompleteness in Synthetic Computability. Dominik Kirst, Benjamin Peters. CSL'23.
 - Synthetic Undecidability and Incompleteness of First-Order Axiom Systems in Coq. Dominik Kirst, Marc Hermes. JAR'23.
+- The Kleene-Post and Post's Theorem in the Calculus of Inductive Constructions. Yannick Forster, Dominik Kirst, Niklas Mück. CSL'24.
+- An Analysis of Tennenbaum's Theorem in Constructive Type Theory (Extended Version). Marc Hermes, Dominik Kirst. LMCS'24.
+- The Blurred Drinker Paradox: Constructive Reverse Mathematics of the Downward Löwenheim-Skolem Theorem. Dominik Kirst, Haoyi Zeng. LICS'25.
 
 ### Workshop Abstracts
 
 - A Toolbox for Mechanised First-Order Logic. Johannes Hostert, Mark Koch, Dominik Kirst. The Coq Workshop, 2021.
 - Synthetic Versions of the Kleene-Post and Post's Theorem. Dominik Kirst, Niklas Mück, Yannick Forster. TYPES, 2022.
 - Strong, Synthetic, and Computational Proofs of Gödel's First Incompleteness Theorem. Benjamin Peters, Dominik Kirst. TYPES, 2022.
 - A Coq Library for Mechanised First-Order Logic. Dominik Kirst, Johannes Hostert, Andrej Dudenhefner, Yannick Forster, Marc Hermes, Mark Koch, Dominique Larchey-Wendling, Niklas Mück, Benjamin Peters, Gert Smolka, Dominik Wehr. The Coq Workshop, 2022.
+- The Blurred Drinker Paradox and Blurred Choice Axioms for the Downward Löwenheim-Skolem Theorem. Dominik Kirst, Haoyi Zeng. TYPES, 2024.

theories/ModelTheory/AnalysisLS.v

@@ -0,0 +1,71 @@
+Require Import FOL.ModelTheory.LogicalPrinciples.
+Require Import FOL.ModelTheory.HenkinEnv.
+Require Import FOL.ModelTheory.ReverseLS. 
+Require Import FOL.ModelTheory.Core.
+
+(** * Full Decomposition of DLS *)
+
+Section LSiffDC.
+
+    Corollary LS_iff_DC_under_CC_nat_LEM: 
+        CC_nat -> LEM -> DLS <-> DC.
+    Proof.
+        intros H1 H2; split.
+        - eapply LS_CC_impl_DC; eauto.
+        - intros DC. eapply LS_downward_with_DC_LEM; eauto.
+    Qed.
+
+    Corollary LS_iff_DC_BDP_BEP_under_CC_nat:
+        CC_nat -> DLS <-> DC /\ BDP /\ BEP.
+    Proof.
+        intros H1; split.
+        - intros HLS. repeat split.
+          now apply LS_CC_impl_DC.
+          now apply LS_impl_BDP.
+          now apply LS_impl_BEP.
+        - intros (h1 & h2 & h3).
+          now apply LS_downward_with_BDP_BEP_DC.
+    Qed.
+
+    Corollary LS_iff_DDC_BDP_BEP_BCC:
+        DLS <-> DDC /\ BDP /\ BEP /\ BCC.
+    Proof.
+        split.
+        - intros HLS. repeat split.
+          assert (OBDC) as HO. now  apply LS_impl_OBDC.
+          assert (BDC2) as H2. intros X x. now apply OBDC_impl_BDC2_on, HO.
+          now apply BDC2_iff_DDC_BCC.
+          now apply LS_impl_BDP. now apply LS_impl_BEP.
+          now eapply BDC_impl_BCC, LS_impl_BDC. 
+        - intros (h1 & h2 & h3 & h4).
+          now apply  LS_downward.
+    Qed.
+
+    Theorem Decomposition1: 
+      DLS -> DDC /\ BDP /\ BEP /\ BCC.
+    Proof. now rewrite LS_iff_DDC_BDP_BEP_BCC. Qed.
+
+    Theorem Decomposition2: 
+      DDC /\ BDP /\ BEP /\ BCC -> BDP /\ BEP /\ BDC2.
+    Proof.
+      intros (h1 & h2 & h3 & h4). repeat split; eauto; now apply res_BDC2.
+    Qed.
+
+    Theorem Decomposition3:
+      BDC2 /\ BDP /\ BEP -> OBDC.
+    Proof.
+      intros (h1 & h2 & h3).
+      assert DDC as h4 by (now apply BDC2_impl_DDC).
+      assert BCC. apply BDC_impl_BCC. now apply BDC2_impl_BDC.
+      assert DLS by now rewrite LS_iff_DDC_BDP_BEP_BCC.
+      now apply LS_impl_OBDC.
+    Qed.
+
+    Theorem Decomposition4:
+      OBDC <-> DLS.
+    Proof.
+      split; [intro H; now apply LS_downward'|].
+      apply LS_impl_OBDC.
+    Qed.
+
+End LSiffDC.

theories/ModelTheory/ClassicalDC.v

@@ -0,0 +1,127 @@
+Require Export Undecidability.FOL.Syntax.Theories.
+Require Import Undecidability.FOL.Syntax.BinSig.
+Require Import FOL.ModelTheory.Core.
+Require Import FOL.ModelTheory.DCPre.
+
+(** * Reverse Analysis: DC-Delta *)
+
+Section DC.
+
+    Existing Instance sig_empty.
+    Existing Instance sig_binary.
+
+    Fact Σ_countable: countable_sig.
+    Proof.
+        repeat split.
+        - exists (fun _ => None). intros [].
+        - exists (fun _ => Some  tt). intros []. exists 42; eauto.
+        - intros []. - intros [] []; firstorder.
+    Qed.
+
+    Variable A: Type.
+    Variable a: A.
+    Variable R: A -> A -> Prop.
+
+    Instance interp__A : interp A :=
+    {
+        i_func := fun F v => match F return A with end;
+        i_atom := fun P v => R (hd v) (last v)
+    }.
+
+    Definition Model__A: model :=
+    {|
+        domain := A;
+        interp' := interp__A
+    |}.
+
+    Definition total_form :=
+        ∀ (∃ (atom _ _ _ _ tt (cons _ ($1) _ (cons _ ($0) _ (nil _))))).
+    Definition forfor_form :=
+        (atom _ _ _ _ tt (cons _ ($1) _ (cons _ ($0) _ (nil _)))).
+
+    Lemma total_sat:
+        forall h, (forall x, exists y, R x y) -> Model__A ⊨[h] total_form.
+    Proof.
+        cbn; intros.
+        destruct (H d) as [e P].
+        now exists e.
+    Qed.
+
+    Definition p {N} (α β: N): env N :=
+        fun n => match n with
+            | 0 => β
+            | _ => α end.
+
+    Lemma forfor_sat {N} (h: N -> A) (α β: N):
+        R (h α) (h β) <-> Model__A ⊨[(p α β) >> h] forfor_form.
+    Proof.
+        unfold ">>"; now cbn.
+    Qed.
+
+    Lemma exists_next:
+    forall B (R': B -> B -> Prop), coutable_model B ->
+        (forall x, exists y, R' x y) -> exists f: nat -> B,
+            forall b, exists n, R' b (f n).
+    Proof.
+        intros B R' (f & h & sur) total.
+        exists f. intro b.
+        destruct (total b) as [c Rbc].
+        exists (h c). now rewrite sur.
+    Qed.    
+
+    Section dec__R_full.
+
+    Definition dec_R := forall x y, dec (R x y).
+
+    Lemma LS_impl_DC: DLS -> dec_R -> DC_on' R.
+    Proof using a.
+        intros LS DecR  total.
+        destruct (LS sig_empty sig_binary Σ_countable Model__A a) as [N [(h & g & Hh) [f HN]]].
+        specialize (@total_sat ((fun _ => (h 42)) >> f) total ) as total'.
+        apply HN in total'.
+        assert (exists R', (forall x: N, (exists y: N, R' x y)) /\ (forall α β, R' α β <-> R (f  α) (f β))).
+        exists (fun x y => tt ₚ[ N] cons N x 1 (cons N y 0 (nil N))).
+        split. intro x. now specialize(total' x).
+        intros α β; rewrite forfor_sat.
+        now unfold elementary_homomorphism in HN; rewrite <- HN.
+        destruct H as [R' [P1 P2]].
+        assert (forall x y, dec (R' x y)) as dec__R'.
+        { intros x y. destruct (DecR (f x) (f y)); firstorder. }
+        assert (forall n : N, exists m : nat, h m = n) as Ht.
+        { intro n. exists (g n). now rewrite Hh. }
+        destruct (@DC_ω _ _ h Ht dec__R' P1 (h 42)) as [g' [case0 Choice]].
+        exists (g' >> f); unfold ">>". 
+        intro n'; now rewrite <- (P2 (g' n') (g' (S n'))).
+    Qed.
+
+    End dec__R_full.
+
+End DC.
+
+Section DCRes.
+
+    Theorem LS_impl_DC_delta: DLS -> DC__Δ .
+    Proof.
+        intros H X R dec_R x tot_R.
+        apply LS_impl_DC; eauto.
+    Qed.
+
+End DCRes.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+