IPL.agda

module IPL where



infixr 90 _&_
infixr 80 _v_
infixr 70 _=>_

data Proposition : Set where
  True : Proposition
  _&_ _v_ _=>_ : Proposition -> Proposition -> Proposition

infix 60 _true
data Judgment : Set where
  _true : Proposition -> Judgment

infixl 50 _,_
data Context : Set where
  <> : Context
  _,_ : Context -> Judgment -> Context


infix 40 _ni_
data _ni_ : (G : Context) -> (J : Judgment) -> Set where
  here : forall {G J} -> G , J ni J
  there : forall {G J K} -> G ni J -> G , K ni J

wkG : forall {G J K} -> G ni J -> G , K ni J
wkG = there

cnG : forall {G J K} -> G , K , K ni J -> G , K ni J
cnG here = here
cnG (there pf) = pf

exG : forall {G J K L} -> G , K , L ni J -> G , L , K ni J
exG here = there here
exG (there here) = here
exG (there (there pf)) = there (there pf)

subG : forall {G J K} -> G ni J -> G , J ni K -> G ni K
subG pf here = pf
subG pf (there pf') = pf'

{-
ex for G !- J
  hyp of some G ni J -- ex on ni
  &-I ???
-}

infix 40 _!-_
data _!-_ (G : Context) : (J : Judgment) -> Set where

  hyp : forall {J} ->    G ni J
                         ------
                   ->    G !- J

  -- True
  True-I : G !- True true

  -- &
  &-I : forall {A B} ->    G !- A true   ->   G !- B true
                           ------------------------------
                     ->           G !- A & B true
  
  &-E-1 : forall {A B} ->   G !- A & B true
                            ---------------
                       ->     G !- A true

  &-E-2 : forall {A B} ->   G !- A & B true
                            ---------------
                       ->     G !- B true

  -- =>
  =>-I : forall {A B} ->   G , A true !- B true
                           --------------------
                      ->     G !- A => B true

  =>-E : forall {A B} ->   G !- A => B true   ->   G !- A true
                           -----------------------------------
                      ->               G !- B true

  -- v
  v-I-1 : forall {A B} ->     G !- A true
                            ---------------
                       ->   G !- A v B true

  v-I-2 : forall {A B} ->     G !- B true
                            ---------------
                       ->   G !- A v B true

  v-E : forall {A B C} ->    G !- A v B true   ->   G , A true !- C true   ->   G , B true !- C true
                             -----------------------------------------------------------------------
                       ->                                G !- C true



extend : forall {G D K} -> (r : forall {J} -> G ni J -> D ni J) -> (forall {J} -> G , K ni J -> D , K ni J)
extend r here = here
extend r (there pf) = there (r pf)

ren : forall {G D J} -> (r : forall {K} -> G ni K -> D ni K) -> G !- J -> D !- J
ren r (hyp x) = hyp (r x)
ren r True-I = True-I
ren r (&-I M N) = &-I (ren r M) (ren r N)
ren r (&-E-1 P) = &-E-1 (ren r P)
ren r (&-E-2 P) = &-E-2 (ren r P)
ren r (=>-I M) = =>-I (ren (extend r) M)
ren r (=>-E M N) = =>-E (ren r M) (ren r N)
ren r (v-I-1 M) = v-I-1 (ren r M)
ren r (v-I-2 N) = v-I-2 (ren r N)
ren r (v-E D M N) = v-E (ren r D) (ren (extend r) M) (ren (extend r) N)

weaken : forall {G K J} -> G !- J -> G , K !- J
weaken = ren there


extendSub : forall {G D K} -> (r : forall {J} -> G ni J -> D !- J) -> (forall {J} -> G , K ni J -> D , K !- J)
extendSub r here = hyp here
extendSub r (there pf) = weaken (r pf)

sub : forall {G D J} -> (r : forall {K} -> G ni K -> D !- K) -> G !- J -> D !- J
sub r (hyp x) = r x
sub r True-I = True-I
sub r (&-I M N) = &-I (sub r M) (sub r N)
sub r (&-E-1 P) = &-E-1 (sub r P)
sub r (&-E-2 P) = &-E-2 (sub r P)
sub r (=>-I M) = =>-I (sub (extendSub r) M)
sub r (=>-E M N) = =>-E (sub r M) (sub r N)
sub r (v-I-1 M) = v-I-1 (sub r M)
sub r (v-I-2 N) = v-I-2 (sub r N)
sub r (v-E D M N) = v-E (sub r D) (sub (extendSub r) M) (sub (extendSub r) N)



lemma : forall {G A B} -> G !- A & B true -> G !- B & A true
lemma pf = &-I (&-E-2 pf) (&-E-1 pf)

lemma1,5 : forall {A} -> <> !- A => A true
lemma1,5 = =>-I (hyp here)

lemma2 : forall {A B} -> <> !- A & B => B & A true
lemma2 = =>-I (&-I (&-E-2 (hyp here)) (&-E-1 (hyp here)))

lemma3 : forall {A B C} -> <> !- (A => (B => C)) => (B => (A => C)) true
lemma3 = {!!}

lemma4 : forall {A B} -> <> !- A => ((A => B) => B) true
lemma4 = {!!}

lemma5 : forall {A B C} -> <> !- (A => B) => ((B => C) => (A => C)) true
lemma5 = {!!}

lemma6f : forall {A B C} -> <> !- ((A & B) => C) => (A => (B => C)) true
lemma6f = {!!}

lemma6b : forall {A B C} -> <> !- (A => (B => C)) => ((A & B) => C) true
lemma6b = {!!}

lemma7 : forall {A B C} -> <> !- (A => (B & C)) => (A => B) & (A => C) true
lemma7 = {!!}

lemma8 : forall {A B C} -> <> !- ((A v B) => C) => (A => C) & (B => C) true
lemma8 = {!!}