Require Import List Permutation.

Set Implicit Arguments.


Local Infix "~p" := (@Permutation _) (at level 70).


Notation ill_vars := nat.

Inductive ill_connective := ill_with | ill_limp | ill_times | ill_plus.
Inductive ill_constant := ill_1 | ill_bot | ill_top.

Inductive ill_form : Set :=
  | ill_var : ill_vars -> ill_form
  | ill_cst : ill_constant -> ill_form
  | ill_ban : ill_form -> ill_form
  | ill_bin : ill_connective -> ill_form -> ill_form -> ill_form.


Notation "⟙" := (ill_cst ill_top).
Notation "⟘" := (ill_cst ill_bot).
Notation "𝟙" := (ill_cst ill_1).

Infix "&" := (ill_bin ill_with) (at level 50).
Infix "⊗" := (ill_bin ill_times) (at level 50).
Infix "⊕" := (ill_bin ill_plus) (at level 50).
Infix "⊸" := (ill_bin ill_limp) (at level 51, right associativity).

Notation "'!' x" := (ill_ban x) (at level 52).

Notation "£" := ill_var.

Notation "‼ x" := (map ill_ban x) (at level 60).

Notation "∅" := nil (only parsing).

Reserved Notation "l '⊢' x" (at level 70, no associativity).

Section S_ill_restr_without_cut.


  Inductive S_ill_restr : list ill_form -> ill_form -> Prop :=

    | in_ill1_ax : forall A, A:: A

    | in_ill1_perm : forall Γ Δ A, Γ ~p Δ -> Γ A
                                           
                                        -> Δ A

    | in_ill1_limp_l : forall Γ Δ A B C, Γ A -> B::Δ C
                                           
                                      -> A B::Γ++Δ C

    | in_ill1_limp_r : forall Γ A B, A::Γ B
                                           
                                        -> Γ A B

    | in_ill1_with_l1 : forall Γ A B C, A::Γ C
                                           
                                      -> A&B::Γ C

    | in_ill1_with_l2 : forall Γ A B C, B::Γ C
                                           
                                      -> A&B::Γ C
 
    | in_ill1_with_r : forall Γ A B, Γ A -> Γ B
                                           
                                      -> Γ A&B

    | in_ill1_bang_l : forall Γ A B, A::Γ B
                                           
                                      -> !A::Γ B

    | in_ill1_bang_r : forall Γ A, Γ A
                                           
                                      -> Γ !A

    | in_ill1_weak : forall Γ A B, Γ B
                                           
                                      -> !A::Γ B

    | in_ill1_cntr : forall Γ A B, !A::!A::Γ B
                                           
                                      -> !A::Γ B

  where "l ⊢ x" := (S_ill_restr l x).

End S_ill_restr_without_cut.

Section S_ill_restr_with_cut.


  Inductive S_ill_restr_wc : list ill_form -> ill_form -> Prop :=

    | in_ill2_ax : forall A, A:: A

    | in_ill2_cut : forall Γ Δ A B, Γ A -> A::Δ B
                                           
                                      -> Γ++Δ B

    | in_ill2_perm : forall Γ Δ A, Γ ~p Δ -> Γ A
                                           
                                        -> Δ A

    | in_ill2_limp_l : forall Γ Δ A B C, Γ A -> B::Δ C
                                           
                                      -> A B::Γ++Δ C

    | in_ill2_limp_r : forall Γ A B, A::Γ B
                                           
                                        -> Γ A B

    | in_ill2_with_l1 : forall Γ A B C, A::Γ C
                                           
                                      -> A&B::Γ C

    | in_ill2_with_l2 : forall Γ A B C, B::Γ C
                                           
                                      -> A&B::Γ C
 
    | in_ill2_with_r : forall Γ A B, Γ A -> Γ B
                                           
                                      -> Γ A&B

    | in_ill2_bang_l : forall Γ A B, A::Γ B
                                           
                                      -> !A::Γ B

    | in_ill2_bang_r : forall Γ A, Γ A
                                           
                                      -> Γ !A

    | in_ill2_weak : forall Γ A B, Γ B
                                           
                                      -> !A::Γ B

    | in_ill2_cntr : forall Γ A B, !A::!A::Γ B
                                           
                                      -> !A::Γ B

  where "l ⊢ x" := (S_ill_restr_wc l x).

End S_ill_restr_with_cut.

