Library BioFLL.LL.SequentCalculi

Sequent Calculi

Focused system for first order focused linear logic.

Require Export Permutation.
Require Import Coq.Relations.Relations.
Require Import Coq.Arith.EqNat.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Setoids.Setoid.
Require Export Coq.Sorting.PermutSetoid.
Require Export Coq.Sorting.PermutEq.
Require Import Coq.Program.Equality.
Require Import Coq.Logic.FunctionalExtensionality.
Require Export LL.StrongInduction.
Require Export LL.Syntax.
Require Import LL.Eqset.

Set Implicit Arguments.

Module SqSystems (DT : Eqset_dec_pol).

Module Export SxLL := FormulasLL DT.
Export DT.

Arrows of the focused system: UP for the negative phase and DW for the positive phase.

  Inductive Arrow :=
  | UP (l : list Lexp)
  | DW (F : Lexp).

  Definition Arrow2LL (A: Arrow) : list Lexp :=
    match A with
    | UP l ⇒ l
    | DW F ⇒ [F]
    end.

  Lemma Arrow_eq_dec : ∀ F1 F2: Arrow , {F1 =F2 } + {F1 ≠ F2 }.
    intros.
    destruct F1;destruct F2.
    generalize(list_eq_dec FEqDec l l0);intro.
    destruct H;subst;auto. right; intuition. apply n;intuition. inversion H;auto.
    right;intro. inversion H.
    right;intro. inversion H.
    generalize(FEqDec F F0);intro.
    destruct H;subst;auto. right;intuition. apply n;inversion H;auto.
  Qed.

Triadic system for first order focused linear logic

  Reserved Notation " '|-F-' B ';' L ';' X " (at level 80).

  Inductive TriSystem: list Lexp → list Lexp → Arrow → Prop :=
  | tri_init1 : ∀ B A, IsNegativeAtom A → |-F - B ; [(Dual_LExp A )] ; DW (A)
  | tri_init2 : ∀ B B' A, IsNegativeAtom A → B =mul = (Dual_LExp A ) :: B' → |-F - B ; [] ; DW (A)
  | tri_one : ∀ B, |-F - B ; [] ; DW One
  | tri_tensor : ∀ B M N MN F G,
      MN =mul = M ++ N → |-F - B ; N ; DW F → |-F - B ; M ; DW G → |-F - B ; MN ; DW (F ** G)
  | tri_plus1 : ∀ B M F G, |-F - B ; M ; DW F → |-F - B ; M ; DW (F ⊕ G)
  | tri_plus2 : ∀ B M F G, |-F - B ; M ; DW G → |-F - B ; M ; DW (F ⊕ G)
  | tri_bang : ∀ B F, |-F - B ; [] ; UP [F ] → |-F - B ; [] ; DW (! F)
  | tri_rel : ∀ B F L, Release F → |-F - B ; L ; UP [F ] → |-F - B ; L ; DW F

  | tri_top : ∀ B L M, |-F - B ; L ; UP (Top :: M)
  | tri_bot : ∀ B L M, |-F - B ; L ; UP M → |-F - B ; L ; UP (Bot :: M)
  | tri_par : ∀ B L M F G, |-F - B ; L ; UP (F ::G ::M) → |-F - B ; L ; UP(F $ G :: M)
  | tri_with : ∀ B L M F G,
      |-F - B ; L ; UP (F :: M) → |-F - B ; L ; UP (G :: M) → |-F - B ; L ; UP (F & G :: M)
  | tri_quest : ∀ B L M F, |-F - B ++ [F ] ; L ; UP M → |-F - B ; L ; UP (? F :: M)
  | tri_store : ∀ B L M F, ¬ Asynchronous F → |-F - B ; L ++ [F ] ; UP M → |-F - B ; L ; UP (F ::M)
  | tri_dec1 : ∀ B L L' F, ¬IsPositiveAtom F → L =mul = F :: L' → |-F - B ; L' ; DW F →|-F - B ; L ; UP []
  | tri_dec2 : ∀ B B' L F, ¬IsPositiveAtom F → B =mul = F :: B' → |-F - B ; L ; DW F → |-F - B ; L ; UP []
  | tri_ex : ∀ B FX M t, |-F - B ; M ; DW (Subst FX t) → |-F - B ; M ; DW (E {FX })
  | tri_fx : ∀ B L FX M, (∀ x, |-F - B ; L ; UP( (Subst FX x ) :: M)) → |-F - B ; L ; UP (F {FX } :: M)
  where " '|-F-' B ';' L ';' X " := (TriSystem B L X).
  Hint Constructors TriSystem.

