Require Import FOL Peano Tarski Deduction CantorPairing NumberTheory Synthetic DecidabilityFacts.
Require Import Lia.
Require Import FOL Peano Tarski Deduction CantorPairing NumberTheory Formulas Synthetic DecidabilityFacts Coding.
Require Import Lia.

Section Model.

  Variable D : Type.
  Variable I : interp D.
  Notation "⊨ phi" := ( rho, ) (at level 21).
  Variable axioms : ax, PA ax ax.

  Notation "N⊨ phi" := ( rho, @sat _ _ interp_nat _ ) (at level 40).
  Notation "x 'i⧀' y" := ( d : D, y = iσ (x i d) ) (at level 40).

  Lemma bounded_definite_unary'' ϕ :
    bounded 1 ϕ x, y, y i x ( _ y) ϕ ( _ y) ϕ.
  Proof.
    intros .
    pose (Φ := ¬¬ $0 $1 --> ϕ ¬ ϕ).
    assert ( d rho, (d .: ) Φ) as H.
    apply induction.
    - apply axioms.
    - repeat solve_bounds; eapply bounded_up; try apply ; try lia.
    - intros . cbn. apply DN.
      now intros y Hy%nolessthen_zero.
    - intros x IHx . cbn -[Q] in *.
      specialize (IHx ).
      assert (~~ ((x .: ) ϕ (x .: ) ϕ) ) as H' by tauto.
      apply (DN_chaining IHx), (DN_chaining H'), DN.
      intros H IH y.
      rewrite lt_S; auto.
      intros [LT| ].
      + destruct (IH _ LT) as [h|h].
        * left. eapply bound_ext. apply . 2 : apply h.
          intros []; solve_bounds.
        * right. intros . apply h.
          eapply bound_ext. apply . 2 : apply .
          intros []; solve_bounds.
      + destruct H as [h|h].
        * left. eapply bound_ext. apply . 2 : apply h.
          intros []; solve_bounds.
        * right. intros . apply h.
          eapply bound_ext. apply . 2 : apply .
          intros []; solve_bounds.
    - intros x.
      specialize (H x ( _ )). cbn in H.
      apply (DN_chaining H), DN. clear H; intros H.
      intros y Hy. destruct (H _ Hy) as [h|h].
      + left. eapply bound_ext. apply . 2: apply h.
        intros []; solve_bounds.
      + right. intros G. apply h.
        eapply bound_ext. apply . 2: apply G.
        intros []; solve_bounds.
  Abort.

  Lemma bounded_definite_unary' ϕ rho :
    bounded 2 ϕ x b, y, y i x (y .: b .: ) ϕ (y .: b .: ) ϕ.
  Proof.
    intros .
    pose (Φ := ¬¬ $0 $2 --> ϕ ¬ ϕ).
    assert ( d rho, (d .: ) Φ) as H.
    apply induction.
    - apply axioms.
    - repeat solve_bounds; eapply bounded_up; try apply ; try lia.
    - intros b. cbn. apply DN.
      now intros y Hy%nolessthen_zero.
    - intros x IHx. cbn -[Q] in *.
      intros b. specialize (IHx b).
      assert (~~ ((x .: b .: b .: ) ϕ (x .: b .: b .: ) ϕ) ) as H' by tauto.
      apply (DN_chaining IHx), (DN_chaining H'), DN.
      intros H IH y.
      rewrite lt_S; auto.
      intros [LT| ].
      + destruct (IH _ LT) as [h|h].
        * left. eapply bound_ext. apply . 2 : apply h.
          intros [|[]]; solve_bounds.
        * right. intros . apply h.
          eapply bound_ext. apply . 2 : apply .
          intros [|[]]; solve_bounds.
      + destruct H as [h|h].
        * left. eapply bound_ext. apply . 2 : apply h.
          intros [|[]]; solve_bounds.
        * right. intros . apply h.
          eapply bound_ext. apply . 2 : apply .
          intros [|[]]; solve_bounds.
    - intros x b.
      specialize (H x ( _ )). cbn in H.
      specialize (H b).
      apply (DN_chaining H), DN. clear H; intros H.
      intros y Hy. destruct (H _ Hy) as [h|h].
      + left. eapply bound_ext. apply . 2: apply h.
        intros [|[]]; solve_bounds.
      + right. intros G. apply h.
        eapply bound_ext. apply . 2: apply G.
        intros [|[]]; solve_bounds.
  Qed.


  Corollary bounded_definite_unary ϕ b rho x :
    bounded 2 ϕ y, y i x (y .: b .: ) ϕ (y .: b .: ) ϕ.
  Proof.
    intros ; now apply bounded_definite_unary'.
  Qed.


  Lemma bounded_definite_binary ϕ :
    bounded 2 ϕ x, y z, y i x z i x (z .: _ y) ϕ (z .: _ y) ϕ.
  Proof.
    intros .
    pose (Φ := ¬¬ ∀∀ $0 $2 --> $1 $2 --> ϕ ¬ ϕ).
    assert ( d rho, (d .: ) Φ) as H.
    apply induction. apply axioms.
    repeat solve_bounds; eapply bounded_up; try apply ; try lia.
    - intros . cbn. intros nH. apply nH.
      now intros y z Hy%nolessthen_zero.
    - intros b IH . cbn -[Q] in *.
      specialize (IH ).
      assert (~~ ((b .: b .: ) ϕ (b .: b .: ) ϕ) ) as Hbb by tauto.
      apply (DN_chaining IH), (DN_chaining Hbb).
      apply (DN_chaining (bounded_definite_unary _ b b )).
      refine (DN_chaining (bounded_definite_unary (ϕ[$1 ..] ) b b _) _).
      { eapply subst_bound; eauto.
        intros [|[]]; solve_bounds. }
      apply DN. clear IH Hbb.
      intros Hbb IH x y.
      rewrite !lt_S; try apply axioms.
      intros [lty| ] [ltx| ].
      + destruct (IH _ _ lty ltx) as [h|h].
        * left. eapply bound_ext. apply . 2 : apply h.
          intros [|[]]; solve_bounds.
        * right. intros . apply h.
          eapply bound_ext. apply . 2 : apply .
          intros [|[]]; solve_bounds.
      + destruct ( _ lty) as [h|h].
        * left. eapply bound_ext. apply . 2 : apply h.
          intros [|[]]; solve_bounds.
        * right. intros . apply h.
          eapply bound_ext. apply . 2 : apply .
          intros [|[]]; solve_bounds.
      + destruct ( _ ltx) as [h|h]; rewrite sat_comp in h.
        * left. eapply bound_ext. apply . 2 : apply h.
          intros [|[]]; solve_bounds.
        * right. intros . apply h.
          eapply bound_ext. apply . 2 : apply .
          intros [|[]]; solve_bounds.
      + destruct Hbb as [h|h].
        * left. eapply bound_ext. apply . 2 : apply h.
          intros [|[]]; solve_bounds.
        * right. intros . apply h.
        eapply bound_ext. apply . 2 : apply .
        intros [|[]]; solve_bounds.
      - intros x.
        specialize (H x ( _ )). cbn in H.
        apply (DN_chaining H), DN. clear H; intros H.
        intros y z Hy Hz. destruct (H _ _ Hz Hy) as [h|h].
        + left. eapply bound_ext. apply . 2: apply h.
          intros [|[]]; solve_bounds.
        + right. intros . apply h.
          eapply bound_ext. apply . 2: apply .
          intros [|[]]; solve_bounds.
  Qed.


  Definition div_num n (d : D) := e, inu n i e = d.
  Definition Div_nat (d : D) := n div_num n d.

  Lemma DN_Div_nat :
    UC bool nonStd D d, ~~Dec (Div_nat d).
  Proof.
    intros uc [e He] d.
    refine (DN_chaining _ _).
    2 : { now apply DN, UC_Def_Dec. }
    refine (DN_chaining (bounded_definite_binary ( $1 $0 == $2) _ (iσ (d i e))) _).
    { repeat solve_bounds. }
    apply DN. intros H n.
    destruct (H d (inu n)) as [h|h].
    - now exists e.
    - apply num_lt_nonStd; auto.
      rewrite add_rec; auto.
      intros h%std_add; auto.
      now apply He.
    - left. apply h.
    - right. apply h.
  Qed.


End Model.