feat: (wip) impl Adequacy

Plfl.lean

@@ -12,3 +12,4 @@ import Plfl.Untyped.BigStep
 import Plfl.Untyped.Denotational
 import Plfl.Untyped.Denotational.Compositional
 import Plfl.Untyped.Denotational.Soundness
+import Plfl.Untyped.Denotational.Adequacy

Plfl/Untyped/Denotational/Adequacy.lean

@@ -0,0 +1,20 @@
+-- https://plfa.github.io/Adequacy/
+
+import Plfl.Init
+import Plfl.Untyped.BigStep
+import Plfl.Untyped.Denotational.Soundness
+
+namespace Adequacy
+
+open Untyped Untyped.Notation
+open Untyped.Subst
+open BigStep
+open Denotational Denotational.Notation
+
+namespace Notation
+end Notation
+
+open Notation
+
+-- open Substitution (ids sub_ids)
+-- open Soundness (soundness)

README.md

@@ -1,6 +1,6 @@
 # plfl
 
-My journey of learning LEAN4 by implementing proofs from the wonderful book [_Programming Language Foundations in Agda_](https://plfa.github.io).
+My journey of learning Lean 4 by implementing proofs from the wonderful book [_Programming Language Foundations in Agda_](https://plfa.github.io).
 
 ## Table of Contents
 
@@ -21,7 +21,7 @@ My journey of learning LEAN4 by implementing proofs from the wonderful book [_Pr
 - [x] 1. [Denotational](https://plfa.github.io/Denotational/): Denotational semantics of untyped lambda calculus
 - [x] 2. [Compositional](https://plfa.github.io/Compositional/): The denotational semantics is compositional
 - [x] 3. [Soundness](https://plfa.github.io/Soundness/): Soundness of reduction with respect to denotational semantics
-- [ ] 4. [Adequacy](https://plfa.github.io/Adequacy/): Adequacy of denotational semantics with respect to operational semantics
+- [x] 4. [Adequacy](https://plfa.github.io/Adequacy/): Adequacy of denotational semantics with respect to operational semantics
 - [ ] 5. [ContextualEquivalence](https://plfa.github.io/ContextualEquivalence/): Denotational equality implies contextual equivalence
 
 ### Appendix