From Equations Require Import Equations.
From Undecidability.Shared Require Import Dec.
From Undecidability.FOL Require Import Syntax.Core Arithmetics.Signature Arithmetics.FA.
Import Vector.VectorNotations Vectors.VectorDef.

Inductive PA_li_funcs: Type :=
    | PA_func: PA_funcs -> PA_li_funcs
    | Nil: PA_li_funcs
    | Cons: PA_li_funcs
    | Len: PA_li_funcs
    | Get: PA_li_funcs
    | App: PA_li_funcs
    | Imp: PA_li_funcs.

Definition PA_li_funcs_ar (f: PA_li_funcs) :=
match f with
    | PA_func f' => PA_funcs_ar f'
    | Nil => 0
    | Cons => 2
    | Len => 1
    | Get => 2
    | App => 2
    | Imp => 2
    end.

Definition PA_li_funcs_eq (x y: PA_li_funcs): {x = y} + {x <> y}.
Proof. decide equality. apply PA_funcs_eq. Defined.

#[global]
Instance PA_li_funcs_signature: funcs_signature :=
{| syms := PA_li_funcs ; ar_syms := PA_li_funcs_ar |}.

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

Lemma PA_li_formulas_eq:
    EqDec form.
Proof.
  intros φ ψ. apply dec_form.
    - apply PA_li_funcs_eq.
    - apply PA_preds_eq.
    - intros x y. unfold Dec.dec. decide equality.
    - intros x y. unfold Dec.dec. decide equality.
Qed.

Declare Scope PA_li_Notation.
Open Scope PA_li_Notation.

Notation "'zero'" := (@func PA_li_funcs_signature (PA_func Zero) ([])) (at level 1): PA_li_Notation.
Notation "'σ' x" := (@func PA_li_funcs_signature (PA_func Succ) ([x])) (at level 32): PA_li_Notation.
Notation "x '⊕' y" := (@func PA_li_funcs_signature (PA_func Plus) ([x ; y]) ) (at level 39): PA_li_Notation.
Notation "x '⊗' y" := (@func PA_li_funcs_signature (PA_func Mult) ([x ; y]) ) (at level 38): PA_li_Notation.
Notation "'[|]'" := (@func PA_li_funcs_signature Nil ([])) (at level 1): PA_li_Notation.
Notation "x ':::' y" := (@func PA_li_funcs_signature Cons ([x ; y])) (at level 40): PA_li_Notation.
Notation "'len' x" := (@func PA_li_funcs_signature Len ([x])) (at level 32): PA_li_Notation.
Notation "x 'G' y" := (@func PA_li_funcs_signature Get ([x ; y])) (at level 40): PA_li_Notation.
Notation "x '+++' y" := (@func PA_li_funcs_signature App ([x ; y])) (at level 37): PA_li_Notation.
Notation "x '~>' y" := (@func PA_li_funcs_signature Imp ([x ; y])) (at level 35): PA_li_Notation.
Notation "x '===' y" := (@atom PA_li_funcs_signature PA_preds_signature _ _ Eq ([x ; y])) (at level 40) : PA_li_Notation.

Fixpoint term_inclusion (t: @term PA_funcs_signature): @term PA_li_funcs_signature := match t with
  | var n => var n
  | func f v => func _ (PA_func f) (map (fun t => term_inclusion t) v)
  end.

Definition num' n := term_inclusion (num n).

Fixpoint form_inclusion {ff: falsity_flag} (f: @form PA_funcs_signature PA_preds_signature full_operators ff): @form PA_li_funcs_signature PA_preds_signature full_operators ff := match f with
  | falsity => falsity
  | bin op f1 f2 => bin op (form_inclusion f1) (form_inclusion f2)
  | quant qt f1 => quant qt (form_inclusion f1)
  | atom P v => atom P (map (fun t => term_inclusion t) v)
  end.

Lemma num'_bound' n k:
  bounded_t k (num' n).
Proof.
  induction n; cbn; constructor.
  - intros t H. inversion H.
  - intros t [-> | H]%vec_cons_inv; [easy | inversion H].
Qed.

Section comparisons.
  Existing Instance PA_preds_signature.
  Existing Instance PA_li_funcs_signature.

  Definition PAlt x y := ∃ y`[↑] === (σ x`[↑] ⊕ $0).
  Definition PAle x y := ∃ y`[↑] === (x`[↑] ⊕ $0).
  Definition PAle' x y := ∃ y`[↑] === ($0 ⊕ x`[↑]).

  Lemma PAlt_subst x y ρ : (PAlt x y)[ρ] = PAlt (x`[ρ]) (y`[ρ]).
  Proof.
    unfold PAlt. cbn. now asimpl.
  Qed.

  Lemma PAle_subst x y ρ : (PAle x y)[ρ] = PAle (x`[ρ]) (y`[ρ]).
  Proof.
    unfold PAle. cbn. now asimpl.
  Qed.

  Lemma PAle'_subst x y ρ : (PAle' x y)[ρ] = PAle' (x`[ρ]) (y`[ρ]).
  Proof.
    unfold PAle'. cbn. now asimpl.
  Qed.
End comparisons.

Notation "x '⧀l' y" := (PAlt x y) (at level 40) : PA_li_Notation.
Notation "x '⧀=l' y" := (PAle x y) (at level 40) : PA_li_Notation.
Notation "x '⧀=l'' y" := (PAle' x y) (at level 40) : PA_li_Notation.