stlc-model11.agda

open import Agda.Builtin.Equality using (_≡_; refl)
open import Data.Nat using (ℕ; _+_; suc)
open import Data.Nat.Properties using (+-cancel-≡; +-comm; +-assoc; _<?_; +-suc)
open import Relation.Nullary using (¬_)
open import Data.Empty using (⊥-elim; ⊥)
open import Data.Unit.Base using (⊤; tt)
open import Agda.Primitive
open import Data.Product
open import Data.Fin hiding (suc; strengthen; _<?_) renaming (_+_ to _Fin+_)
open import Data.Vec
open import Relation.Binary.PropositionalEquality
open import Data.Bool using (true; false)

data `Type : Set where
  `False : `Type
  `Base : `Type
  `Fun : `Type -> `Type -> `Type

data Syn {Var : Set} : Set where
  `base : Syn
  `lam : (Var -> Syn {Var}) -> Syn {Var}
  `app : Syn {Var} -> Syn {Var} -> Syn
  `var : Var -> Syn

data _^_⊢_∈_ (Var : Set) (IsType : Var -> `Type -> Set) : Syn {Var} -> `Type -> Set where

  IVar : ∀ {A} ->
    (m : Var) ->
    (D : (IsType m A)) ->
    -------------------------
    Var ^ IsType ⊢ `var m ∈ A

  IFun-I : ∀ {A B} ->
    {e : (Var -> Syn {Var})} ->
    ((v : Var) -> (D : (IsType v A)) ->
      Var ^ IsType ⊢ (e v) ∈ B) ->
    ----------------------
    Var ^ IsType ⊢ `lam e ∈ `Fun A B

  IFun-E : ∀ {A B e1 e2} ->
    Var ^ IsType ⊢ e1 ∈ `Fun A B ->
    Var ^ IsType ⊢ e2 ∈ A ->
    ------------------
    Var ^ IsType ⊢ `app e1 e2 ∈ B

  IBase-I :
    ----------------
    Var ^ IsType ⊢ `base ∈ `Base

module tests where
  Var : Set
  IsType : Var -> `Type -> Set

  ⊢_∈_ : Syn {Var} -> `Type -> Set
  ⊢_∈_ e A = Var ^ IsType ⊢ e ∈ A

  example1 : ⊢ (`lam `var) ∈ `Fun `Base `Base
  example1 = IFun-I IVar

  example2 : ⊢ (`app (`lam `var) `base) ∈ `Base
  example2 = IFun-E (IFun-I IVar) IBase-I

sub : ∀ {Var : Set} -> Syn {Syn {Var}} -> Syn {Var}
sub `base = `base
sub (`lam f) = `lam λ x → (sub (f (`var x)))
sub (`app e1 e2) = `app (sub e1) (sub e2)
sub (`var e) = e

Term1 = ∀ {Var : Set} -> Var -> Syn {Var}
Term = ∀ {Var : Set} -> Syn {Var}

Sub : Term1 -> Term -> Term
Sub e1 e2 {Var} = sub (e1 {Syn {Var}} (e2 {Var}))

data _⟶_ {Var : Set} : Syn {Syn {Var}} -> Syn {Var} -> Set where
  β : ∀ {f : (Syn {Var}) -> Syn {Syn {Var}}}
    {e2 : Syn {Syn {Var}}} ->
    ----------------------------------------
    (`app (`lam f) e2) ⟶ (sub (f (sub e2)))

  capp1 : ∀ {e1 e2 e1'} ->
    e1 ⟶ e1' ->
    ----------------------------
    (`app e1 e2) ⟶ (`app e1' (sub e2))

  capp2 : ∀ {e1 e2 e2'} ->
    e2 ⟶ e2' ->
    ----------------------------
    (`app e1 e2) ⟶ (`app (sub e1) e2')


module tests' where
  Var : Set
  _ : (`app (`lam `var) `base) ⟶ `base
  _ = β

module Foo where
  Var : Set
  IsType : Var -> `Type -> Set

  ⊢_∈_ : Syn {Var} -> `Type -> Set
  ⊢_∈_ e A = Var ^ IsType ⊢ e ∈ A

  IsType' : (Syn {Var}) -> `Type -> Set
  IsType' e A = ⊢ e ∈ A

  ⊢'_∈_ : Syn {Syn {Var}} -> `Type -> Set
  ⊢'_∈_ e A = Syn {Var} ^ IsType' ⊢ e ∈ A

  sub-lemma : ∀
    {e A} ->
    (⊢' e ∈ A) ->
    (⊢ (sub e) ∈ A)
  sub-lemma (IVar m D) = D
  sub-lemma (IFun-I Df) = IFun-I λ v D → (sub-lemma (Df (`var v) (IVar v D)))
  sub-lemma (IFun-E D D₁) = IFun-E (sub-lemma D) (sub-lemma D₁)
  sub-lemma IBase-I = IBase-I

  subject-reduction : ∀ {A} {e e'} ->
                      (⊢' e ∈ A) -> (e ⟶ e') ->
                      (⊢ e' ∈ A)
  subject-reduction {e = `app (`lam e1) e2} {e' = e'} (IFun-E (IFun-I D) Darg) β =
    (sub-lemma (D (sub e2) (sub-lemma Darg)))
  subject-reduction {e = `app e1 e2} (IFun-E D D₁) (capp1 step) =
    IFun-E (subject-reduction D step) (sub-lemma D₁)
  subject-reduction {e = `app e1 e2} (IFun-E D D₁) (capp2 step) =
    IFun-E (sub-lemma D) (subject-reduction D₁ step)