Skip to content

Instantly share code, notes, and snippets.

@BekaValentine
Created May 14, 2023 00:18
Show Gist options
  • Save BekaValentine/893aded0e1d9f27e8ff7880478abf9fb to your computer and use it in GitHub Desktop.
Save BekaValentine/893aded0e1d9f27e8ff7880478abf9fb to your computer and use it in GitHub Desktop.
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 = {!!}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment