From Undecidability.Synthetic Require Import Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts.
From Undecidability Require Import Shared.ListAutomation.
From Undecidability Require Import Shared.Libs.PSL.Vectors.Vectors Shared.Libs.PSL.Vectors.VectorForall.
Import ListAutomationNotations.

Import Coq.Vectors.Vector.
Local Notation vec := t.

Set Default Proof Using "Type".

Inductive peirce := class | intu.
Existing Class peirce.

Definition scons {X: Type} (x : X) (xi : nat -> X) :=
  fun n => match n with
        | 0 => x
        | S n => xi n
        end.

Definition funcomp {X Y Z} (g : Y -> Z) (f : X -> Y) :=
  fun x => g (f x).

Fixpoint iter {X: Type} f n (x : X) :=
  match n with
    0 => x
  | S m => f (iter f m x)
  end.

Fact iter_switch {X} f n x :
  f (@iter X f n x) = iter f n (f x).
Proof.
  induction n; cbn; now try rewrite IHn.
Qed.


Class funcs_signature :=
  { syms : Type; ar_syms : syms -> nat }.

Coercion syms : funcs_signature >-> Sortclass.

Class preds_signature :=
  { preds : Type; ar_preds : preds -> nat }.

Coercion preds : preds_signature >-> Sortclass.

