From 009228f287b7ab0266973d8743c4db07b55ed69c Mon Sep 17 00:00:00 2001
From: rami3l <rami3l@outlook.com>
Date: Thu, 27 Jul 2023 11:01:38 +0800
Subject: [PATCH] feat: (wip) impl `Adequacy`, pt. 5

---
 Plfl/Untyped/Denotational.lean          |  2 +-
 Plfl/Untyped/Denotational/Adequacy.lean | 62 ++++++++++++++++++++++---
 2 files changed, 57 insertions(+), 7 deletions(-)

diff --git a/Plfl/Untyped/Denotational.lean b/Plfl/Untyped/Denotational.lean
index b060a9a..5d7ca54 100644
--- a/Plfl/Untyped/Denotational.lean
+++ b/Plfl/Untyped/Denotational.lean
@@ -347,7 +347,7 @@ lemma fn_elem (i : v ⇾ w ⊆ u) : v ⇾ w ∈ u := i rfl
 
 -- https://plfa.github.io/Denotational/#function-values
 /-- `IsFn u` means that `u` is a function value. -/
-inductive IsFn (u : Value) : Prop | isFn (h : u = v ⇾ w)
+inductive IsFn (u : Value) : Prop where | isFn (h : u = v ⇾ w)
 
 /-- `AllFn v` means that all elements of `v` are function values. -/
 def AllFn (v : Value) : Prop := ∀ {u}, u ∈ v → IsFn u
diff --git a/Plfl/Untyped/Denotational/Adequacy.lean b/Plfl/Untyped/Denotational/Adequacy.lean
index 654ee2b..e465faf 100644
--- a/Plfl/Untyped/Denotational/Adequacy.lean
+++ b/Plfl/Untyped/Denotational/Adequacy.lean
@@ -10,6 +10,7 @@ open Untyped Untyped.Notation
 open Untyped.Subst
 open BigStep BigStep.Notation
 open Denotational Denotational.Notation
+open Soundness (soundness)
 
 -- https://plfa.github.io/Adequacy/#the-property-of-being-greater-or-equal-to-a-function
 /-- `GtFn u` means that it is "greater than" a certain function value. -/
@@ -57,29 +58,78 @@ theorem GtFn.dec (v : Value) : Decidable (GtFn v) := by induction v with
 
 -- https://plfa.github.io/Adequacy/#relating-values-to-closures
 mutual
+  /--
+  `𝕍 v c` will hold when:
+  - `c` is in WHNF (i.e. is a λ-abstraction);
+  - `v` is a function;
+  - `c`'s body evaluates according to `v`.
+  -/
   def 𝕍 : Value → Clos → Prop
   | _, .clos (` _) _ => ⊥
   | _, .clos (_ □ _) _ => ⊥
   | ⊥, .clos (ƛ _) _ => ⊤
   | v ⇾ w, .clos (ƛ n) γ =>
     have : sizeOf w < 1 + sizeOf v + sizeOf w := by simp_arith; apply Nat.zero_le
-    ∀ c, 𝔼 v c → GtFn w → ∃ c', (γ‚' c ⊢ n ⇓ c') ∧ 𝕍 w c'
+    ∀ {c}, 𝔼 v c → GtFn w → ∃ c', (γ‚' c ⊢ n ⇓ c') ∧ 𝕍 w c'
   | .conj u v, c@(.clos (ƛ _) _) =>
     have : sizeOf v < 1 + sizeOf u + sizeOf v := by simp_arith; apply Nat.zero_le
     𝕍 u c ∧ 𝕍 v c
 
+  /--
+  `𝔼 v c` will hold when:
+  - `v` is greater than a function value;
+  - `c` evaluates to a closure `c'` in WHNF;
+  - `𝕍 v c` holds.
+  -/
   def 𝔼 : Value → Clos → Prop
   | v, .clos m γ' => GtFn v → ∃ c, (γ' ⊢ m ⇓ c) ∧ 𝕍 v c
 end
--- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Termination.20of.20mutual.20recursive.20defs.20with.20a.20.22shorthand.22.3F/near/378733953
+-- https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20Termination.20of.20mutual.20recursive.20defs.20with.20a.20.22shorthand.22.3F/near/378733953
 termination_by
   𝕍 v c => (sizeOf v, 0)
   𝔼 v c => (sizeOf v, 1)
 
+/-- `𝔾` relates `γ` to `γ'` if the corresponding values and closures are related by `𝔼` -/
+def 𝔾 (γ : Env Γ) (γ' : ClosEnv Γ) : Prop := ∀ {x : Γ ∋ ✶}, 𝔼 (γ x) (γ' x)
 
--- namespace Notation
--- end Notation
+/-- The proof of a term being in Weak-Head Normal Form. -/
+def WHNF (t : Γ ⊢ a) : Prop := ∃ n : Γ‚ ✶ ⊢ ✶, t = (ƛ n)
 
--- open Notation
+/-- A closure in a 𝕍 relation must be in WHNF. -/
+lemma WHNF.of_𝕍 (vc : 𝕍 v (.clos m γ)) : WHNF m := by
+  cases m with (simp [𝕍] at vc; try contradiction) | lam n => exists n
 
--- open Soundness (soundness)
+lemma 𝕍.conj (uc : 𝕍 u c) (vc : 𝕍 v c) : 𝕍 (u ⊔ v) c := by
+  let .clos m γ := c; cases m with (simp [𝕍] at *; try contradiction)
+  | lam => unfold 𝕍; exact ⟨uc, vc⟩
+
+lemma 𝕍.of_not_gtFn (nf : ¬ GtFn v) : 𝕍 v (.clos (ƛ n) γ') := by induction v with unfold 𝕍
+| bot => triv
+| fn v w => exfalso; apply nf; exists v, w
+| conj _ _ ih ih' => exact not_gtFn_conj_inv nf |>.imp ih ih'
+
+mutual
+  lemma 𝕍.sub (vvc : 𝕍 v c) (lt : v' ⊑ v) : 𝕍 v' c := by
+    let .clos m γ := c; cases m with (simp [𝕍] at *; try contradiction) | lam m =>
+      rename_i Γ; induction lt generalizing Γ with
+      | bot => triv
+      | conjL lt lt' ih ih' => unfold 𝕍; exact ⟨ih _ _ _ vvc, ih' _ _ _ vvc⟩
+      | conjR₁ lt ih => apply ih; unfold 𝕍 at vvc; exact vvc.1
+      | conjR₂ lt ih => apply ih; unfold 𝕍 at vvc; exact vvc.2
+      | trans lt lt' ih ih' => apply_rules [ih, ih']
+      | fn lt lt' ih ih' =>
+        unfold 𝕍; intro c evc gtw; unfold 𝕍 at vvc; rename_i v₂ v₁ _ _
+        have : sizeOf v₁ + sizeOf v₂ < sizeOf v + sizeOf v' := sorry
+        have ⟨c', ec', h⟩ := vvc (evc.sub lt) (gtw.sub lt'); exists c', ec'
+        let .clos m γ := c'; have ⟨m', h'⟩ := WHNF.of_𝕍 h; subst h'; exact ih' _ _ _ h
+      | dist => sorry
+
+  lemma 𝔼.sub (evc : 𝔼 v c) (lt : v' ⊑ v) : 𝔼 v' c := by
+    let .clos m γ := c; simp only [𝔼] at *; intro gtv'
+    have ⟨c, ec, vvc⟩ := evc <| gtv'.sub lt; exists c, ec; exact vvc.sub lt
+end
+termination_by
+  𝕍.sub => (sizeOf v + sizeOf v', 0)
+  𝔼.sub => (sizeOf v + sizeOf v', 1)
+
+#print Value.fn.sizeOf_spec