From Loeb.internal_provability Require Import PA_Lists_Signature.
From Loeb Require Import Definitions.
From Undecidability.FOL Require Import Syntax.Core Arithmetics.Robinson.
From FOL.Incompleteness Require Import utils.
From FOL.Proofmode Require Import Theories ProofMode.
Require Import String List.
From Equations Require Import Equations.

Open Scope PA_li_Notation.

Existing Instance PA_li_funcs_signature.
Existing Instance PA_preds_signature.
Existing Instance full_operators.
Existing Instance falsity_on.

Section Axioms.

    Context {göd: goedelisation}.

    Definition ax_len_nil := len [|] === zero.
    Definition ax_len_cons := ∀∀ len ($0 ::: $1) === σ (len $1).
    Definition ax_get_zero := ∀∀ (($0 ::: $1) G zero) === $0.
    Definition ax_get_succ := ∀∀∀ (($0 ::: $1) G (σ $2)) === ($1 G $2).
    Definition ax_len_app := ∀∀ len ($0 +++ $1) === len $0 ⊕ len $1.
    Definition ax_get_app_left := ∀∀∀ $2 ⧀l len $0 → (($0 +++ $1) G $2) === ($0 G $2).
    Definition ax_get_app_right := ∀∀∀ $2 ⧀l len $1 → (($0 +++ $1) G ($2 ⊕ len $0)) === ($1 G $2).
    Definition ax_impl (φ ψ: form) := (num' ((göd.(g)) (φ → ψ))) === (num' ((göd.(g)) φ)) ~> (num' ((göd.(g)) ψ)).

    Definition ax_cons_congr := ∀∀∀∀ $0 === $1 → $2 === $3 → ($0 ::: $2) === ($1 ::: $3).
    Definition ax_len_congr := ∀∀ $0 === $1 → len ($0) === len ($1).
    Definition ax_get_congr := ∀∀∀∀ $0 === $1 → $2 === $3 → ($0 G $2) === ($1 G $3).
    Definition ax_app_congr := ∀∀∀∀ $0 === $1 → $2 === $3 → ($0 +++ $2) === ($1 +++ $3).
    Definition ax_imp_congr := ∀∀∀∀ $0 === $1 → $2 === $3 → ($0 ~> $2) === ($1 ~> $3).

    Definition Li := ax_len_nil::ax_len_cons::ax_get_zero::ax_get_succ::ax_len_app::ax_get_app_left::ax_get_app_right::ax_cons_congr::ax_len_congr::ax_get_congr::ax_app_congr::ax_imp_congr::nil.

    Definition QLi := (map (fun f => form_inclusion f) Q) ++ Li.
    Definition QEqLi := QLi ++ (map (fun f => form_inclusion f) EQ).

    Definition ax_induction' (φ: form) :=
    φ[zero..] → (∀ φ → φ[σ $0 .: S >> var]) → ∀ φ.

    Inductive QEqLiFull: form -> Prop :=
    | In_QEqLi φ: In φ QEqLi -> QEqLiFull φ
    | QEqImpl φ ψ: QEqLiFull (ax_impl φ ψ)
    | QEqInduction φ: QEqLiFull (ax_induction' φ).

End Axioms.

Section QEqLi_rewriting.

    Instance eqdec_funcs: EqDec PA_li_funcs_signature.
    Proof. intros x y. apply PA_li_funcs_eq. Qed.

    Instance eqdec_preds : EqDec PA_preds_signature.
    Proof. intros x y. destruct x, y. now left. Qed.

    Open Scope string_scope.

    Opaque QEqLi.

    Context {pei: peirce}.
    Context {göd: goedelisation}.

    Program Instance PA_li_Leibniz : Leibniz PA_li_funcs_signature PA_preds_signature falsity_on.
    Next Obligation. exact Eq. Defined.
    Next Obligation. exact QEqLi. Defined.
    Next Obligation.
      fintros. unfold PA_li_Leibniz_obligation_1.
      fapply ((form_inclusion ax_refl)).
    Qed.
    Next Obligation.
      fintros. unfold PA_li_Leibniz_obligation_1.
      fapply ((form_inclusion ax_sym)). ctx.
    Qed.
    Next Obligation.
      unfold PA_li_Leibniz_obligation_1 in *. rename v1 into t; rename v2 into t0.
      destruct F; repeat dependent elimination t0; repeat dependent elimination t.
      - destruct p; repeat dependent elimination t0; repeat dependent elimination t.
        + fapply ((form_inclusion ax_refl)).
        + fapply ((form_inclusion ax_succ_congr)). apply H1.
        + fapply ((form_inclusion ax_add_congr)); apply H1.
        + fapply ((form_inclusion ax_mult_congr)); apply H1.
      - fapply ((form_inclusion ax_refl)).
      - fapply (ax_cons_congr); apply H1.
      - fapply (ax_len_congr). apply H1.
      - fapply (ax_get_congr); apply H1.
      - fapply (ax_app_congr); apply H1.
      - fapply (ax_imp_congr); apply H1.
    Qed.
    Next Obligation.
    unfold PA_li_Leibniz_obligation_1 in *. rename v1 into t; rename v2 into t0.
    destruct P; repeat dependent elimination t0; repeat dependent elimination t.
    - cbn in H1. split.
      + intros H2. feapply ((form_inclusion ax_trans)). feapply ((form_inclusion ax_sym)).
        apply H1. feapply ((form_inclusion ax_trans)). apply H2. apply H1.
      + intros H2. feapply ((form_inclusion ax_trans)). apply H1. feapply ((form_inclusion ax_trans)).
        apply H2. fapply ((form_inclusion ax_sym)). apply H1.
    Qed.

    Lemma QEqLi_leibniz_t t x y : QEqLi ⊢ x === y → t`[x..] === t`[y..].
    Proof.
        induction t.
        - destruct x0; cbn.
          + fintros. ctx.
          + fintros. fapply ((form_inclusion ax_refl)).
        - destruct F. destruct p.
          + rewrite (vec_0_nil v).
            cbn. fintros. fapply ((form_inclusion ax_refl)).
          + destruct (vec_1_inv v) as [z ->]. cbn.
            fintros. fapply ((form_inclusion ax_succ_congr)).
            frevert 0. fapply IH. apply Vector.In_cons_hd.
          + destruct (vec_2_inv v) as (a & b & ->).
            cbn. fintros. fapply ((form_inclusion ax_add_congr)).
            all: frevert 0; fapply IH.
            * apply Vector.In_cons_hd.
            * apply Vector.In_cons_tl, Vector.In_cons_hd.
          + destruct (vec_2_inv v) as (a & b & ->).
            cbn. fintros. fapply ((form_inclusion ax_mult_congr)).
            all: frevert 0; fapply IH.
            * apply Vector.In_cons_hd.
            * apply Vector.In_cons_tl, Vector.In_cons_hd.
          + cbn in v. rewrite (vec_0_nil v).
            cbn. fintros. fapply ((form_inclusion ax_refl)).
          + destruct (vec_2_inv v) as (a & b & ->).
            cbn. fintros. fapply ax_cons_congr.
            all: frevert 0; fapply IH.
            * apply Vector.In_cons_hd.
            * apply Vector.In_cons_tl, Vector.In_cons_hd.
          + destruct (vec_1_inv v) as [z ->]. cbn.
            fintros. fapply ax_len_congr.
            frevert 0. fapply IH. apply Vector.In_cons_hd.
          + destruct (vec_2_inv v) as (a & b & ->).
            cbn. fintros. fapply ax_get_congr.
            all: frevert 0; fapply IH.
            * apply Vector.In_cons_hd.
            * apply Vector.In_cons_tl, Vector.In_cons_hd.
          + destruct (vec_2_inv v) as (a & b & ->).
            cbn. fintros. fapply ax_app_congr.
            all: frevert 0; fapply IH.
            * apply Vector.In_cons_hd.
            * apply Vector.In_cons_tl, Vector.In_cons_hd.
          + destruct (vec_2_inv v) as (a & b & ->).
            cbn. fintros. fapply ax_imp_congr.
            all: frevert 0; fapply IH.
            * apply Vector.In_cons_hd.
            * apply Vector.In_cons_tl, Vector.In_cons_hd.
    Qed.

  Lemma QEqLi_leibniz x y φ:
        QEqLi ⊢ x === y → φ[x..] → φ[y..].
  Proof.
      enough (QEqLi ⊢ x === y → φ[x..] ↔ φ[y..]).
      { fintros. fapply H; ctx. }
      induction φ using form_ind_subst.
      - cbn. fintros. fsplit; fintros; ctx.
      - destruct P0. cbn in t.
        destruct (vec_2_inv t) as (a & b & ->).
        cbn. fstart. fintros.
        fassert (a`[x..] === a`[y..]).
        { pose proof (QEqLi_leibniz_t a x y).
          fapply H. fapply "H". }
        fassert (b`[x..] === b`[y..]).
        { pose proof (QEqLi_leibniz_t b x y).
          fapply H. fapply "H". }
        frewrite "H0". frewrite "H1".
        fsplit; fintros; ctx.
      - fstart; fintros.
        fassert (φ1[x..] ↔ φ1[y..]) by (fapply IHφ1; fapply "H").
        fassert (φ2[x..] ↔ φ2[y..]) by (fapply IHφ2; fapply "H").
        destruct b0; fsplit; cbn.
        + fintros "[H2 H3]". fsplit.
          * fapply "H0". ctx.
          * fapply "H1". ctx.
        + fintros "[H2 H3]". fsplit.
          * fapply "H0". ctx.
          * fapply "H1". ctx.
        + fintros "[H2|H3]".
          * fleft. fapply "H0". ctx.
          * fright. fapply "H1". ctx.
        + fintros "[H2|H3]".
          * fleft. fapply "H0". ctx.
          * fright. fapply "H1". ctx.
        + fintros "H2" "H3".
          fapply "H1". fapply "H2". fapply "H0". ctx.
        + fintros "H2" "H3".
          fapply "H1". fapply "H2". fapply "H0". ctx.
      - fstart. fintros. fsplit; destruct q; cbn; fintros.
        + specialize (H (x0`[↑]..)).
          asimpl in H. asimpl. fapply H.
          * ctx.
          * fspecialize ("H0" x0). asimpl. ctx.
        + fdestruct "H0". fexists x0.
          specialize (H (x0`[↑]..)).
          asimpl in H. asimpl. fapply H; ctx.
        + specialize (H (x0`[↑]..)).
          asimpl in H. asimpl. fapply H.
          * ctx.
          * fspecialize ("H0" x0). asimpl. ctx.
        + fdestruct "H0". fexists x0.
          specialize (H (x0`[↑]..)).
          asimpl in H. asimpl. fapply H; ctx.
  Qed.

  Lemma QEqLiFull_leibniz x y φ:
    QEqLiFull ⊩ (x === y → φ[x..] → φ[y..]).
  Proof.
    exists QEqLi. split.
    - intros ψ Hψ. now apply In_QEqLi.
    - apply QEqLi_leibniz.
  Qed.

  Transparent QEqLi.

End QEqLi_rewriting.