(**************************************************************)
(*   Copyright Dominique Larchey-Wendling *                 *)
(*                                                            *)
(*                             * Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Permutation Arith.

From Undecidability.ILL Require Import ILL.

Set Implicit Arguments.

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

Inductive cll_connective := cll_with | cll_plus | cll_limp | cll_times | cll_par.
Inductive cll_constant := cll_1 | cll_0 | cll_bot | cll_top.
Inductive cll_modality := cll_bang | cll_qmrk | cll_neg.

Notation cll_vars := nat.

Inductive cll_form : Set :=
  | cll_var : cll_vars -> cll_form
  | cll_cst : cll_constant -> cll_form
  | cll_una : cll_modality -> cll_form -> cll_form
  | cll_bin : cll_connective -> cll_form -> cll_form -> cll_form.

(* Symbols for cut&paste ⟙   ⟘  𝟙 ﹠ ⊗  ⊕  ⊸ ! ‼ ‽ ⁇ ∅  ⊢ *)

(* These notations replace the ILL notations *)

(* Variables *)

Notation "'£' x" := (cll_var x) (at level 1).

(* Constants *)

Notation "⟙" := (cll_cst cll_top).
Notation "⟘" := (cll_cst cll_bot).
Notation "𝟙" := (cll_cst cll_1).
Notation "𝟘" := (cll_cst cll_0).

(* Unary connectives: linear negation and modalities *)
(* ? cannot be used because it is reserved by Coq so we use ‽ instead *)

Notation "'⊖' x" := (cll_una cll_neg x) (at level 50, format "⊖ x").
Notation "'!' x" := (cll_una cll_bang x) (at level 52).
Notation "'‽' x" := (cll_una cll_qmrk x) (at level 52).

(* Binary connectives *)

Infix "&" := (cll_bin cll_with) (at level 50).
Infix "⅋" := (cll_bin cll_par) (at level 50).
Infix "⊗" := (cll_bin cll_times) (at level 50).
Infix "⊕" := (cll_bin cll_plus) (at level 50).
Infix "⊸" := (cll_bin cll_limp) (at level 51, right associativity).

(* Modalities iterated over lists *)

Notation "‼ x" := (map (cll_una cll_bang) x) (at level 60).
Notation "⁇ x" := (map (cll_una cll_qmrk) x) (at level 60).

(* The empty list *)

Notation "∅" := nil.

Local Reserved Notation "Γ ⊢ Δ" (at level 70, no associativity).

Section S_cll_restr_without_cut.

  (* CLL rules restricted to the (!,&,-o) fragment without cut *)

  Inductive S_cll_restr : list cll_form -> list cll_form -> Prop :=

    | in_cll1_ax : forall A, A:: A::

    | in_cll1_perm : forall Γ Δ Γ' Δ', Γ ~p Γ' -> Δ ~p Δ' -> Γ Δ
                                           (*-----------------------------*)
                                      -> Γ' Δ'

    | in_cll1_limp_l : forall Γ Δ Γ' Δ' A B, Γ A::Δ -> B::Γ' Δ'
                                           (*-----------------------------*)
                                      -> A B::Γ++Γ' Δ++Δ'

    | in_cll1_limp_r : forall Γ Δ A B, A::Γ B::Δ
                                           (*-----------------------------*)
                                      -> Γ A B::Δ

    | in_cll1_with_l1 : forall Γ Δ A B, A::Γ Δ
                                           (*-----------------------------*)
                                      -> A&B::Γ Δ

    | in_cll1_with_l2 : forall Γ Δ A B, B::Γ Δ
                                           (*-----------------------------*)
                                      -> A&B::Γ Δ
 
    | in_cll1_with_r : forall Γ Δ A B, Γ A::Δ -> Γ B::Δ
                                           (*-----------------------------*)
                                      -> Γ A&B::Δ

    | in_cll1_bang_l : forall Γ A Δ, A::Γ Δ
                                           (*-----------------------------*)
                                      -> !A::Γ Δ

    | in_cll1_bang_r : forall Γ A, Γ A::nil (* since ? is absent, only ??Δ = nil works *)
                                           (*-----------------------------*)
                                      -> Γ !A::nil

    | in_cll1_weak_l : forall Γ A Δ, Γ Δ
                                           (*-----------------------------*)
                                      -> !A::Γ Δ

    | in_cll1_cntr_l : forall Γ A Δ, !A::!A::Γ Δ
                                           (*-----------------------------*)
                                      -> !A::Γ Δ

  where "l ⊢ m" := (S_cll_restr l m).

End S_cll_restr_without_cut.

Section S_cll_without_cut_on_ill_syntax.

  (* CLL rules restricted to the (𝟘,?,⅋) free fragment without cut 
      which shares the same formula language as ILL, but of course 
      not the same rules *)


  Inductive S_cll_2 : list cll_form -> list cll_form -> Prop :=

    | in_cll2_ax : forall A, A:: A::

    | in_cll2_perm : forall Γ Δ Γ' Δ', Γ ~p Γ' -> Δ ~p Δ' -> Γ Δ
                                           (*-----------------------------*)
                                      -> Γ' Δ'

    | in_cll2_limp_l : forall Γ Δ Γ' Δ' A B, Γ A::Δ -> B::Γ' Δ'
                                           (*-----------------------------*)
                                      -> A B::Γ++Γ' Δ++Δ'

    | in_cll2_limp_r : forall Γ Δ A B, A::Γ B::Δ
                                           (*-----------------------------*)
                                      -> Γ A B::Δ

    | in_cll2_with_l1 : forall Γ Δ A B, A::Γ Δ
                                           (*-----------------------------*)
                                      -> A&B::Γ Δ

    | in_cll2_with_l2 : forall Γ Δ A B, B::Γ Δ
                                           (*-----------------------------*)
                                      -> A&B::Γ Δ
 
    | in_cll2_with_r : forall Γ Δ A B, Γ A::Δ -> Γ B::Δ
                                           (*-----------------------------*)
                                      -> Γ A&B::Δ

    | in_cll2_times_l : forall Γ A B Δ, A::B::Γ Δ
                                           (*-----------------------------*)
                                      -> AB::Γ Δ
 
    | in_cll2_times_r : forall Γ Δ Γ' Δ' A B, Γ A::Δ -> Γ' B::Δ'
                                           (*-----------------------------*)
                                      -> Γ++Γ' AB::Δ++Δ'

    | in_cll2_plus_l : forall Γ A B Δ, A::Γ Δ -> B::Γ Δ
                                           (*-----------------------------*)
                                      -> AB::Γ Δ

    | in_cll2_plus_r1 : forall Γ A B Δ, Γ A::Δ
                                           (*-----------------------------*)
                                      -> Γ AB::Δ

    | in_cll2_plus_r2 : forall Γ A B Δ, Γ B::Δ
                                           (*-----------------------------*)
                                      -> Γ AB::Δ

    | in_cll2_bot_l : forall Γ Δ, ::Γ Δ

    | in_cll2_top_r : forall Γ Δ, Γ ::Δ

    | in_cll2_unit_l : forall Γ Δ, Γ Δ
                                           (*-----------------------------*)
                                        -> 𝟙::Γ Δ

    | in_cll2_unit_r : 𝟙::


    | in_cll2_bang_l : forall Γ A Δ, A::Γ Δ
                                           (*-----------------------------*)
                                      -> !A::Γ Δ

    | in_cll2_bang_r : forall Γ A, Γ A::nil (* since ? is absent, only ??Δ = nil works *)
                                           (*-----------------------------*)
                                      -> Γ !A::nil

    | in_cll2_weak_l : forall Γ A Δ, Γ Δ
                                           (*-----------------------------*)
                                      -> !A::Γ Δ

    | in_cll2_cntr_l : forall Γ A Δ, !A::!A::Γ Δ
                                           (*-----------------------------*)
                                      -> !A::Γ Δ

  where "l ⊢ m" := (S_cll_2 l m).

End S_cll_without_cut_on_ill_syntax.

Section cut_free_cll.

  (* All the rules of Cut-free CLL *)

  Reserved Notation "Γ ⊢ Δ" (at level 70, no associativity).

  Inductive S_cll : list cll_form -> list cll_form -> Prop :=

    | in_cll_ax : forall A, A:: A::

(*
    | in_cll_cut   : forall Γ Δ Γ' Δ' A,        Γ ⊢ A::Δ    ->   A::Γ' ⊢ Δ'
                                             (*-----------------------------*)
                                        ->           Γ++Γ' ⊢ Δ++Δ'
*)


    | in_cll_perm : forall Γ Δ Γ' Δ', Γ ~p Γ' -> Δ ~p Δ' -> Γ Δ
                                             (*-----------------------------*)
                                        -> Γ' Δ'

    | in_cll_neg_l : forall Γ Δ A, Γ A::Δ
                                             (*-----------------------------*)
                                        -> A::Γ Δ

    | in_cll_neg_r : forall Γ Δ A, A::Γ Δ
                                             (*-----------------------------*)
                                        -> Γ A::Δ


    | in_cll_limp_l : forall Γ Δ Γ' Δ' A B, Γ A::Δ -> B::Γ' Δ'
                                             (*-----------------------------*)
                                        -> A B::Γ++Γ' Δ++Δ'

    | in_cll_limp_r : forall Γ Δ A B, A::Γ B::Δ
                                             (*-----------------------------*)
                                        -> Γ A B::Δ

    | in_cll_with_l1 : forall Γ Δ A B, A::Γ Δ
                                             (*-----------------------------*)
                                        -> A&B::Γ Δ

    | in_cll_with_l2 : forall Γ Δ A B, B::Γ Δ
                                             (*-----------------------------*)
                                        -> A&B::Γ Δ
 
    | in_cll_with_r : forall Γ Δ A B, Γ A::Δ -> Γ B::Δ
                                             (*-----------------------------*)
                                        -> Γ A&B::Δ

    | in_cll_times_l : forall Γ A B Δ, A::B::Γ Δ
                                             (*-----------------------------*)
                                        -> AB::Γ Δ
 
    | in_cll_times_r : forall Γ Δ Γ' Δ' A B, Γ A::Δ -> Γ' B::Δ'
                                             (*-----------------------------*)
                                        -> Γ++Γ' AB::Δ++Δ'

    | in_cll_par_l : forall Γ Δ Γ' Δ' A B, A::Γ Δ -> B::Γ' Δ'
                                             (*-----------------------------*)
                                        -> A⅋B::Γ++Γ' Δ++Δ'

    | in_cll_par_r : forall Γ A B Δ, Γ A::B::Δ
                                             (*-----------------------------*)
                                        -> Γ A⅋B::Δ

    | in_cll_plus_l : forall Γ A B Δ, A::Γ Δ -> B::Γ Δ
                                             (*-----------------------------*)
                                        -> AB::Γ Δ

    | in_cll_plus_r1 : forall Γ A B Δ, Γ A::Δ
                                             (*-----------------------------*)
                                        -> Γ AB::Δ

    | in_cll_plus_r2 : forall Γ A B Δ, Γ B::Δ
                                             (*-----------------------------*)
                                        -> Γ AB::Δ

    | in_cll_bot_l : forall Γ Δ, ::Γ Δ

    | in_cll_top_r : forall Γ Δ, Γ ::Δ

    | in_cll_unit_l : forall Γ Δ, Γ Δ
                                             (*-----------------------------*)
                                        -> 𝟙::Γ Δ

    | in_cll_unit_r : 𝟙::

    | in_cll_zero_l : (*-----------------------------*)
                                             (* *) 𝟘::

    | in_cll_zero_r : forall Γ Δ, Γ Δ
                                             (*-----------------------------*)
                                        -> Γ 𝟘::Δ


    | in_cll_bang_l : forall Γ A Δ, A::Γ Δ
                                             (*-----------------------------*)
                                        -> !A::Γ Δ

    | in_cll_bang_r : forall Γ A Δ, Γ A::Δ
                                             (*-----------------------------*)
                                        -> Γ !A::Δ

    | in_cll_qmrk_l : forall Γ A Δ, A::Γ Δ
                                             (*-----------------------------*)
                                        -> A::Γ Δ

    | in_cll_qmrk_r : forall Γ A Δ, Γ A::Δ
                                             (*-----------------------------*)
                                        -> Γ A::Δ

    | in_cll_weak_l : forall Γ A Δ, Γ Δ
                                             (*-----------------------------*)
                                        -> !A::Γ Δ

    | in_cll_weak_r : forall Γ A Δ, Γ Δ
                                             (*-----------------------------*)
                                        -> Γ A::Δ

    | in_cll_cntr_l : forall Γ A Δ, !A::!A::Γ Δ
                                             (*-----------------------------*)
                                        -> !A::Γ Δ

    | in_cll_cntr_r : forall Γ A Δ, Γ A::A::Δ
                                             (*-----------------------------*)
                                        -> Γ A::Δ

  where "Γ ⊢ Δ" := (S_cll Γ Δ).

End cut_free_cll.

Definition rCLL_cf_PROVABILITY (S : _*_) := let (Γ,Δ) := S in S_cll_restr Γ Δ.
Definition CLL_cf_PROVABILITY (S : _*_) := let (Γ,Δ) := S in S_cll Γ Δ.