feat: (wip) impl Soundness, pt. 5

Plfl/Untyped/Denotational/Soundness.lean

@@ -107,6 +107,7 @@ section
 end
 
 -- https://plfa.github.io/Soundness/#simultaneous-substitution-reflects-denotations
+/-- Simultaneous substitution reflects denotations. -/
 theorem subst_reflect {σ : Subst Γ Δ} (d : δ ⊢ l ⇓ v) (h : ⟪σ⟫ m = l)
 : ∃ (γ : Env Γ), (δ `⊢ σ ⇓ γ) ∧ (γ ⊢ m ⇓ v)
 := by
@@ -134,3 +135,52 @@ theorem subst_reflect {σ : Subst Γ Δ} (d : δ ⊢ l ⇓ v) (h : ⟪σ⟫ m =
   | sub _ lt' ih => let ⟨γ, dγ, dm⟩ := ih h; exact ⟨γ, dγ, dm.sub lt'⟩
 
 -- https://plfa.github.io/Soundness/#single-substitution-reflects-denotations
+lemma subst₁σ_reflect {δ : Env Δ} {γ : Env (Δ‚ ✶)} (d : δ `⊢ subst₁σ m ⇓ γ)
+: ∃ w, (γ `⊑ δ`‚ w) ∧ (δ ⊢ m ⇓ w)
+:= by
+  exists γ.last; constructor
+  · intro
+    | .z => rfl
+    | .s i => apply var_inv (d i.s)
+  · exact d .z
+
+/-- Single substitution reflects denotations. -/
+theorem subst₁_reflect {δ : Env Δ} (d : δ ⊢ n ⇷ m ⇓ v) : ∃ w, (δ ⊢ m ⇓ w) ∧ (δ`‚ w ⊢ n ⇓ v)
+:= by
+  have ⟨γ, dγ, dn⟩ := subst_reflect d rfl; have ⟨w, ltw, dw⟩ := subst₁σ_reflect dγ
+  exists w, dw; exact sub_env dn ltw
+
+-- https://plfa.github.io/Soundness/#reduction-reflects-denotations-1
+theorem reflect {γ : Env Γ} {m n : Γ ⊢ a} (d : γ ⊢ n ⇓ v) (r : m —→ n) : γ ⊢ m ⇓ v := by
+  induction r generalizing v with
+  | lamβ =>
+    rename_i n u; generalize hx : n ⇷ u = x at *
+    induction d with
+    | var => apply beta; rw [hx]; exact .var
+    | ap d d' => apply beta; rw [hx]; exact d.ap d'
+    | fn d => apply beta; rw [hx]; exact d.fn
+    | bot => exact .bot
+    | conj _ _ ih ih' => exact (ih hx).conj (ih' hx)
+    | sub _ lt ih => exact (ih hx).sub lt
+  | lamζ r ihᵣ =>
+    rename_i _ n'; generalize hx : (ƛ n') = x at *
+    induction d with try contradiction
+    | fn d ih => sorry
+      -- refine .fn ?_; injection hx; subst_vars;
+      -- apply ih r ihᵣ rfl
+    | bot => exact .bot
+    | conj _ _ ih ih' => exact (ih r ihᵣ hx).conj (ih' r ihᵣ hx)
+    | sub _ lt ih => exact (ih r ihᵣ hx).sub lt
+  | apξ₁ r ihᵣ =>
+    sorry
+    -- rename_i l m; generalize hx : l □ m = x at *
+    -- induction d with try contradiction
+    -- | ap _ d' ih _ => exact (ih r ihᵣ hx).ap d'
+    -- | bot => exact .bot
+    -- | conj _ _ ih ih' => exact (ih r ihᵣ hx).conj (ih' r ihᵣ hx)
+    -- | sub _ lt ih => exact (ih r ihᵣ hx).sub lt
+  | apξ₂ =>
+    sorry
+  where
+    beta {Γ m n v} {γ : Env Γ} (d : γ ⊢ n ⇷ m ⇓ v) : γ ⊢ (ƛ n) □ m ⇓ v := by
+      let ⟨v, dm, dn⟩ := subst₁_reflect d; exact dn.fn.ap dm