feat: (wip) impl Adequacy, pt. 8

Plfl/Untyped/Denotational.lean

@@ -145,7 +145,7 @@ end Env.Sub
 inductive Eval : Env Γ → (Γ ⊢ ✶) → Value → Prop where
 | var : Eval γ (` i) (γ i)
 | ap : Eval γ l (v ⇾ w) → Eval γ m v → Eval γ (l □ m) w
-| fn : Eval (γ`‚ v) n w → Eval γ (ƛ n) (v ⇾ w)
+| fn {v w} : Eval (γ`‚ v) n w → Eval γ (ƛ n) (v ⇾ w)
 | bot : Eval γ m ⊥
 | conj : Eval γ m v → Eval γ m w → Eval γ m (v ⊔ w)
 | sub : Eval γ m v → w ⊑ v → Eval γ m w

Plfl/Untyped/Denotational/Adequacy.lean

@@ -91,6 +91,12 @@ termination_by
 /-- `𝔾` relates `γ` to `γ'` if the corresponding values and closures are related by `𝔼` -/
 def 𝔾 (γ : Env Γ) (γ' : ClosEnv Γ) : Prop := ∀ {i : Γ ∋ ✶}, 𝔼 (γ i) (γ' i)
 
+def 𝔾.empty : 𝔾 `∅ ∅ := by intro.
+
+def 𝔾.ext (g : 𝔾 γ γ') (e : 𝔼 v c) : 𝔾 (γ`‚ v) (γ'‚' c) := by unfold 𝔾; intro
+| .z => exact e
+| .s _ => exact g
+
 /-- The proof of a term being in Weak-Head Normal Form. -/
 def WHNF (t : Γ ⊢ a) : Prop := ∃ n : Γ‚ ✶ ⊢ ✶, t = (ƛ n)
 
@@ -141,13 +147,21 @@ lemma 𝔼.sub (evc : 𝔼 v c) (lt : v' ⊑ v) : 𝔼 v' c := by
   have ⟨c, ec, vvc⟩ := evc <| gtv'.sub lt; exists c, ec; exact vvc.sub lt
 
 -- https://plfa.github.io/Adequacy/#programs-with-function-denotation-terminate-via-call-by-name
-theorem 𝔼.of_eval (g : 𝔾 γ γ') (d : γ ⊢ m ￬ v) : 𝔼 v (.clos m γ') := by
-  induction d with (unfold 𝔾 at g; unfold 𝔼 at g ⊢)
+theorem 𝔼.of_eval {Γ} {γ : Env Γ} {γ' : ClosEnv Γ} {m : Γ ⊢ ✶} (g : 𝔾 γ γ') (d : γ ⊢ m ￬ v)
+: 𝔼 v (.clos m γ')
+:= by
+  generalize hx : v = x at *
+  induction d generalizing v with (unfold 𝔼; intro gt)
   | @var _ γ i =>
-    intro gt; have := @g i; split at this; rename_i Δ m' δ h
-    have ⟨c, e, v⟩ := this gt; refine ⟨c, ?_, v⟩; exact e.var h
-  | ap => sorry
-  | fn => sorry
-  | bot => sorry
+    unfold 𝔾 𝔼 at g; have := @g i; split at this
+    have ⟨c, em', vγi⟩ := this gt; refine ⟨c, ?_, vγi⟩; apply em'.var; trivial
+  | @ap _ _ _ _ _ m _ _ ih ih' =>
+    unfold 𝔼 at ih; have ⟨.clos l' δ, e_cl', v_cl'⟩ := ih g rfl ⟨_, _, .refl⟩
+    have ⟨m', h'⟩ := WHNF.of_𝕍 v_cl'; subst h'; unfold 𝕍 at v_cl'
+    have ⟨c', em'c', v_c'⟩ := @v_cl' (.clos m γ') (ih' g rfl) gt; exact ⟨c', e_cl'.ap em'c', v_c'⟩
+  | @fn _ _ n _ _ _ ih =>
+    unfold 𝔼 at ih; exists .clos (ƛ n) γ', .lam; unfold 𝕍; intro c ev₁c; exact ih (g.ext ev₁c) rfl
+  | bot => subst_vars; exfalso; exact not_gtFn_bot gt
+  | sub _ lt ih =>
+    unfold 𝔼 at ih; have ⟨c, e_c, v_c⟩ := ih g rfl <| gt.sub lt; exact ⟨c, e_c, v_c.sub lt⟩
   | conj => sorry
-  | sub => sorry