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

(* Certified Undecidability of Intuitionistic Linear Logic via Binary Stack Machines and Minsky Machines. Yannick Forster and Dominique Larchey-Wendling. CPP '19. http://uds-psl.github.io/ill-undecidability/ *)

Require Import List Permutation.

From Undecidability.ILL Require Import ILL.

Set Implicit Arguments.

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

Notation eill_vars := nat.

Inductive eill_cmd : Set :=
  | in_eill_cmd_inc : eill_vars -> eill_vars -> eill_vars -> eill_cmd
  | in_eill_cmd_dec : eill_vars -> eill_vars -> eill_vars -> eill_cmd
  | in_eill_cmd_fork : eill_vars -> eill_vars -> eill_vars -> eill_cmd.

Notation LL_INC := in_eill_cmd_inc.
Notation LL_DEC := in_eill_cmd_dec.
Notation LL_FORK := in_eill_cmd_fork.

Definition eill_cmd_vars c :=
  match c with
    | LL_INC a p q => a::p::q::nil
    | LL_DEC a p q => a::p::q::nil
    | LL_FORK p q r => p::q::r::nil
  end.

(* The embedding of eill commands into ill 
   or its (!,&,-o) fragment *)


Definition eill_cmd_map c :=
  match c with
    | LL_INC a p q => (£a £p) £ q
    | LL_DEC a p q => £a £p £ q
    | LL_FORK p q r => (£p & £q) £ r
  end.

(* Symbols for cut&paste ⟙   ⟘   𝝐  ﹠ ⊗  ⊕  ⊸  !  ‼  ∅  ⊢ ⟦ ⟧ Γ Δ Σ *)

Section GeILL.

  Reserved Notation "Σ ; Γ ⊦ u" (at level 70, no associativity).

  Inductive G_eill (Σ : list eill_cmd) : list eill_vars -> eill_vars -> Prop :=
    | in_geill_ax : forall u, Σ; u:: u
    | in_geill_perm : forall Γ Δ p, Γ ~p Δ -> Σ; Γ p
                                                              -> Σ; Δ p
    | in_geill_inc : forall Γ a p q, In (LL_INC a p q) Σ -> Σ; a::Γ p
                                                              -> Σ; Γ q
    | in_geill_dec : forall Γ Δ p q r, In (LL_DEC p q r) Σ -> Σ; Γ p
                                                              -> Σ; Δ q
                                                              -> Σ; Γ++Δ r
    | in_geill_fork : forall Γ p q r, In (LL_FORK p q r) Σ -> Σ; Γ p
                                                              -> Σ; Γ q
                                                              -> Σ; Γ r
  where "Σ ; Γ ⊦ u" := (G_eill Σ Γ u).

End GeILL.

Definition EILL_SEQUENT := (list eill_cmd * list eill_vars * eill_vars)%type.

Definition EILL_PROVABILITY (c : EILL_SEQUENT) := match c with (Σ,Γ,u) => G_eill Σ Γ u end.