iris/BidirTT/Examples.lean

import BidirTT.Syntax

namespace BidirTT.Examples

open BidirTT

def idTy : Raw :=
  .pi "A" (.univ 0) (.pi "_" (.var "A") (.var "A"))

def idTm : Raw :=
  .lam "A" (.lam "x" (.var "x"))

def idAnn : Raw := .ann idTm idTy

def constTy : Raw :=
  .pi "A" (.univ 0) (.pi "B" (.univ 0)
    (.pi "_" (.var "A") (.pi "_" (.var "B") (.var "A"))))

def constTm : Raw :=
  .lam "A" (.lam "B" (.lam "x" (.lam "_" (.var "x"))))

def constAnn : Raw := .ann constTm constTy

def swapTy : Raw :=
  .pi "A" (.univ 0) (.pi "B" (.univ 0)
    (.pi "_" (.sig "_" (.var "A") (.var "B"))
             (.sig "_" (.var "B") (.var "A"))))

def swapTm : Raw :=
  .lam "A" (.lam "B" (.lam "p"
    (.pair (.snd (.var "p")) (.fst (.var "p")))))

def swapAnn : Raw := .ann swapTm swapTy

def depPairTy : Raw :=
  .sig "A" (.univ 2) (.var "A")

def depPairTm : Raw :=
  .pair
    (.univ 1)
    (.pi "_" (.univ 0) (.univ 0))

def depPairAnn : Raw := .ann depPairTm depPairTy

def fstDepPair : Raw := .fst depPairAnn

def sndDepPair : Raw := .snd depPairAnn

def univMax : Raw := .univ (.max 0 1)

def natTwo : Raw :=
  .succ (.succ .zero)

def natFoldId : Raw :=
  .ann
    (.natElim "n" .nat .zero "k" "ih" (.succ (.var "ih")) natTwo)
    .nat

def unitToNat : Raw :=
  .ann
    (.unitElim "u" .nat natTwo .triv)
    .nat

def absurdNat : Raw :=
  .ann
    (.lam "e" (.emptyElim "x" .nat (.var "e")))
    (.pi "e" .empty .nat)

def reflZero : Raw :=
  .ann .refl (.id .nat .zero .zero)

def idElimNat : Raw :=
  .ann
    (.idElim "y" "p" .nat .zero .zero reflZero)
    .nat

def transportNatTy : Raw :=
  .pi "x" .nat
    (.pi "y" .nat
      (.pi "p" (.id .nat (.var "x") (.var "y"))
        (.pi "z" .nat .nat)))

def transportNatTm : Raw :=
  .lam "x" (.lam "y" (.lam "p" (.lam "z"
    (.idElim "y'" "p'" .nat (.var "z") (.var "y") (.var "p")))))

def transportNat : Raw := .ann transportNatTm transportNatTy

def transportNatRefl : Raw :=
  .ann
    (.app (.app (.app (.app transportNat .zero) .zero) reflZero) natTwo)
    .nat

def congSuccTy : Raw :=
  .pi "x" .nat
    (.pi "y" .nat
      (.pi "p" (.id .nat (.var "x") (.var "y"))
        (.id .nat (.succ (.var "x")) (.succ (.var "y")))))

def congSuccTm : Raw :=
  .lam "x" (.lam "y" (.lam "p"
    (.idElim "y'" "p'"
      (.id .nat (.succ (.var "x")) (.succ (.var "y'")))
      .refl
      (.var "y")
      (.var "p"))))

def congSucc : Raw := .ann congSuccTm congSuccTy

def congSuccRefl : Raw :=
  .ann
    (.app (.app (.app congSucc .zero) .zero) reflZero)
    (.id .nat (.succ .zero) (.succ .zero))

def omegaTy : Raw :=
  .pi "A" (.univ 0) (.var "A")

def omegaTm : Raw :=
  .lam "x" (.app (.var "x") (.var "x"))

def omegaAnn : Raw := .ann omegaTm omegaTy

def unknownVar : Raw := .var "nope"

def pairMismatch : Raw :=
  .ann (.pair (.univ 1) (.univ 1))
       (.sig "A" (.univ 2) (.var "A"))

def badFst : Raw := .fst (.univ 0)

def letUniverse : Raw :=
  .ann
    (.letE "A" (.univ 1) (.pi "_" (.univ 0) (.univ 0)) (.var "A"))
    (.univ 1)

def badSucc : Raw := .succ (.univ 0)

def badRefl : Raw :=
  .ann .refl (.id .nat .zero (.succ .zero))

def univ0 : Raw := .univ 0

end BidirTT.Examples