From FOL Require Import FullSyntax Arithmetics Theories.
From Undecidability.Shared Require Import ListAutomation.
From FOL.Tennenbaum Require Import MoreDecidabilityFacts Church Coding NumberUtils Formulas SyntheticInType Peano CantorPairing.

Require Import Lia.

Import Vector.VectorNotations.

Notation "x ∣ y" := ( k, x * k = y) (at level 50).

Section Model.
  Existing Instance PA_preds_signature.
  Existing Instance PA_funcs_signature.

  Variable D : Type.
  Variable I : interp D.
  Existing Instance Peano.I'.
  Notation Q := Qeq.

  Notation "⊨ phi" := ( ρ, ρ ⊨ ) (at level 21).
  Notation "N⊨ phi" := ( ρ, @sat _ _ interp_nat _ ρ ) (at level 40).
  Variable axioms : ax, PAeq ax ρ, sat (Peano.I' I) ρ ax.

  Notation "x 'i=' y" := (@i_atom PA_funcs_signature PA_preds_signature D I Eq ([x ; y])) (at level 40).
  Notation "'iσ' x" := (@i_func PA_funcs_signature PA_preds_signature D I Succ ([x])) (at level 37).
  Notation "x 'i⊕' y" := (@i_func PA_funcs_signature PA_preds_signature D I Plus ([x ; y])) (at level 39).
  Notation "x 'i⊗' y" := (@i_func PA_funcs_signature PA_preds_signature D I Mult ([x ; y])) (at level 38).
  Notation "'i0'" := (i_func (Σ_funcs:=PA_funcs_signature) (f:=Zero) []) (at level 2) : PA_Notation.
  Notation "x 'i⧀' y" := ( d : D, y = iσ (x i⊕ d) ) (at level 40).

  Variable ψ : form.
  Variable Hψ : binary ψ ( x, Q ⊢I ∀ ψ[up (num x)..] ↔ $0 == num (Irred x) ).

  Definition div_num n (d : D) := @Coding.div_num D I n d.
  Definition div_pi n a := @Coding.div_pi D I ψ n a.

Tennenbaum's Theorem

Proof via Diagonal Argument

Enumerable and discrete PA models have decidable divisibility.

  Lemma nat_eq_dec (n m : ) : {n = m} + {n m}.
  Proof. decide equality. Qed.

  Lemma dec_div :
    Enumerable D Discrete D Dec ( '(n, d) div_num n d).
  Proof.
    intros [G Hg] [eq]%Discrete_sum.
    pose (g n := match G n with None | Some d d end).
    constructor. intros [n d].
    destruct (eq d ) as [|h].
    { left; exists . now rewrite mult_zero_r. }
    destruct n as [|n].
    { right; intros [k Hk]. rewrite mult_zero in Hk; auto. }
    refine (let H' := @iEuclid' D I axioms d (S n) _ in _).
    assert ( q r, r < S n d = (g q) i⊗ inu (S n) i⊕ inu r) as H.
    { destruct H' as [Q [r ]], (Hg Q) as [q Hq].
      exists q, r. unfold g. now rewrite Hq.
    } clear H'.
    apply ProductWO in H.
    destruct H as [q [r [? Hr]]].
    * destruct (nat_eq_dec r 0) as [E|E].
      + left. exists (g q).
        now rewrite Hr, E, add_zero_r, mult_comm.
      + right. intros [k Hk]. apply E.
        enough (iE : inu r = inu 0).
        { now apply inu_inj in iE. }
        enough ((g q) = k inu r = inu 0) by tauto.
        eapply (@iFac_unique D I axioms).
        -- eapply lt_equiv; eauto.
        -- eapply lt_equiv; auto || .
        -- rewrite add_zero, add_comm; auto.
           rewrite Hr. rewrite mult_comm. all:eauto.
    * intros x y. apply and_dec; [apply Compare_dec.lt_dec|apply eq].
    Unshelve. .
  Qed.

We can show the same for types that are witnessing and discrete. This is a bit more general, since every enumerable type is witnessing.
  Lemma dec_div_2 :
    Witnessing D Discrete D Dec ( '(n, d) div_num n d).
  Proof.
    intros wo [eq]%Discrete_sum.
    constructor. intros [n d].
    destruct (eq d ) as [|h].
    { left; exists . now rewrite mult_zero_r. }
    destruct n as [|n].
    { right; intros [k Hk]. rewrite mult_zero in Hk; auto. }
    refine (let H := @iEuclid' D I axioms d (S n) _ in _).
    apply wo in H.
    - destruct H as [a Ha].
      apply Witnessing_nat in Ha.
      * destruct Ha as [r [? Hr]].
        destruct (nat_eq_dec r 0) as [E|E].
        + left. exists a.
          now rewrite Hr, E, add_zero_r, mult_comm.
        + right. intros [k Hk]. apply E.
          enough (iE : inu r = inu 0).
          { now apply inu_inj in iE. }
          enough (a = k inu r = inu 0) by tauto.
          unshelve eapply (@iFac_unique D I axioms (inu (S n))).
          -- apply lt_equiv; auto.
          -- apply lt_equiv; auto || .
          -- rewrite add_zero. rewrite add_comm.
             rewrite Hr. rewrite mult_comm. all: eauto.
      * intros x. apply and_dec; [apply Compare_dec.lt_dec|apply eq].
    - intros ?. apply dec_lt_bounded_exist.
      intros ?. apply eq.
    Unshelve. .
  Qed.

Tennenbaum's Theorem via a diagnoal argument.

  Fact dec_contraposition A B :
    dec B (B A) (A B).
  Proof. intros HB nB a. destruct HB; tauto. Qed.

  Fact Stable_std_stable_stdModel :
    Stable std stable (stdModel D).
  Proof.
    intros Hstd H e. apply Hstd. intros He. apply H.
    intros HD. apply He, HD.
  Qed.

  Fact Stable_std_negn_nonStd__sdtMobel_equiv :
    Stable std stdModel D nonStd D.
  Proof.
    intros stab. split.
    - apply forall__neg_exists_neg.
    - unfold nonStd, stdModel, std.
      apply (Stable_neg_exists_neg__forall); eauto.
  Qed.

  Fact MP_Discrete_stable_std :
    MP Discrete D Stable std.
  Proof.
    intros mp [eq]%Discrete_sum e. unfold Stable.
    refine (MP_Dec_stable mp _ _).
    constructor. intros ?; apply eq.
  Qed.

This lemma is similar to the coding lemmas in Coding.v as it allows decidable predicates to be coded.
  Lemma Coding_Dec p :
    @WCT_Q intu Stable std stdModel D Dec p
    ~~ c, n, p n div_pi n c.
  Proof.
    intros wrt%WCT_WRTs ? notStd Dec_p.
    apply (DN_remove (wrt _ Dec_p)).
    intros [ϕ ( & _ & & )].
    unshelve refine (let H:= @Coding_nonStd_unary _ _ _ _ Hψ _ _ ϕ _ in _); auto.
    apply (DN_chaining H), DN; clear H.
    intros [c Hc].
    exists c; intros n. split.
    + intros H. specialize (Hc n ( _ c)) as [ _].
      apply in H. apply soundness in H.
      unfold div_pi.
      eapply bound_ext with (N:= 2)(:= inu n .: c .: ( _ c)).
      { repeat solve_bounds.
        eapply bounded_up; [apply Hψ|]. }
      { intros [|[]]; cbn; [reflexivity|reflexivity|]. }
      cbn in ; apply .
      unfold valid_ctx in *.
      specialize (H D (Peano.I' I) ( _ c)).
      rewrite switch_num.
      eapply bound_ext with (N:=0). 3: apply H.
      { eapply subst_bound; eauto.
        intros []; try .
        intros _. apply num_bound. }
      { . }
      apply sat_Q_axioms, axioms.
    + specialize (Hc n ( _ c)) as [_ ].
      destruct (Dec_p) as [dec_p]; auto.
      apply dec_contraposition; [apply dec_p|].
      intros h [d Hd].
      specialize ( _ h). apply soundness in .
      eapply with ( := _ inu 0)(I:= Peano.I' I).
      { apply sat_Q_axioms, axioms. }
      apply switch_num. cbn in .
      eapply bound_ext with (N:= 1)(:= inu n .: c .: ( _ c)).
      { now solve_bounds. }
      intros []; cbn; [reflexivity|].
      apply . exists d. split.
      { eapply bound_ext. apply Hψ. 2: apply Hd.
        intros [|[]]; cbn; [reflexivity|reflexivity|]. }
      destruct Hd as [_ [k Hk]]. exists k.
      now rewrite Hk.
  Qed.

  Lemma Coding_Dec_ct p :
    @CT_Q intu Stable std stdModel D
    Dec p ~~ c, n, p n div_pi n c.
  Proof. now intros ?%CT_WCT; apply Coding_Dec. Qed.

We can now use the above coding lemma in combination with RT to give a diagonal argument which shows that enumerable and discrete PA models must potentially be standard. The double negation can actually also be eliminated, and this is done in Variants.v, where the needed lemmas are shown. We can still establish the result with the weaker assumption of WCT_Q.
  Theorem Tennenbaum_diagonal :
   @WCT_Q intu MP Enumerable D Discrete D e, std e.
  Proof.
    intros wct mp enum eq.
    apply Stable_std_stable_stdModel.
    { apply MP_Discrete_stable_std; auto. }
    intros notStd.
    specialize (dec_div enum eq) as [dec_div].
    specialize enum as [G HG].
    pose (g n := match G n with None | Some d d end).
    pose (p n := div_pi n (g n)).
    apply (@Coding_Dec p); auto.
    - intros e. apply MP_Dec_stable; auto.
      apply Discrete_sum in eq.
      destruct eq as [eq].
      constructor. intros n. apply eq.
    - unfold p. constructor. intros n.
      destruct (dec_div (Irred n, g n)) as [h|nh].
      + right. apply DN. now apply ψ_equiv.
      + left. intros ?. apply nh. eapply ψ_equiv; eauto.
    - intros [c' H]. destruct (HG c') as [c Hc].
      specialize (H c). revert H.
      unfold p, g. rewrite Hc.
      tauto.
  Qed.

  Theorem Tennenbaum_diagonal_ct :
    @CT_Q intu MP Enumerable D Discrete D e, std e.
  Proof. now intros ?%CT_WCT; apply Tennenbaum_diagonal. Qed.

End Model.