Linear_Lean

import standard
import data.bag
import data.nat data.list.perm algebra.binary
open nat quot list subtype binary function eq.ops
open [decl] perm

namespace linear
open nat fin

namespace Enums

inductive sign : Type :=
 | Pos
 | Neg

notation `#+` := sign.Pos
notation `#-` := sign.Neg

inductive join : Type :=
 | Add
 | Mul

notation `%+` := join.Add
notation `%*` := join.Mul

inductive conj : Type :=
 | Con
 | Dis

notation `@&` := conj.Con
notation `@$` := conj.Dis

prefix `~` := has_neg.neg

definition sign_has_neg [instance]
  : has_neg sign :=
 begin
 constructor 1, intro x, induction x, right, left
 end

end Enums
open Enums

record opclass :=
 mkJC :: (join : join) (conj : conj)

attribute opclass.join [coercion]
attribute opclass.conj [coercion]

namespace opclass
 open Enums

 protected definition f
 : Enums.conj -> Enums.sign
 | @& := #+
 | @$ := #-

 definition sign [coercion]
  : opclass -> Enums.sign :=
   take a : opclass,
   match a with
   | (mkJC %* b) :=    opclass.f b
   | (mkJC %+ b) := ~ (opclass.f b)
   end

 definition mkCS
  : Enums.conj -> Enums.sign -> opclass
 | @& #+ := mkJC %* @&
 | @& #- := mkJC %+ @&
 | @$ #+ := mkJC %+ @$
 | @$ #- := mkJC %* @$

 definition mkJS
  : Enums.join -> Enums.sign -> opclass
 | %+ #+ := mkJC %+ @$
 | %+ #- := mkJC %+ @&
 | %* #+ := mkJC %* @&
 | %* #- := mkJC %* @$

 lemma mkJC_id
  : forall x : linear.opclass
  , x = mkJC x x
  :=
  begin
    intro x
  , cases x
  , all_goals (apply rfl),
  end

  lemma mkJS_id
  : forall x : linear.opclass
  , x = mkJS x x
  :=
  begin
    intro x
  , cases x with J S
    : cases J
    : cases S
    : esimp
  end

  lemma mkCS_id
  : forall x : linear.opclass
  , x = mkCS x x
  :=
  begin
    intro x
  , cases x with J C
    : cases J
    : cases C
    : unfold mkCS
  end

end opclass

inductive MALL (A  : Type) : Type :=
 | Var : bool -> A -> MALL A
 | Null : opclass ->
    MALL A
 | Bi : opclass ->
    MALL A -> MALL A -> MALL A

open MALL

abbreviation MALL.top {A : Type} :=
 Null A (opclass.mkJS %+ #-)
abbreviation MALL.bottom [A : Type] :=
 Null A (opclass.mkJS %* #-)
abbreviation MALL.one [A : Type] :=
 Null A (opclass.mkJS %* #+)
abbreviation MALL.zero  (A : Type) :=
 Null A (opclass.mkJS %+ #+)

definition MALL.has_zero [instance] {A : Type}
 : has_zero (MALL A) :=
  has_zero.mk (MALL.zero A)

definition MALL.has_one [instance] {A : Type}
 : has_one (MALL A) :=
  has_one.mk MALL.one

postfix `^^`:70 := Dual

open MALL

infix `*&`:50 :=
 Bi (opclass.mkJC %* @&)
infix `*$`:50 :=
 Bi (opclass.mkJC %* @$)
infix `+&`:50 :=
 Bi (opclass.mkJC %+ @&)
infix `+$`:50 :=
 Bi (opclass.mkJC %+ @$)

definition two {A} : MALL A := one +$ one

structure seq A :=
 (hypo : bag (MALL A)) (concl : bag (MALL A))

infix `!-`:50 := seq.mk

local notation `[[` a ]]` := bag.of_list [a]

local notation bag' `-:` item := bag.insert item bag'
local notation item `:-` bag := bag.insert item bag'
local notation bag' `++` bag'' := bag.append bag' bag''

section P

parameter {A}
variables D D' G G D1 D2 G1 G2 : bag (MALL A)
variables B B1 B2 : MALL A

inductive P : seq A -> Type :=
 | init :
    P ([[B]] !- [[B]])
 | cut :
    P (D !- (B :- G)) ->
    P ((D' -: B) !- G') ->
    P ((D ++ D') !- (G ++ G'))
 | negL :
    P (D !- (B :- G)) ->
    P ((D -: B^^) !- G)
 | negR :
    P ((D -: B) !- G)) ->
    P (D !- (B^^ :- G))
 | oneL :
    P (D !- G) ->
    P ((D -: one) !- G)
 | oneR :
    P (bag.empty !- [[ one ]])
 | tensorL :
    P ((D ++ [[ B1 ,  B2  ]]) !- G) ->
    P ((D -: (  B1 *& B2  ))  !- G)
 | tensorR :
    P (D1 !- (B1 :- G1)) ->
    P (D2 !- (B2 :- G2)) ->
    P ((D1 ++ D2) !- ((B1 *& B2) :- (G1 ++ G2)))
 | parL :
   P ((D1 -: B1) !- G1) ->
   P ((D2 -: B2) !- G2) ->
   P

end P

end linear