-- Non-Commutative Linear Lambda Calculus
--
-- Relations and non-commutative linear logic
-- by Carolyn Brown, Doug Gurr
-- https://www.sciencedirect.com/science/article/pii/0022404994001472
--
-- Frank Pfenning's lectures on logic influeced the proof making.
-- The proof is essentially the same as his proof for STLC,
-- yet in Agda (not informal / Twelf) and for NCILL.
-- Cut-Elimination proof for NCILL is easy to mechanize, as
-- contexts are lists, not sets (STLC) or multisets (ILL).
--
-- Rendered HTML docs are at http://oleg.fi/ncill/
-- Source code is at https://github.com/phadej/ncill
--
module NCILL.README where

-- Non-commutative Intuitinistic Linear Logic
------------------------------------------------------------------------
--
-- ∙ Types

import NCILL.Types

-- ∙ Context is just a set of types: Ctx = List Ty

import NCILL.Ctx

-- ∙ Sqnt are sequents

import NCILL.Sequent

-- ∙ Sqnt⁺ are sequents with Cut

import NCILL.SequentPlus

-- ∙ We prove Cut Elimination Theorem (Soundness), Completeness is trivial

import NCILL.Cut

-- ⋯ using Admissibility of Cut lemma

import NCILL.Admit

-- ∙ For development, you can

import NCILL

-- Examples
------------------------------------------------------------------------

-- ∙ We show terms for many equivalences in NCILL:
--   ∘ Quantale structure: Monoids of ⊗ and ♯1; ⊕ and ♯0; & and ♯⊤,
--     distributivity
--   ∘ More equivalences from Girard's Linear Logic (only ⊗-comm doesn't hold!)
--   ∘ Example of difference between ⊸ and ⊸ʳ
--
import NCILL.Examples.Equivalences

-- ∙ Though CUT is admissible in NCILL, η-reductions aren't performed.
--   This example shows ⊗ η and β -reductions.
--   ∘ original and η-reduced term aren't the same, yet logically they are 
--   ∘ β involves CUT, and terms are definitionally equal
--   ∘ we compare that to Agda's own behaviour
--
import NCILL.Examples.EtaBeta

-- Extras
------------------------------------------------------------------------

-- ∙ there are some extras to write the proofs

import ListExtras          -- few additional list related lemmas
import Simple-list-solver  -- solver for list concatenations (simpler to use than monoid-solver)
import AssocProofs         -- associativity lemmas up to 5 arguments "pre-proved"