1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115

-- Simply typed lambda calculus in Lean!

/-- We use Greek letters for variables with type `Typ` -/
inductive Typ
  /-- New named type -/
  | new (x : Nat)
  /-- Function type -/
  | fn (α β : Typ)
deriving BEq, ReflBEq, LawfulBEq

inductive Term
  /-- Variable -/
  | var (x : Nat)
  /-- Lambda with de Bruijin indices -/
  | lam (b : Term)
  /-- Function application -/
  | app (f a : Term) (α : Typ)

/-- The type checker! The variable names are chosen so that i.e. `a : Term` corresponds to `α : Typ`. -/
def check (env : List Typ) : Term → Typ → Bool
  | .var x, α =>
    if _ : x < env.length then env[x] == α else false
  | .lam b, .fn α β =>
    check (α :: env) b β
  | .app f a α, β =>
    check env f (.fn α β) && check env a α
  | _, _ =>
    false

/-- Increment free variables by `k` -/
def incr (k d : Nat) : Term → Term
  | .var x =>
    .var (if d ≤ x then x + k else x)
  | .lam b =>
    .lam (incr k (d + 1) b)
  | .app f a α =>
    .app (incr k d f) (incr k d a) α

/-- `incr` preserves type -/
theorem check_incr env' env'' (h : check (env' ++ env) t τ) (hk : env''.length = k)
    : check (env' ++ (env'' ++ env)) (incr k env'.length t) τ := by
  match t, τ with
  | .var x, α =>
    grind [check, incr]
  | .lam b, .fn α β =>
    simp [check] at h
    simpa [check, incr] using check_incr (α :: env') env'' h hk
  | .app f a α, β =>
    simp [check] at h
    simpa [check, incr] using ⟨check_incr env' env'' h.1 hk, check_incr env' env'' h.2 hk⟩

/-- `incr 0` does nothing -/
theorem incr_zero : incr 0 d s = s := by
  cases s <;> simp [incr]
  · exact incr_zero
  · exact ⟨incr_zero, incr_zero⟩

/-- Substitute `s` at index `n` in a term -/
def sub (n : Nat) (s : Term) : Term → Term
  | .var x =>
    if x == n then incr n 0 s else .var (if n < x then x - 1 else x)
  | .lam b =>
    .lam (sub (n + 1) s b)
  | .app f a α =>
    .app (sub n s f) (sub n s a) α

/-- `sub` preserves type -/
theorem check_sub env' (h : check (env' ++ σ :: env) t τ) (hs : check env s σ) (hs' : check (env' ++ env) (incr env'.length 0 s) σ)
    : check (env' ++ env) (sub env'.length s t) τ := by
  match t, τ with
  | .var x, α =>
    grind [check, sub]
  | .lam b, .fn α β =>
    simp [check] at h
    simpa [check, sub] using check_sub (α :: env') h hs (check_incr [] (α :: env') hs (by grind))
  | .app f a α, β =>
    simp [check] at h
    simpa [check, sub] using ⟨check_sub env' h.1 hs hs', check_sub env' h.2 hs hs'⟩

/-- Eval without worrying about types -/
partial def eval_untyped : Term → Term
  | .var x =>
    .var x
  | .lam b =>
    .lam (eval_untyped b)
  | .app f a α =>
    let a' := eval_untyped a
    match eval_untyped f with
    | .lam b => eval_untyped (sub 0 a' b)
    | x => .app x a' α

/--
Eval a well-typed expression

TODO: Prove this terminates, see https://cecchetti.sites.cs.wisc.edu/cs704/2025fa/notes/lec23-normalization.pdf
-/
def eval env t τ (h : check env t τ) : { t' // check env t' τ } :=
  match t, τ with
  | .var x, α =>
    ⟨.var x, h⟩
  | .lam b, .fn α β =>
    let ⟨b', hb⟩ := eval (α :: env) b β h
    ⟨.lam b', by grind [check]⟩
  | .app f a α, β =>
    let ⟨a', ha⟩ := eval env a α (by grind [check])
    let ⟨f', hf⟩ := eval env f (.fn α β) (by grind [check])
    match f' with
    | .lam b =>
      eval env (sub 0 a' b) β (by
        simp [check] at hf
        exact check_sub [] hf (by grind) (by grind [incr_zero]))
    | x =>
      ⟨.app x a' α, by simpa [check] using ⟨hf, ha⟩⟩
decreasing_by
  all_goals sorry