第3部　型付き計算の理論

open FormalLab.Foundation.UntypedLambdaCalculus
open FormalLab.TypeTheory.SimplyTypedLambdaCalculus

example (A : SimpleType) : HasType [] identity (A ⇒ A) :=
  .lam (.var .zero)

example (A B : SimpleType) : HasType [] constant (A ⇒ B ⇒ A) :=
  .lam (.lam (.var (.succ .zero)))

example (A : SimpleType) : HasType [] (.app identity identity) (A ⇒ A) :=
  .app (identity_has_type (A ⇒ A)) (identity_has_type A)

open FormalLab.Foundation.UntypedLambdaCalculus
open FormalLab.TypeTheory.SimplyTypedLambdaCalculus

def applyTerm : Term :=
  .lam (.lam (.app (.var 1) (.var 0)))

theorem applyTermHasType (A B : SimpleType) :
    HasType [] applyTerm ((A ⇒ B) ⇒ A ⇒ B) :=
  .lam (.lam (.app (.var (.succ .zero)) (.var .zero)))

example (X Y : SimpleType) : X ≠ X ⇒ Y :=
  X.ne_self_arrow Y

variable {Term Ty : Type}

def Preservation (HasType : Term → Ty → Prop) (Step : Term → Term → Prop) : Prop :=
  ∀ ⦃term next type⦄, HasType term type → Step term next → HasType next type

def Progress (HasType : Term → Ty → Prop) (Step : Term → Term → Prop)
    (Value : Term → Prop) : Prop :=
  ∀ ⦃term type⦄, HasType term type → Value term ∨ ∃ next, Step term next

def Stuck (Step : Term → Term → Prop) (Value : Term → Prop) (term : Term) : Prop :=
  ¬Value term ∧ ¬∃ next, Step term next

#check FormalLab.TypeTheory.StructuralRules.weakenFront
#check FormalLab.TypeTheory.StructuralRules.exchangeFront
#check FormalLab.TypeTheory.StructuralRules.contraction
#check FormalLab.TypeTheory.StructuralRules.substituteTop

open FormalLab.TypeTheory.SimplyTypedLambdaCalculus
open FormalLab.TypeTheory.StructuralRules

def outerVariableUnderBinder (A C : SimpleType) : Tm [A] (C ⇒ A) :=
  .lam (.var (.succ .zero))

example {A C : SimpleType} (argument : Tm [] A) :
    substituteTop (B := C ⇒ A) argument (outerVariableUnderBinder A C) =
      .lam (weakenFront (B := C) argument) := rfl

open FormalLab.Foundation.UntypedLambdaCalculus
open FormalLab.TypeTheory.OperationalSemantics

def threeApplications : Term :=
  .app (.app identity identity) constant

example : step? threeApplications = some (.app identity constant) := rfl
example : step? (.app identity constant) = some constant := rfl
example : step? constant = none := rfl

open FormalLab.Foundation.UntypedLambdaCalculus
open FormalLab.TypeTheory.OperationalSemantics

theorem step?_complete {term next : Term}
    (reduction : FormalLab.TypeTheory.OperationalSemantics.Step term next) :
    step? term = some next := by
  induction term generalizing next with
  | var index => cases reduction
  | lam body => cases reduction
  | app function argument functionIH argumentIH =>
      cases reduction with
      | beta value => cases value; rfl
      | appLeft functionStep =>
          cases function with
          | var index => cases functionStep
          | lam body => exact False.elim (valueCannotStep .lam functionStep)
          | app left right =>
              change (match step? (.app left right) with
                | some function' => some (Term.app function' argument)
                | none => none) = _
              rw [functionIH functionStep]
      | appRight functionValue argumentStep =>
          cases functionValue
          cases argument with
          | var index => cases argumentStep
          | lam body => exact False.elim (valueCannotStep .lam argumentStep)
          | app left right =>
              change (match step? (.app left right) with
                | some argument' => some (Term.app (Term.lam _) argument')
                | none => none) = _
              rw [argumentIH argumentStep]

theorem stepDeterministic {term first second : Term}
    (left : FormalLab.TypeTheory.OperationalSemantics.Step term first)
    (right : FormalLab.TypeTheory.OperationalSemantics.Step term second) : first = second := by
  have leftResult := step?_complete left
  have rightResult := step?_complete right
  rw [leftResult] at rightResult
  exact Option.some.inj rightResult

open FormalLab.TypeTheory.RecursiveTypes

def listBody (element : RType) : RType :=
  .sum .unit (.product element (.bound 0))

def emptyList (element : RType) : Term :=
  .roll (listBody element) (.inl .unit)

def unitListBody : RType := listBody .unit

def emptyUnitList : Term := emptyList .unit

def prepend (element : RType) (head tail : Term) : Term :=
  .roll (listBody element) (.inr (.pair head tail))

def prependUnit (tail : Term) : Term := prepend .unit .unit tail

def twoUnitList : Term := prependUnit (prependUnit emptyUnitList)

theorem emptyUnitListHasType : HasType emptyUnitList (.mu unitListBody) := by
  exact .roll (.inl .unit)

theorem prependUnitHasType {tail : Term} (typedTail : HasType tail (.mu unitListBody)) :
    HasType (prependUnit tail) (.mu unitListBody) := by
  exact .roll (.inr (.pair .unit typedTail))

theorem twoUnitListHasType : HasType twoUnitList (.mu unitListBody) := by
  exact prependUnitHasType (prependUnitHasType emptyUnitListHasType)

example : HasType zero recursiveNat := zero_typed
example : HasType (successor zero) recursiveNat := one_typed

example : HasType (.inl .unit) (unfoldType natBody) :=
  preservation (.unroll zero_typed) (.cancel (.inl .unit))

example : HasType (.inl .unit) (unfoldType unitListBody) :=
  preservation (.unroll emptyUnitListHasType) (.cancel (.inl .unit))

open FormalLab.TypeTheory.RecursiveTypes

def naiveSubstitute (target : Nat) (replacement : RType) : RType → RType
  | .unit => .unit
  | .sum left right =>
      .sum (naiveSubstitute target replacement left)
        (naiveSubstitute target replacement right)
  | .product left right =>
      .product (naiveSubstitute target replacement left)
        (naiveSubstitute target replacement right)
  | .arrow domain codomain =>
      .arrow (naiveSubstitute target replacement domain)
        (naiveSubstitute target replacement codomain)
  | .bound index => if index = target then replacement else .bound index
  | .mu body => .mu (naiveSubstitute (target + 1) replacement body)

example :
    naiveSubstitute 0 (.bound 0) (.mu (.bound 1)) = .mu (.bound 0) := rfl

example :
    substitute 0 (.bound 0) (.mu (.bound 1)) = .mu (.bound 1) := rfl

inductive ChoiceStep : Bool → Bool → Prop where
  | finish : ChoiceStep true false
  | loop : ChoiceStep true true

theorem falseIsNormal : ¬∃ next, ChoiceStep false next := by
  rintro ⟨next, step⟩
  cases step

def infiniteLoop : Nat → Bool := fun _ => true

theorem infiniteLoopSteps : ∀ n, ChoiceStep (infiniteLoop n) (infiniteLoop (n + 1)) :=
  fun _ => .loop