SystemF-Proof-Theory.agda

module SystemF-Proof-Theory where


open import Data.Bool hiding (if_then_else_ ; _≟_)
open import Data.String
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary



data Type : Set where
  Zero One Two : Type
  _*_ _=>_ : Type -> Type -> Type
  free : String -> Type
  bound : String -> Type
  all : String -> Type -> Type



openAsType : String -> Type -> String -> Type
openAsType x Zero x' = Zero
openAsType x One x' = One
openAsType x Two x' = Two
openAsType x (A * A') x' = openAsType x A x' * openAsType x A' x'
openAsType x (A => A') x' = openAsType x A x' => openAsType x A' x'
openAsType x (free y) x' = free y
openAsType x (bound y) x' with x ≟ y
openAsType x (bound y) x' | yes p = free x'
openAsType x (bound y) x' | no ¬p = bound y
openAsType x (all y A) x' with x ≟ y
openAsType x (all y A) x' | yes p = all y A
openAsType x (all y A) x' | no ¬p = all y (openAsType x A x')

substituteType : Type -> String -> Type -> Type
substituteType A x Zero = Zero
substituteType A x One = One
substituteType A x Two = Two
substituteType A x (B * B') = substituteType A x B * substituteType A x B'
substituteType A x (B => B') = substituteType A x B => substituteType A x B'
substituteType A x (free y) with x ≟ y
substituteType A x (free y) | yes p = A
substituteType A x (free y) | no ¬p = free y
substituteType A x (bound y) = bound y
substituteType A x (all y B) = all y (substituteType A x B)



data HJudgment : Set where
  _::_ : String -> Type -> HJudgment
  _type : String -> HJudgment

data Cx : Set where
  <> : Cx
  _,_ : Cx -> HJudgment -> Cx

data Var : Cx -> HJudgment -> Set where
  top : forall {G J} -> Var (G , J) J
  pop : forall {G J' J} -> Var G J -> Var (G , J') J

data Term : Set where
  free : String -> Term
  bound : String -> Term
  <> : Term
  abort : Term -> Term
  true false : Term
  if_then_else_ : Term -> Term -> Term -> Term
  <_,_> : Term -> Term -> Term
  fst snd : Term -> Term
  lam : String -> Term -> Term
  _$_ : Term -> Term -> Term
  abs : String -> Term -> Term
  inst : Term -> Type -> Term


openAs : String -> Term -> String -> Term
openAs x (free y) x' = free y
openAs x (bound y) x' with x ≟ y
openAs x (bound y) x' | yes p = free x'
openAs x (bound y) x' | no ¬p = bound y
openAs x <> x' = <>
openAs x (abort M) x' = abort (openAs x M x')
openAs x true x' = true
openAs x false x' = false
openAs x (if M then M' else M'') x' = if openAs x M x' then openAs x M' x' else openAs x M'' x'
openAs x < M , M' > x' = < openAs x M x' , openAs x M' x' >
openAs x (fst M) x' = fst (openAs x M x')
openAs x (snd M) x' = snd (openAs x M x')
openAs x (lam y M) x' with x ≟ y
openAs x (lam y M) x' | yes p = lam y M
openAs x (lam y M) x' | no ¬p = lam y (openAs x M x')
openAs x (M $ M') x' = openAs x M x' $ openAs x M' x'
openAs x (abs y M) x' with x ≟ y
openAs x (abs y M) x' | yes p = abs y M
openAs x (abs y M) x' | no ¬p = abs y (openAs x M x')
openAs x (inst M B) x' = inst (openAs x M x') (openAsType x B x')

data Fresh : Cx -> String -> Set where
  <>-fresh : forall {x} -> Fresh <> x
  ::-fresh : forall {G x y A} -> Fresh G x -> ¬ x ≡ y -> Fresh (G , (y :: A)) x
  type-fresh : forall {G x y} -> Fresh G x -> ¬ x ≡ y -> Fresh (G , (y type)) x


data IsType : Cx -> Type -> Set where
  hyp : forall {G x} -> Var G (x type) -> IsType G (free x)
  Zero-F : forall {G} -> IsType G Zero
  One-F : forall {G} -> IsType G One
  Two-F : forall {G} -> IsType G Two
  Prod-F : forall {G A B} -> IsType G A -> IsType G B -> IsType G (A * B)
  Fun-F : forall {G A B} -> IsType G A -> IsType G B -> IsType G (A => B)
  Forall-F : forall {G A x x'} -> Fresh G x' -> IsType (G , (x' type)) (openAsType x A x') -> IsType G (all x A)

data HasType : Cx -> Term -> Type -> Set where
  hyp : forall {G x A} -> Var G (x :: A) -> HasType G (free x) A
  Zero-E : forall {G M C} -> HasType G M Zero -> HasType G (abort M) C
  One-I : forall {G} -> HasType G <> One
  Two-I-1 : forall {G} -> HasType G true Two
  Two-I-2 : forall {G} -> HasType G false Two
  Two-E : forall {G M N P C} -> HasType G M Two -> HasType G N C -> HasType G P C -> HasType G (if M then N else P) C
  Prod-I : forall {G M N A B} -> HasType G M A -> HasType G N B -> HasType G < M , N > (A * B)
  Prod-E-1 : forall {G M A B} -> HasType G M (A * B) -> HasType G (fst M) A
  Prod-E-2 : forall {G M A B} -> HasType G M (A * B) -> HasType G (snd M) B
  Fun-I : forall {G M A B x} x' -> Fresh G x' -> HasType (G , (x' :: A)) (openAs x M x') B -> HasType G (lam x M) (A => B)
  Fun-E : forall {G M N A B} -> HasType G M (A => B) -> HasType G N A -> HasType G (M $ N) B
  Forall-I : forall {G M A x x'} x'' -> Fresh G x'' -> HasType (G , (x'' type)) (openAs x M x'') (openAsType x' A x'') -> HasType G (abs x M) (all x' A)
  Forall-E : forall {G M A B x} x' -> Fresh G x' -> HasType G M (all x A) -> IsType G B -> HasType G (inst M B) (substituteType B x' (openAsType x A x'))

  



id-proof : HasType <> (abs "a" (lam "x" (bound "x"))) (all "a" (bound "a" => bound "a"))
id-proof = Forall-I "a" <>-fresh (Fun-I "x" (type-fresh <>-fresh (\ ())) (hyp top))

swap-proof : HasType <> (abs "a" (abs "b" (lam "p" < snd (bound "p") , fst (bound "p") >))) (all "a" (all "b" ((bound "a" * bound "b") => (bound "b" * bound "a"))))
swap-proof = Forall-I "a" <>-fresh (Forall-I "b" (type-fresh <>-fresh (\ ())) (Fun-I "p" (type-fresh (type-fresh <>-fresh (\())) (\())) (Prod-I (Prod-E-2 (hyp top)) (Prod-E-1 (hyp top)))))

eta-id : HasType <> (abs "b" (lam "y" (inst (abs "a" (lam "x" (bound "x"))) (bound "b") $ bound "y"))) (all "b" (bound "b" => bound "b"))
eta-id = Forall-I "b" <>-fresh (Fun-I "y" (type-fresh <>-fresh (\ ())) (Fun-E id-proof' (hyp top)))
  where
    id-proof' : HasType ((<> , ("b" type)) , ("y" :: free "b")) (inst (abs "a" (lam "x" (bound "x"))) (free "b")) (free "b" => free "b")
    id-proof' = Forall-E {A = bound "a" => bound "a"} {x = "a"} "a" (::-fresh (type-fresh <>-fresh (\ ())) (\ ())) (Forall-I "a" (::-fresh (type-fresh <>-fresh (\ ())) (\ ())) (Fun-I "x" (type-fresh (::-fresh (type-fresh <>-fresh (\ ())) (\ ())) (\ ())) (hyp top))) (hyp (pop top))