SkBlaz · SkBlaz · Jul 14, 2026 · Jul 14, 2026 · Jul 14, 2026
@@ -1,6 +1,7 @@
 import Py3plex.DSL.Syntax
 import Py3plex.DSL.Semantics
 import Py3plex.Optimizer.FilterFusion
+import Py3plex.Optimizer.ProjectIdentity
 
 /-!
 # Py3plex Lean Formal Library

@@ -11,6 +11,8 @@ semantics of a `Plan` — and proves basic sanity theorems about it.
 * `eval (scan rows)          = rows`
 * `eval emptyScan            = []`
 * `eval (filter p child)     = (eval child).filter p`
+* `eval (project f child)    = (eval child).map f`
+* `eval (limit n child)      = (eval child).take n`
 -/
 
 namespace Py3plex.DSL
@@ -24,6 +26,8 @@ def Plan.eval : Plan α → List α
   | .scan rows      => rows
   | .emptyScan      => []
   | .filter p child => child.eval.filter p
+  | .project f child => child.eval.map f
+  | .limit n child => child.eval.take n
 
 -- ---------------------------------------------------------------------------
 -- Equation lemmas (marked @[simp] for use in later proofs)
@@ -44,6 +48,16 @@ theorem Plan.eval_emptyScan :
 theorem Plan.eval_filter (p : α → Bool) (child : Plan α) :
     (Plan.filter p child).eval = child.eval.filter p := rfl
 
+/-- Evaluating a `project` maps each row in the child's result. -/
+@[simp]
+theorem Plan.eval_project (f : α → α) (child : Plan α) :
+    (Plan.project f child).eval = child.eval.map f := rfl
+
+/-- Evaluating a `limit` keeps the first `n` rows of the child's result. -/
+@[simp]
+theorem Plan.eval_limit (n : Nat) (child : Plan α) :
+    (Plan.limit n child).eval = child.eval.take n := rfl
+
 -- ---------------------------------------------------------------------------
 -- Basic sanity theorems
 -- ---------------------------------------------------------------------------
@@ -80,4 +94,9 @@ theorem Plan.filter_const_false (child : Plan α) :
 theorem Plan.filter_empty_scan (p : α → Bool) :
     (Plan.filter p (Plan.emptyScan : Plan α)).eval = [] := by simp
 
+/-- Projecting with the identity function is the identity plan. -/
+theorem Plan.project_id (child : Plan α) :
+    (Plan.project (fun x => x) child).eval = child.eval := by
+  simp
+
 end Py3plex.DSL
@@ -2,9 +2,9 @@
 # Py3plex.DSL.Syntax — Abstract Query Plan Type
 
 Defines the inductive type `Plan α`, a minimal abstract query plan
-parameterised over row type `α`.  The type is deliberately small: only a
-base-case scan, a distinguished empty scan, and a filter step are included.
-This is enough to state and machine-check optimizer equivalence theorems.
+parameterised over row type `α`.  The type is deliberately small but now covers
+the minimum additional operators needed for reachable TODO items:
+scan/emptyScan/filter plus project/limit.
 
 ## Relation to py3plex Python code
 
@@ -13,6 +13,8 @@ This is enough to state and machine-check optimizer equivalence theorems.
 | `Plan.scan`      | `LogicalScanNodes` / `LogicalScanEdges` in `py3plex/optimizer/plan_nodes.py` |
 | `Plan.emptyScan` | `LogicalEmptyScan` in the same file |
 | `Plan.filter`    | `LogicalFilter` in the same file |
+| `Plan.project`   | `LogicalProject` in the same file |
+| `Plan.limit`     | `LogicalLimit` in the same file |
 
 Phase 1 does **not** prove that the Python optimizer always emits exactly the
 transformations proved here; that correspondence belongs to a later phase.
@@ -22,15 +24,21 @@ namespace Py3plex.DSL
 
 /-- An abstract query plan, generic over row type `α`.
 
-    * `scan rows`       — base case: yield a fixed list of rows.
-    * `emptyScan`       — known-empty result, matching Python's
-                          `LogicalEmptyScan`.
-    * `filter p child`  — keep only rows from `child` that satisfy
-                          boolean predicate `p`.
+    * `scan rows`          — base case: yield a fixed list of rows.
+    * `emptyScan`          — known-empty result, matching Python's
+                             `LogicalEmptyScan`.
+    * `filter p child`     — keep only rows from `child` that satisfy
+                             boolean predicate `p`.
+    * `project f child`    — row-wise projection/map, abstract counterpart of
+                             `LogicalProject`.
+    * `limit n child`      — keep at most the first `n` rows, abstract
+                             counterpart of `LogicalLimit`.
 -/
 inductive Plan (α : Type) where
   | scan   : List α → Plan α
   | emptyScan : Plan α
   | filter : (α → Bool) → Plan α → Plan α
