From Undecidability.FOL.Incompleteness Require Import utils Axiomatisations.

From Undecidability.Synthetic Require Import Definitions EnumerabilityFacts.

From Undecidability.FOL Require Import FullSyntax.
From Undecidability.FOL.Arithmetics Require Import PA NatModel TarskiFacts DeductionFacts.

From Undecidability.FOL.Proofmode Require Import Theories ProofMode.
Require Import String List.
Open Scope string_scope.

From Equations Require Import Equations.
Require Import Lia List.


Notation "I ⊨=L T" := ( psi, List.In T I ⊨= ) (at level 20).
Notation "I ; rho '⊨' phi" := (@sat _ _ _ I _ ) (at level 20, at next level).

Section lemmas.
  Existing Instance PA_preds_signature.
  Existing Instance PA_funcs_signature.
  Existing Instance interp_nat.

  Lemma iμ_standard (k : ) : k = k.
  Proof.
    induction k; cbn; congruence.
  Qed.


  Lemma sat_single_PA M (I : interp M) φ ρ k : ( k .: ρ) φ ρ φ[(num k)..].
  Proof.
    erewrite eval_num. apply sat_single.
  Qed.


  Lemma sat_single_nat φ ρ k : interp_nat; (k .: ρ) φ interp_nat; ρ φ[(num k)..].
  Proof.
    erewrite iμ_standard at 1.
    now rewrite sat_single_PA.
  Qed.


End lemmas.

Lemma list_theory_enumerable {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} A :
  enumerable (list_theory A).
Proof.
  exists (List.nth_error A).
  intros x. split.
  - apply List.In_nth_error.
  - intros [k Hk]. eapply List.nth_error_In, Hk.
Qed.


Definition Qeq := Qeq.
Global Opaque Qeq.
Lemma Qeq_def : Qeq = Robinson.Qeq.
Proof. reflexivity. Qed.

Section PM.
  Existing Instance PA_preds_signature.
  Existing Instance PA_funcs_signature.

  Global Program Instance PA_Leibniz : Leibniz PA_funcs_signature PA_preds_signature falsity_on.
  Next Obligation. exact Eq. Defined.
  Next Obligation. exact Qeq. Defined.
  Next Obligation. fintros. fapply ax_refl. Qed.
  Next Obligation. fintros. fapply ax_sym. ctx. Qed.
  Next Obligation.
    unfold PA_Leibniz_obligation_1 in *. rename into t; rename into .
    destruct F; repeat dependent elimination ; repeat dependent elimination t.
    - fapply ax_refl.
    - fapply ax_succ_congr. apply .
    - fapply ax_add_congr; apply .
    - fapply ax_mult_congr; apply .
  Qed.

  Next Obligation.
    unfold PA_Leibniz_obligation_1 in *. rename into t; rename into .
    destruct P; repeat dependent elimination ; repeat dependent elimination t.
    - cbn in . split.
      + intros . feapply ax_trans. feapply ax_sym. apply . feapply ax_trans.
        apply . apply .
      + intros . feapply ax_trans. apply . feapply ax_trans. apply .
        fapply ax_sym. apply .
  Qed.


End PM.

Section n.
  Existing Instance PA_preds_signature.
  Existing Instance PA_funcs_signature.
  Context `{pei : peirce}.

  Lemma closed_term_is_num s : bounded_t 0 s { n & Qeq s == num n }.
  Proof.
    intros H.
    induction s using term_rect. 2: destruct F.
    - exfalso. inversion H. .
    - exists 0. cbn. cbn in v. enough (func Zero v = zero) as by fapply ax_refl.
      f_equal. apply vec_0_nil.
    - destruct (vec_1_inv v) as [t ]. destruct (X t) as [n Hn].
      + left.
      + revert H. invert_bounds. apply . left.
      + exists (S n). fapply ax_succ_congr. apply Hn.
    - destruct (vec_2_inv v) as ( & & ).
      destruct (X , X ) as [[ ] [ ]].
      + left.
      + revert H. invert_bounds. apply . left.
      + right. left.
      + revert H. invert_bounds. apply . right. left.
      + exists ( + ).
        pose proof num_add_homomorphism as H'.
        refine (( H'' _) (H' _ Qeq _ )).
        2: { firstorder. }
        frewrite H''.
        fapply ax_add_congr; assumption.
    - destruct (vec_2_inv v) as ( & & ).
      destruct (X , X ) as [[ ] [ ]].
      + left.
      + revert H. invert_bounds. apply . left.
      + right. left.
      + revert H. invert_bounds. apply . right. left.
      + exists ( * ).
        pose proof num_mult_homomorphism as H'.
        refine (( H'' _) (H' _ Qeq _ )).
        2: { firstorder. }
        frewrite H''.
        fapply ax_mult_congr; assumption.
  Qed.


End n.