Triadic system with a measure on the height of derivations

  Reserved Notation " n '|-F-' B ';' L ';' X " (at level 80).
  Inductive TriSystemh: nat → list Lexp → list Lexp → Arrow → Prop :=
  | trih_init1 : ∀ B A n, IsNegativeAtom A → n |-F - B ; [(Dual_LExp A )] ; DW (A)
  | trih_init2 : ∀ B B' A n, IsNegativeAtom A → B =mul = (Dual_LExp A ) :: B' → n |-F - B ; [] ; DW (A)
  | trih_one : ∀ B n, n |-F - B ; [] ; DW One
  | trih_tensor : ∀ B M N MN F G n,
      MN =mul = M ++ N → n |-F - B ; N ; DW F → n |-F - B ; M ; DW G → S n |-F - B ; MN ; DW (F ** G)
  | trih_plus1 : ∀ B M F G n, n |-F - B ; M ; DW F → S n |-F - B ; M ; DW (F ⊕ G)
  | trih_plus2 : ∀ B M F G n, n |-F - B ; M ; DW G → S n |-F - B ; M ; DW (F ⊕ G)
  | trih_bang : ∀ B F n, n |-F - B ; [] ; UP [F ] → S n |-F - B ; [] ; DW (! F)
  | trih_rel : ∀ B F L n, Release F → n |-F - B ; L ; UP [F ] → S n |-F - B ; L ; DW F

  | trih_top : ∀ B L M n, n |-F - B ; L ; UP (Top :: M)
  | trih_bot : ∀ B L M n, n |-F - B ; L ; UP M → S n |-F - B ; L ; UP (Bot :: M)
  | trih_par : ∀ B L M F G n, n |-F - B ; L ; UP (F ::G ::M) → S n |-F - B ; L ; UP(F $ G :: M)
  | trih_with : ∀ B L M F G n,
      n |-F - B ; L ; UP (F :: M) → n |-F - B ; L ; UP (G :: M) → S n |-F - B ; L ; UP (F & G :: M)
  | trih_quest : ∀ B L M F n, n |-F - B ++ [F ] ; L ; UP M → S n |-F - B ; L ; UP (? F :: M)
  | trih_store : ∀ B L M F n, ¬ Asynchronous F → n |-F - B ; L ++ [F ] ; UP M → S n |-F - B ; L ; UP (F ::M)
  | trih_dec1 : ∀ B L L' F n, ¬IsPositiveAtom F → L =mul = F :: L' → n |-F - B ; L' ; DW F → S n |-F - B ; L ; UP []
  | trih_dec2 : ∀ B B' L F n, ¬IsPositiveAtom F → B =mul = F :: B' → n |-F - B ; L ; DW F → S n |-F - B ; L ; UP []
  | trih_ex : ∀ B n FX M t,
      n |-F - B ; M ; DW (Subst FX t) → S n |-F - B ; M ; DW (E {FX })
  | trih_fx :
      ∀ B L n FX M,
        (∀ x : Term, n |-F - B ; L ; UP( (Subst FX x ) :: M)) → S n |-F - B ; L ; UP (F {FX } :: M)
  where " n '|-F-' B ';' L ';' X " := (TriSystemh n B L X).
  Hint Constructors TriSystemh.
End SqSystems.