+  | project : (α → α) → Plan α → Plan α
+  | limit : Nat → Plan α → Plan α
 
 end Py3plex.DSL
@@ -0,0 +1,23 @@
+import Py3plex.DSL.Semantics
+
+/-!
+# Py3plex.Optimizer.ProjectIdentity — Redundant Project Elimination
+
+## What this file proves
+
+`Plan.project (fun x => x) child` is semantically equivalent to `child`.
+
+This is the abstract counterpart of the Python optimizer rule
+`RemoveRedundantProject` in `py3plex/optimizer/rules.py`.
+-/
+
+namespace Py3plex.Optimizer
+
+open Py3plex.DSL
+
+/-- Removing an identity project preserves semantics. -/
+theorem remove_redundant_project {α : Type} (child : Plan α) :
+    (Plan.project (fun x => x) child).eval = child.eval := by
+  simpa using Plan.project_id child
+
+end Py3plex.Optimizer
@@ -20,7 +20,8 @@ formal/
     │   ├── Syntax.lean         Abstract Plan type
     │   └── Semantics.lean      Plan.eval + basic correctness theorems
     └── Optimizer/
-        └── FilterFusion.lean   Filter-fusion equivalence theorem
+        ├── FilterFusion.lean     Filter-fusion equivalence theorem
+        └── ProjectIdentity.lean  Redundant-project equivalence theorem
 ```
 
 ---
@@ -43,12 +44,15 @@ mathematical proof.
 | `Plan.eval_scan` | `Py3plex/DSL/Semantics.lean` | Evaluating a scan returns the original rows |
 | `Plan.eval_emptyScan` | `Py3plex/DSL/Semantics.lean` | Evaluating `emptyScan` yields `[]` |
 | `Plan.eval_filter` | `Py3plex/DSL/Semantics.lean` | Evaluating a filter applies the predicate to the child's result |
+| `Plan.eval_project` | `Py3plex/DSL/Semantics.lean` | Evaluating a project maps each row of the child's result |
+| `Plan.eval_limit` | `Py3plex/DSL/Semantics.lean` | Evaluating a limit keeps the first `n` rows |
 | `Plan.filter_const_true` | `Py3plex/DSL/Semantics.lean` | Filtering with `fun _ => true` is the identity |
 | `Plan.filter_const_false` | `Py3plex/DSL/Semantics.lean` | Filtering with `fun _ => false` yields `[]` |
 | `Plan.filter_empty_scan` | `Py3plex/DSL/Semantics.lean` | Filtering *any* predicate over `emptyScan` yields `[]` (models `ShortCircuitEmptyLayer`) |
 | `Py3plex.Optimizer.filter_compose` | `Py3plex/Optimizer/FilterFusion.lean` | Two `List.filter` calls compose into one with a conjunctive predicate |
 | `Py3plex.Optimizer.filterFusion` | `Py3plex/Optimizer/FilterFusion.lean` | **Main theorem**: two adjacent `Plan.filter` nodes are semantically equal to a single filter with a conjunctive predicate |
 | `Py3plex.Optimizer.filterFusion_length` | `Py3plex/Optimizer/FilterFusion.lean` | Filter fusion preserves the result length |
+| `Py3plex.Optimizer.remove_redundant_project` | `Py3plex/Optimizer/ProjectIdentity.lean` | Identity project elimination preserves semantics |
 
 All proofs are fully machine-checked; none use `sorry`, `admit`, or unsafe
 axioms.
@@ -78,6 +82,8 @@ The Lean `Plan` type abstracts:
 | `Plan.scan` | `LogicalScanNodes` / `LogicalScanEdges` in `plan_nodes.py` |
 | `Plan.emptyScan` | `LogicalEmptyScan` in `plan_nodes.py` |
 | `Plan.filter` | `LogicalFilter` in `plan_nodes.py` |
+| `Plan.project` | `LogicalProject` in `plan_nodes.py` |
+| `Plan.limit` | `LogicalLimit` in `plan_nodes.py` |
 
 The `filterFusion` theorem models the `CombineAdjacentFilters` rule in
 `py3plex/optimizer/rules.py` (class `CombineAdjacentFilters`, method `apply`,
@@ -191,8 +197,8 @@ New constructors mirror every `LogicalOp` subclass in
 - [x] `Plan.scan` — models `LogicalScanNodes` / `LogicalScanEdges`
 - [x] `Plan.filter` — models `LogicalFilter`
 - [x] `Plan.emptyScan` — models `LogicalEmptyScan`
-- [ ] `Plan.project` — models `LogicalProject`
-- [ ] `Plan.limit` — models `LogicalLimit`
+- [x] `Plan.project` — models `LogicalProject`
+- [x] `Plan.limit` — models `LogicalLimit`
 - [ ] `Plan.topK` — models `LogicalTopK`
 - [ ] `Plan.orderBy` — models `LogicalOrderBy`
 - [ ] `Plan.compute` — models `LogicalCompute`
@@ -218,7 +224,7 @@ The two checked items are already proved; the rest are open.
       Statement: reordering independent filters preserves semantics
 - [ ] `orderby_limit_to_topk` ↔ `ConvertOrderByLimitToTopK`  
       Statement: `limit k (orderBy key plan)`.eval = `topK k key plan`.eval
-- [ ] `remove_redundant_project` ↔ `RemoveRedundantProject`  
+- [x] `remove_redundant_project` ↔ `RemoveRedundantProject`  
       Statement: `project id plan`.eval = `plan`.eval
 - [ ] `early_limit_pushdown` ↔ `EarlyLimitPushdown`  
       Statement: `limit k (compute f plan)`.eval = `compute f (limit k plan)`.eval  

@@ -17,6 +17,7 @@ def test_formal_readme_matches_phase1_tree_and_toolchain():
     assert "Syntax.lean" in readme
     assert "Semantics.lean" in readme
     assert "FilterFusion.lean" in readme
+    assert "ProjectIdentity.lean" in readme
     assert toolchain in readme
 
 
@@ -32,17 +33,21 @@ def test_formal_theorems_listed_in_readme_exist_in_lean_sources():
     readme = _read(FORMAL / "README.md")
     semantics = _read(FORMAL / "Py3plex/DSL/Semantics.lean")
     filter_fusion = _read(FORMAL / "Py3plex/Optimizer/FilterFusion.lean")
+    project_identity = _read(FORMAL / "Py3plex/Optimizer/ProjectIdentity.lean")
 
     theorem_names = [
         "Plan.eval_scan",
         "Plan.eval_emptyScan",
         "Plan.eval_filter",
+        "Plan.eval_project",
+        "Plan.eval_limit",
         "Plan.filter_const_true",
         "Plan.filter_const_false",
         "Plan.filter_empty_scan",
         "Py3plex.Optimizer.filter_compose",
         "Py3plex.Optimizer.filterFusion",
         "Py3plex.Optimizer.filterFusion_length",
+        "Py3plex.Optimizer.remove_redundant_project",
     ]
 
     for theorem_name in theorem_names:
@@ -51,12 +56,15 @@ def test_formal_theorems_listed_in_readme_exist_in_lean_sources():
     assert "theorem Plan.eval_scan" in semantics
     assert "theorem Plan.eval_emptyScan" in semantics
     assert "theorem Plan.eval_filter" in semantics
+    assert "theorem Plan.eval_project" in semantics
+    assert "theorem Plan.eval_limit" in semantics
     assert "theorem Plan.filter_const_true" in semantics
     assert "theorem Plan.filter_const_false" in semantics
     assert "theorem Plan.filter_empty_scan" in semantics
     assert "theorem filter_compose" in filter_fusion
     assert "theorem filterFusion" in filter_fusion
     assert "theorem filterFusion_length" in filter_fusion
+    assert "theorem remove_redundant_project" in project_identity
 
 
 def test_formal_build_entrypoints_stay_aligned():
@@ -108,3 +116,24 @@ def test_formal_empty_scan_is_marked_done_and_mapped_to_python_node():
     assert "| `Plan.emptyScan` | `LogicalEmptyScan` in the same file |" in syntax
     assert "| emptyScan : Plan α" in syntax
     assert "theorem Plan.eval_emptyScan" in semantics
+
+
+def test_formal_project_and_limit_are_marked_done_and_defined():
+    readme = _read(FORMAL / "README.md")
+    syntax = _read(FORMAL / "Py3plex/DSL/Syntax.lean")
+    semantics = _read(FORMAL / "Py3plex/DSL/Semantics.lean")
+    project_identity = _read(FORMAL / "Py3plex/Optimizer/ProjectIdentity.lean")
+
+    assert "- [x] `Plan.project` — models `LogicalProject`" in readme
+    assert "- [x] `Plan.limit` — models `LogicalLimit`" in readme
+    assert "- [x] `remove_redundant_project` ↔ `RemoveRedundantProject`" in readme
+    assert "| `Plan.project` | `LogicalProject` in `plan_nodes.py` |" in readme
+    assert "| `Plan.limit` | `LogicalLimit` in `plan_nodes.py` |" in readme
+    assert "| `Plan.project`   | `LogicalProject` in the same file |" in syntax
+    assert "| `Plan.limit`     | `LogicalLimit` in the same file |" in syntax
+    assert "| project : (α → α) → Plan α → Plan α" in syntax
+    assert "| limit : Nat → Plan α → Plan α" in syntax
+    assert "theorem Plan.eval_project" in semantics
+    assert "theorem Plan.eval_limit" in semantics
+    assert "theorem Plan.project_id" in semantics
+    assert "theorem remove_redundant_project" in project_identity