Section S_ill_without_cut.


  Inductive S_ill : list ill_form -> ill_form -> Prop :=

    | in_ill3_ax : forall A, A:: A

    | in_ill3_perm : forall Γ Δ A, Γ ~p Δ -> Γ A
                                           
                                        -> Δ A

    | in_ill3_limp_l : forall Γ Δ A B C, Γ A -> B::Δ C
                                           
                                      -> A B::Γ++Δ C

    | in_ill3_limp_r : forall Γ A B, A::Γ B
                                           
                                        -> Γ A B

    | in_ill3_with_l1 : forall Γ A B C, A::Γ C
                                           
                                      -> A&B::Γ C

    | in_ill3_with_l2 : forall Γ A B C, B::Γ C
                                           
                                      -> A&B::Γ C
 
    | in_ill3_with_r : forall Γ A B, Γ A -> Γ B
                                           
                                      -> Γ A&B

    | in_ill3_bang_l : forall Γ A B, A::Γ B
                                           
                                      -> !A::Γ B

    | in_ill3_bang_r : forall Γ A, Γ A
                                           
                                      -> Γ !A

    | in_ill3_weak : forall Γ A B, Γ B
                                           
                                      -> !A::Γ B

    | in_ill3_cntr : forall Γ A B, !A::!A::Γ B
                                           
                                      -> !A::Γ B

    | in_ill3_times_l : forall Γ A B C, A::B::Γ C
                                           
                                      -> AB::Γ C
 
    | in_ill3_times_r : forall Γ Δ A B, Γ A -> Δ B
                                           
                                      -> Γ++Δ AB

    | in_ill3_plus_l : forall Γ A B C, A::Γ C -> B::Γ C
                                           
                                      -> AB::Γ C

    | in_ill3_plus_r1 : forall Γ A B, Γ A
                                           
                                      -> Γ AB

    | in_ill3_plus_r2 : forall Γ A B, Γ B
                                           
                                      -> Γ AB

    | in_ill3_bot_l : forall Γ A, ::Γ A

    | in_ill3_top_r : forall Γ, Γ

    | in_ill3_unit_l : forall Γ A, Γ A
                                           
                                      -> 𝟙::Γ A

    | in_ill3_unit_r : 𝟙

  where "l ⊢ x" := (S_ill l x).

End S_ill_without_cut.

Section S_ill_with_cut.


  Inductive S_ill_wc : list ill_form -> ill_form -> Prop :=

    | in_ill4_ax : forall A, A:: A

    | in_ill4_cut : forall Γ Δ A B, Γ A -> A::Δ B
                                           
                                      -> Γ++Δ B

    | in_ill4_perm : forall Γ Δ A, Γ ~p Δ -> Γ A
                                           
                                        -> Δ A

    | in_ill4_limp_l : forall Γ Δ A B C, Γ A -> B::Δ C
                                           
                                      -> A B::Γ++Δ C

    | in_ill4_limp_r : forall Γ A B, A::Γ B
                                           
                                        -> Γ A B

    | in_ill4_with_l1 : forall Γ A B C, A::Γ C
                                           
                                      -> A&B::Γ C

    | in_ill4_with_l2 : forall Γ A B C, B::Γ C
                                           
                                      -> A&B::Γ C
 
    | in_ill4_with_r : forall Γ A B, Γ A -> Γ B
                                           
                                      -> Γ A&B

    | in_ill4_bang_l : forall Γ A B, A::Γ B
                                           
                                      -> !A::Γ B

    | in_ill4_bang_r : forall Γ A, Γ A
                                           
                                      -> Γ !A

    | in_ill4_weak : forall Γ A B, Γ B
                                           
                                      -> !A::Γ B

    | in_ill4_cntr : forall Γ A B, !A::!A::Γ B
                                           
                                      -> !A::Γ B

    | in_ill4_times_l : forall Γ A B C, A::B::Γ C
                                           
                                      -> AB::Γ C
 
    | in_ill4_times_r : forall Γ Δ A B, Γ A -> Δ B
                                           
                                      -> Γ++Δ AB

    | in_ill4_plus_l : forall Γ A B C, A::Γ C -> B::Γ C
                                           
                                      -> AB::Γ C

    | in_ill4_plus_r1 : forall Γ A B, Γ A
                                           
                                      -> Γ AB

    | in_ill4_plus_r2 : forall Γ A B, Γ B
                                           
                                      -> Γ AB

    | in_ill4_bot_l : forall Γ A, ::Γ A

    | in_ill4_top_r : forall Γ, Γ

    | in_ill4_unit_l : forall Γ A, Γ A
                                           
                                      -> 𝟙::Γ A

    | in_ill4_unit_r : 𝟙

  where "l ⊢ x" := (S_ill_wc l x).

End S_ill_with_cut.

Definition rILL_cf_PROVABILITY (S : _*_) := let (Γ,A) := S in S_ill_restr Γ A.
Definition rILL_PROVABILITY (S : _*_) := let (Γ,A) := S in S_ill_restr_wc Γ A.

Definition ILL_cf_PROVABILITY (S : _*_) := let (Γ,A) := S in S_ill Γ A.
Definition ILL_PROVABILITY (S : _*_) := let (Γ,A) := S in S_ill_wc Γ A.