Section fix_signature.

  Context {Σ_funcs : funcs_signature}.


  Unset Elimination Schemes.

  Inductive term : Type :=
  | var : nat -> term
  | func : forall (f : syms), vec term (ar_syms f) -> term.
  Arguments func _ _ : clear implicits.
  Lemma term_rect' (p : term -> Type) :
    (forall x, p (var x)) -> (forall F v, (ForallT p v) -> p (@func F v)) -> forall (t : term), p t.
  Proof.
    intros f1 f2. fix strong_term_ind' 1. destruct t as [n|F v].
    - apply f1.
    - apply f2. induction v.
      + econstructor.
      + econstructor. now eapply strong_term_ind'. eauto.
  Qed.

  Lemma term_rect (p : term -> Type) :
    (forall x, p (var x)) -> (forall F v, (forall t, Vector_In2 t v -> p t) -> p (@func F v)) -> forall (t : term), p t.
  Proof.
    intros f1 f2. eapply term_rect'.
    - apply f1.
    - intros. apply f2. intros t. induction 1; inversion X; subst; eauto.
  Qed.

  Lemma term_ind (p : term -> Prop) :
    (forall x, p (var x)) -> (forall F v (IH : forall t, In t v -> p t), p (func F v)) -> forall (t : term), p t.
  Proof.
    intros f1 f2. eapply term_rect'.
    - apply f1.
    - intros. apply f2. intros t. induction 1; inversion X; subst; eauto.
  Qed.

  Set Elimination Schemes.

  Fixpoint subst_term (σ : nat -> term) (t : term) : term :=
    match t with
    | var t => σ t
    | func f v => func f (map (subst_term σ) v)
    end.

  Context {Σ_preds : preds_signature}.


  Inductive falsity_flag := falsity_off | falsity_on.
  Existing Class falsity_flag.
  Existing Instance falsity_on | 1.
  Existing Instance falsity_off | 0.

  Class operators := {binop : Type ; quantop : Type}.
  Context {ops : operators}.

  Inductive form : falsity_flag -> Type :=
  | falsity : form falsity_on
  | atom {b} : forall (P : preds), vec term (ar_preds P) -> form b
  | bin {b} : binop -> form b -> form b -> form b
  | quant {b} : quantop -> form b -> form b.
  Arguments form {_}.
  Arguments atom {_} _ _, _ _ _.
  Arguments bin {_} _ _ _, _ _ _ _.
  Arguments quant {_} _ _, _ _ _.

  Definition up (σ : nat -> term) := scons (var 0) (funcomp (subst_term (funcomp var S)) σ).

  Fixpoint subst_form `{falsity_flag} (σ : nat -> term) (phi : form) : form :=
    match phi with
    | falsity => falsity
    | atom P v => atom P (map (subst_term σ) v)
    | bin op phi1 phi2 => bin op (subst_form σ phi1) (subst_form σ phi2)
    | quant op phi => quant op (subst_form (up σ) phi)
    end.

End fix_signature.

Arguments term _, {_}.
Arguments var _ _, {_} _.
Arguments func _ _ _, {_} _ _.
Arguments subst_term {_} _ _.

Arguments form _ _ _ _, _ _ {_ _}, {_ _ _ _}, {_ _ _} _.
Arguments atom _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments bin _ _ _ _, _ _ {_ _}, {_ _ _ _}.
Arguments quant _ _ _ _, _ _ {_ _}, {_ _ _ _}.

Arguments up _, {_}.
Arguments subst_form _ _ _ _, _ _ {_ _}, {_ _ _ _}.


Declare Scope subst_scope.
Open Scope subst_scope.

Notation "$ x" := (var x) (at level 3, format "$ '/' x") : subst_scope.
Notation "t `[ sigma ]" := (subst_term sigma t) (at level 7, left associativity, format "t '/' `[ sigma ]") : subst_scope.
Notation "phi [ sigma ]" := (subst_form sigma phi) (at level 7, left associativity, format "phi '/' [ sigma ]") : subst_scope.
Notation "s .: sigma" := (scons s sigma) (at level 70, right associativity) : subst_scope.
Notation "f >> g" := (funcomp g f) (at level 50) : subst_scope.
Notation "s '..'" := (scons s var) (at level 4, format "s ..") : subst_scope.
Notation "↑" := (S >> var) : subst_scope.


Module FullSyntax.

  Inductive full_logic_sym : Type :=
  | Conj : full_logic_sym
  | Disj : full_logic_sym
  | Impl : full_logic_sym.

  Inductive full_logic_quant : Type :=
  | All : full_logic_quant
  | Ex : full_logic_quant.

  Definition full_operators : operators :=
    {| binop := full_logic_sym ; quantop := full_logic_quant |}.

  #[export] Hint Immediate full_operators : typeclass_instances.

  Declare Scope full_syntax.
  Delimit Scope full_syntax with Ffull.

  #[global] Open Scope full_syntax.
  Notation "∀ Phi" := (@quant _ _ full_operators _ All Phi) (at level 50) : full_syntax.
  Notation "∃ Phi" := (@quant _ _ full_operators _ Ex Phi) (at level 50) : full_syntax.
  Notation "A ∧ B" := (@bin _ _ full_operators _ Conj A B) (at level 41) : full_syntax.
  Notation "A ∨ B" := (@bin _ _ full_operators _ Disj A B) (at level 42) : full_syntax.
  Notation "A → B" := (@bin _ _ full_operators _ Impl A B) (at level 43, right associativity) : full_syntax.
  Notation "⊥" := (falsity) : full_syntax.
  Notation "¬ A" := (A ) (at level 42) : full_syntax.
  Notation "A ↔ B" := ((A B) (B A)) (at level 43) : full_syntax.

  Fixpoint impl {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} (A : list form) phi :=
    match A with
    | [] => phi
    | psi :: A => bin _ _ full_operators _ Impl psi (impl A phi)
    end.

  Notation "A ==> phi" := (impl A phi) (right associativity, at level 55).

  Definition exist_times {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} n (phi : form) := iter (fun psi => psi) n phi.
  Definition forall_times {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} n (phi : form) := iter (fun psi => psi) n phi.

End FullSyntax.


Module FragmentSyntax.

  Inductive frag_logic_binop : Type :=
  | Impl : frag_logic_binop.

  Inductive frag_logic_quant : Type :=
  | All : frag_logic_quant.

  Definition frag_operators : operators :=
    {| binop := frag_logic_binop ; quantop := frag_logic_quant |}.

  #[export] Hint Immediate frag_operators : typeclass_instances.

  Declare Scope fragment_syntax.
  Delimit Scope fragment_syntax with Ffrag.

  #[global] Open Scope fragment_syntax.
  Notation "∀ Phi" := (@quant _ _ frag_operators _ All Phi) (at level 50) : fragment_syntax.
  Notation "phi → psi" := (@bin _ _ frag_operators _ Impl phi psi) (at level 43, right associativity) : fragment_syntax.
  Notation "¬ phi" := (phi falsity) (at level 42) : fragment_syntax.
  Notation "⊥" := (falsity) : fragment_syntax.

  Fixpoint impl {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} (A : list form) phi :=
    match A with
    | [] => phi
    | psi :: A => bin _ _ frag_operators _ Impl psi (impl A phi)
    end.

  Notation "A ==> phi" := (impl A phi) (right associativity, at level 55).

  Definition forall_times {Σ_funcs : funcs_signature} {Σ_preds : preds_signature} {ff : falsity_flag} n (phi : form) := iter (fun psi => psi) n phi.

End FragmentSyntax.