(**************************************************************)
(*   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.

Set Implicit Arguments.

(* * Intuitionistic Multiplicative Sub-Exponential Linear Logic 

      derived from  https://doi.org/10.1017/S0960129516000293 *)


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

Reserved Notation "A ⊸ B" (at level 51, right associativity, format "A ⊸ B").
Reserved Notation "'![' m ']' x" (at level 52, format "![ m ] x").
Reserved Notation "‼ x" (at level 60, format "‼ x").

Section IMSELL.

  Variables (var bang : Type)
            (bang_le : bang -> bang -> Prop) (* a pre-order on modalities *)
            (bang_U : bang -> Prop) (* universal modalities have structural rules *)
            .

  Notation Λ := bang.

  Inductive imsell_form : Type :=
    | imsell_var : var -> imsell_form
    | imsell_ban : Λ -> imsell_form -> imsell_form
    | imsell_imp : imsell_form -> imsell_form -> imsell_form.

  Infix "⊸" := imsell_imp.
  Notation "![ m ] x" := (imsell_ban m x).
  Notation "£" := imsell_var.

  Definition imsell_lban := map (fun '(m,A) => ![m]A).

  Notation "‼ Γ" := (imsell_lban Γ).
  Notation "u ≼ l" := (forall '(v,A), In (v,A) l -> bang_le u v) (at level 70).
  Notation U := bang_U.

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

  (* We consider the (!.,-o) fragment of IMSELL without cut *)

  Inductive S_imsell : list imsell_form -> imsell_form -> Prop :=

    | in_imsell_ax A : A::nil A (* identity *)

    | in_imsell_perm Γ Δ A : Γ ~p Δ -> Γ A
                                    (*-----------------------------  permutation *)
                                -> Δ A

    | in_imsell_limp_l Γ Δ A B C : Γ A -> B::Δ C
                                    (*-----------------------------  L *)
                                -> AB::Γ++Δ C

    | in_imsell_limp_r Γ A B : A::Γ B
                                    (*-----------------------------  R *)
                                -> Γ AB

    | in_imsell_bang_l Γ m A B : A::Γ B
                                    (*-----------------------------  !L *)
                                -> ![m]A::Γ B

    | in_imsell_bang_r Γ m A : m Γ -> Γ A
                                    (*-----------------------------  !R *)
                                -> Γ ![m]A

    | in_imsell_weak Γ u A B : U u -> Γ B
                                    (*-----------------------------  weakening *)
                                -> ![u]A::Γ B

    | in_imsell_cntr Γ u A B : U u -> ![u]A::![u]A::Γ B
                                    (*-----------------------------  contraction *)
                                -> ![u]A::Γ B

  where "Γ ⊢ A" := (S_imsell Γ A).

End IMSELL.

Infix "⊸" := imsell_imp.
Notation "![ m ] x" := (imsell_ban m x).
Notation "£" := imsell_var.
Notation "‼ Γ" := (imsell_lban Γ).

(* An IMSELL signature is a type of modalities pre-ordered
    and an upper-closed subset of exponentials *)


Record IMSELL_sig : Type :=
  { IMSELL_Λ :> Type;
    IMSELL_le : IMSELL_Λ -> IMSELL_Λ -> Prop;
    IMSELL_refl : forall m, IMSELL_le m m;
    IMSELL_trans : forall u v w, IMSELL_le u v -> IMSELL_le v w -> IMSELL_le u w;
    IMSELL_U : IMSELL_Λ -> Prop;
    IMSELL_clos : forall u v, IMSELL_U u -> IMSELL_le u v -> IMSELL_U v
  }.

Section imsell3.

  (* The minimal signature for this undecidability proof 

     3 modalities {a,b,∞} with a,b < ∞ and ∞ is the only 
     universal modality *)


  Let bang := option bool.

  Let bang_le (u v : bang) :=
    match v with
      | None => True
      | Some _ => u = v
    end.

  Let bang_U := @eq bang None.

  Definition imsell3 : IMSELL_sig.
  Proof.
    exists bang bang_le bang_U; trivial.
    all: repeat intros [[]|]; now simpl.
  Defined.

End imsell3.

Local Infix "≤" := (@IMSELL_le _) (at level 70).
Local Notation "u ≰ v" := (~ u v) (at level 70).
Local Notation U := (@IMSELL_U _).

Definition IMSELL_sig3 :=
  { S : IMSELL_sig | exists a b i : S, a i /\ b i /\ a b /\ b a
                                    /\ ~ U a /\ ~ U b /\ U i }.

Definition IMSELL_problem (S : IMSELL_sig) :=
  let F := imsell_form nat (IMSELL_Λ S) in (list F * F)%type.

Definition IMSELL_problem3 (S : IMSELL_sig3) := IMSELL_problem (proj1_sig S).

(* Cut-free provability over an IMSELL signature *)

Definition IMSELL_cf_PROVABILITY S (P : IMSELL_problem S) :=
  let (Γ,A) := P in S_imsell (IMSELL_le S) (IMSELL_U S) Γ A.

Definition IMSELL_cf_PROVABILITY3 S (P : IMSELL_problem3 S) := IMSELL_cf_PROVABILITY P.