fix(tg-0): Tangle.lean compiles cleanly + wire CI build oracle (#33)

hyperpolymath · claude · web-flow · commit 01c19a416bc0 · 2026-06-02T10:22:26.000+01:00
Closes #32 (TG-0). Problem ======= Empirical audit on 2026-06-01 found `proofs/Tangle.lean` had **121 errors** on every Lean 4 version v4.9 through v4.16. The 2026-03-30 commit titled *"feat: add Lean 4 formal proofs — progress, preservation, determinism"* with body *"Zero sorry. ... Covers knot-theoretic compose/tensor/close operations"* was committed without ever compiling. No CI ran Lean, so the broken claim went undetected for ~2 months. Fix === **62 inserts / 51 deletes**, zero `sorry` / `axiom` / `admit` / `Admitted`. All 4 headline theorems preserved in full: - `progress` — well-typed closed terms are values or can step - `preservation` — stepping preserves types - `determinism` — the step relation is deterministic - `type_safety` — progress + preservation corollary Auxiliary lemmas (`canonical_*`, `value_no_step`, `generatorWidth_*`) also preserved. What changed mechanically: 1. `foldl_max_init`: replaced terse one-liner with explicit `rw [ih (max a (g.idx+1)), ih (max 0 (g.idx+1))]` — the old `rw [ih, ih (max 0 _)]` left omega with an unresolved metavariable. 2. `foldl_shift_init`: replaced `split <;> omega` (couldn't close the if-then-else interaction) with `by_cases hrest : rest = []` plus targeted simp/omega per branch. 3. `cases ht with | tComposeWord ... =>` and siblings (tTensorWord, tEqWord, tEqNum, tEqStr, tAddNum, tCloseWord, tPipeline): dropped one underscore per pattern; modern Lean does not bind Γ as a separate name when it unifies to `[]`. 4. Progress sub-goals for `composeIdL`/`composeIdR`/`tensorIdL`/ `tensorIdR`: removed spurious explicit args; `Step` constructors have only implicit args. 5. `composeWords` arm of preservation: added `rw [← generatorWidth_append]` so the resulting type matches. 6. `tensorWords` arm of preservation: replaced broken split/rename_i with explicit `have hgoal` and targeted `rw`. 7. `congrArg (·.compose _) (ih h)` and siblings: replaced left-side dot-notation sections (which produced `?m = ?m` failures because `_` became a fresh per-side metavar) with `rw [ih h]`. Right-side forms (`Expr.compose _ ·`) still work unchanged. CI build oracle =============== - `proofs/lean-toolchain`: pins `leanprover/lean4:v4.14.0`. Verified 0 errors on v4.10–v4.16 inclusive. - `.github/workflows/lean-proofs.yml`: builds `proofs/Tangle.lean` on every PR / push to `main` that touches `proofs/**` or the workflow. Two gates: (a) `lean Tangle.lean` returns 0 errors; (b) no `sorry`/`axiom`/`admit`/`Admitted` outside comments. - Future drift fails CI rather than landing silently — same shape as the ephapax `coq-build.yml` rule [[feedback-proof-pr-build-oracle-is-only-truth]]. Truthful narrative update ========================= - `PROOF-NARRATIVE.md` §2: adds "Build oracle" sub-section recording the 121→0 trajectory; cross-documents echo-types audit as NOT-RELEVANT (per [[proofs-must-check-and-cross-doc-echo-types]]). - `ASSUMPTIONS.md` changelog: new 2026-06-01 row noting TG-0 closure and the CI gate. Unblocks ======== - TG-1 (let-binding extension, #26) — was blocked on a base file that did not compile. Now unblocked. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/.github/workflows/lean-proofs.yml b/.github/workflows/lean-proofs.yml
@@ -0,0 +1,84 @@
+# SPDX-License-Identifier: MPL-2.0
+# Owner: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Lean proof build oracle for proofs/Tangle.lean.
+#
+# Closes the TG-0 gap: prior to 2026-06-01, the Lean file claimed to prove
+# Progress / Preservation / Determinism / TypeSafety but had 121 errors on
+# every Lean 4 version 4.9-4.16, with no CI running it. This workflow makes
+# the build oracle the single source of truth — any future PR that breaks the
+# proofs fails CI rather than landing silently.
+#
+# Pinned via `proofs/lean-toolchain` to `leanprover/lean4:v4.14.0`. Verified
+# 0 errors on v4.10–v4.16 inclusive.
+
+name: Lean Proofs
+
+on:
+  pull_request:
+    paths:
+      - 'proofs/**'
+      - '.github/workflows/lean-proofs.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'proofs/**'
+      - '.github/workflows/lean-proofs.yml'
+  workflow_dispatch: {}
+
+permissions:
+  contents: read
+
+jobs:
+  build:
+    name: Build Lean proofs (oracle)
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v5
+        with:
+          persist-credentials: false
+
+      - name: Install elan
+        run: |
+          curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh \
+            | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      - name: Pin Lean toolchain from proofs/lean-toolchain
+        working-directory: proofs
+        run: |
+          test -f lean-toolchain || { echo "::error::proofs/lean-toolchain missing"; exit 1; }
+          echo "Using toolchain: $(cat lean-toolchain)"
+          lean --version
+
+      - name: Build Tangle.lean (oracle)
+        working-directory: proofs
+        run: |
+          set -euo pipefail
+          lean Tangle.lean 2>&1 | tee /tmp/lean-output.txt
+          errors=$(grep -c "error:" /tmp/lean-output.txt || true)
+          if [ "$errors" -ne 0 ]; then
+            echo "::error::Tangle.lean has $errors errors — see job output above."
+            exit 1
+          fi
+          echo "Tangle.lean: 0 errors. Build oracle GREEN."
+
+      - name: Assert no sorry / axiom / admit slippage
+        working-directory: proofs
+        run: |
+          set -euo pipefail
+          banned_count=0
+          for pat in '\bsorry\b' '\baxiom\b' '\badmit\b' '\bAdmitted\b'; do
+            matches=$(grep -nE "$pat" Tangle.lean | grep -vE "^\s*--|^\s*/--|/-" || true)
+            if [ -n "$matches" ]; then
+              echo "::error::Forbidden token matching '$pat' in Tangle.lean:"
+              echo "$matches"
+              banned_count=$((banned_count + 1))
+            fi
+          done
+          if [ "$banned_count" -ne 0 ]; then
+            exit 1
+          fi
+          echo "No sorry/axiom/admit/Admitted found outside comments."
diff --git a/ASSUMPTIONS.md b/ASSUMPTIONS.md
@@ -70,3 +70,4 @@ date and reason.
 |------|--------|-----|
 | 2026-06-01 | Initial registry, scoped to Tangle metatheory + implementation refinement obligations | Audit |
 | 2026-06-01 | A-TG-9.1 reformulated under TG-9 Option B — accept LSP-only categories instead of pretending refinement (full Option A queued at #28). See `compiler/tangle-lsp/docs/lsp-diagnostic-categories.md`. | TG-9 Option B PR |
+| 2026-06-01 | TG-0 closed: `proofs/Tangle.lean` previously had 121 errors on Lean 4.9–4.16 (commit 8ce7be7 was committed without ever compiling). Repaired: 62/51 diff, 0 errors on Lean 4.10–4.16. CI oracle at `.github/workflows/lean-proofs.yml` pinned to v4.14.0 via `proofs/lean-toolchain`. Sorry/axiom/admit slippage check added. Closes hyperpolymath/tangle#32. | TG-0 PR |
diff --git a/PROOF-NARRATIVE.md b/PROOF-NARRATIVE.md
@@ -52,7 +52,22 @@ delivered slice and the remaining gap explicit.
 ## 2. Proven now
 
 All 16 results live in [`proofs/Tangle.lean`](proofs/Tangle.lean)
-(Lean 4, ~560 LoC, no `sorry`, no `axiom`).
+(Lean 4, ~570 LoC, no `sorry`, no `axiom`).
+
+**Build oracle.** As of 2026-06-01 (PR closing TG-0, hyperpolymath/tangle#32),
+the file is verified at every push/PR by `.github/workflows/lean-proofs.yml`,
+pinned to `proofs/lean-toolchain = leanprover/lean4:v4.14.0`. Empirical
+result on the original 2026-03-30 commit: 121 errors on every Lean 4
+version 4.9–4.16 — the file had never compiled. The current commit
+returns **0 errors**, verified locally on v4.10/4.11/4.12/4.13/4.14/4.15/4.16,
+with CI gating both `lean Tangle.lean` and a `sorry`/`axiom`/`admit`
+slippage check. Future drift will fail CI rather than land silently.
+
+**Echo-types audit.** Per [[proofs-must-check-and-cross-doc-echo-types]]:
+echo-types is fibre-based loss-with-residue semantics — it has zero
+lambda-calculus / progress / preservation content. Verdict:
+**NOT-RELEVANT** for all four theorems below. Recorded once at
+`feedback_echo_types_audit_krl_tangle_quandledb_not_relevant.md`.
 
 ### Theorems (the main results)
 
diff --git a/proofs/Tangle.lean b/proofs/Tangle.lean
@@ -214,7 +214,10 @@ private theorem foldl_max_init (gs : List Generator) (a : Nat) :
     max a (gs.foldl (fun acc g => max acc (g.idx + 1)) 0) := by
   induction gs generalizing a with
   | nil => simp [List.foldl]
-  | cons g rest ih => simp only [List.foldl]; rw [ih, ih (max 0 _)]; omega
+  | cons g rest ih =>
+    simp only [List.foldl]
+    rw [ih (max a (g.idx + 1)), ih (max 0 (g.idx + 1))]
+    omega
 
 theorem generatorWidth_append (gs₁ gs₂ : List Generator) :
     generatorWidth (gs₁ ++ gs₂) = max (generatorWidth gs₁) (generatorWidth gs₂) := by
@@ -226,11 +229,14 @@ private theorem foldl_shift_init (gs : List Generator) (n a : Nat) :
     if gs = [] then a
     else max a (gs.foldl (fun acc g => max acc (g.idx + 1)) 0 + n) := by
   induction gs generalizing a with
-  | nil => simp [List.foldl, List.map]
+  | nil => simp
   | cons g rest ih =>
-    simp only [List.map, List.foldl, List.cons_ne_nil, ↓reduceIte]
-    rw [ih, foldl_max_init rest (max 0 _)]
-    split <;> omega
+    simp only [List.map, List.foldl, List.cons_ne_nil, if_false]
+    rw [ih]
+    rw [foldl_max_init rest (max 0 (g.idx + 1))]
+    by_cases hrest : rest = []
+    · subst hrest; simp [List.foldl]; omega
+    · simp [hrest]; omega
 
 theorem generatorWidth_shift (gs : List Generator) (n : Nat) :
     generatorWidth (shiftGenerators gs n) =
@@ -252,39 +258,39 @@ theorem progress : HasType [] e τ → IsValue e ∨ ∃ e', Step e e' := by
   | tBool => left; exact .boolLit _
   | tIdentity => left; exact .identity
   | tBraid => left; exact .braidLit _
-  | tComposeWord _ _ _ n m h₁ h₂ =>
+  | tComposeWord _ _ n m h₁ h₂ =>
     right
     rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩
     · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩
       · rcases canonical_word hv₁ h₁ with ⟨rfl, _⟩ | ⟨gs₁, rfl, _⟩ <;>
         rcases canonical_word hv₂ h₂ with ⟨rfl, _⟩ | ⟨gs₂, rfl, _⟩
         · exact ⟨_, .composeIdId⟩
-        · exact ⟨_, .composeIdL gs₂⟩
-        · exact ⟨_, .composeIdR gs₁⟩
+        · exact ⟨_, .composeIdL⟩
+        · exact ⟨_, .composeIdR⟩
         · exact ⟨_, .composeWords⟩
       · exact ⟨_, .composeRight hv₁ hs₂⟩
     · exact ⟨_, .composeLeft hs₁⟩
-  | tTensorWord _ _ _ n m h₁ h₂ =>
+  | tTensorWord _ _ n m h₁ h₂ =>
     right
     rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩
     · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩
       · rcases canonical_word hv₁ h₁ with ⟨rfl, _⟩ | ⟨gs₁, rfl, _⟩ <;>
         rcases canonical_word hv₂ h₂ with ⟨rfl, _⟩ | ⟨gs₂, rfl, _⟩
         · exact ⟨_, .tensorIdId⟩
-        · exact ⟨_, .tensorIdL gs₂⟩
-        · exact ⟨_, .tensorIdR gs₁⟩
+        · exact ⟨_, .tensorIdL⟩
+        · exact ⟨_, .tensorIdR⟩
         · exact ⟨_, .tensorWords⟩
       · exact ⟨_, .tensorRight hv₁ hs₂⟩
     · exact ⟨_, .tensorLeft hs₁⟩
-  | tPipeline _ _ _ _ _ => exact .inr ⟨_, .pipeline⟩
-  | tCloseWord _ _ n h =>
+  | tPipeline _ _ _ _ => exact .inr ⟨_, .pipeline⟩
+  | tCloseWord _ n h =>
     right
     rcases progress h with hv | ⟨e', hs⟩
     · rcases canonical_word hv h with ⟨rfl, _⟩ | ⟨gs, rfl, _⟩
       · exact ⟨_, .closeId⟩
       · exact ⟨_, .closeWord⟩
     · exact ⟨_, .closeStep hs⟩
-  | tAddNum _ _ _ h₁ h₂ =>
+  | tAddNum _ _ h₁ h₂ =>
     right
     rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩
     · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩
@@ -293,7 +299,7 @@ theorem progress : HasType [] e τ → IsValue e ∨ ∃ e', Step e e' := by
         exact ⟨_, .addNums⟩
       · exact ⟨_, .addRight hv₁ hs₂⟩
     · exact ⟨_, .addLeft hs₁⟩
-  | tEqWord _ _ _ n h₁ h₂ =>
+  | tEqWord _ _ n h₁ h₂ =>
     right
     rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩
     · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩
@@ -305,7 +311,7 @@ theorem progress : HasType [] e τ → IsValue e ∨ ∃ e', Step e e' := by
         · exact ⟨_, .eqBraids⟩
       · exact ⟨_, .eqRight hv₁ hs₂⟩
     · exact ⟨_, .eqLeft hs₁⟩
-  | tEqNum _ _ _ h₁ h₂ =>
+  | tEqNum _ _ h₁ h₂ =>
     right
     rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩
     · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩
@@ -314,7 +320,7 @@ theorem progress : HasType [] e τ → IsValue e ∨ ∃ e', Step e e' := by
         exact ⟨_, .eqNums⟩
       · exact ⟨_, .eqRight hv₁ hs₂⟩
     · exact ⟨_, .eqLeft hs₁⟩
-  | tEqStr _ _ _ h₁ h₂ =>
+  | tEqStr _ _ h₁ h₂ =>
     right
     rcases progress h₁ with hv₁ | ⟨e₁', hs₁⟩
     · rcases progress h₂ with hv₂ | ⟨e₂', hs₂⟩
@@ -334,61 +340,66 @@ theorem preservation : HasType [] e τ → Step e e' → HasType [] e' τ := by
   intro ht hs
   induction hs generalizing τ with
   | composeLeft hs ih =>
-    cases ht with | tComposeWord _ _ _ n m h₁ h₂ => exact .tComposeWord _ _ _ n m (ih h₁) h₂
+    cases ht with | tComposeWord _ _ n m h₁ h₂ => exact .tComposeWord _ _ _ n m (ih h₁) h₂
   | composeRight _ hs ih =>
-    cases ht with | tComposeWord _ _ _ n m h₁ h₂ => exact .tComposeWord _ _ _ n m h₁ (ih h₂)
+    cases ht with | tComposeWord _ _ n m h₁ h₂ => exact .tComposeWord _ _ _ n m h₁ (ih h₂)
   | composeWords =>
-    cases ht with | tComposeWord _ _ _ n m h₁ h₂ =>
-    cases h₁; cases h₂; exact .tBraid _ _
+    cases ht with | tComposeWord _ _ n m h₁ h₂ =>
+    cases h₁; cases h₂
+    rw [← generatorWidth_append]
+    exact .tBraid _ _
   | composeIdL =>
-    cases ht with | tComposeWord _ _ _ n m h₁ h₂ =>
+    cases ht with | tComposeWord _ _ n m h₁ h₂ =>
     cases h₁ with | tIdentity => simp at *; exact h₂
   | composeIdR =>
-    cases ht with | tComposeWord _ _ _ n m h₁ h₂ =>
+    cases ht with | tComposeWord _ _ n m h₁ h₂ =>
     cases h₂ with | tIdentity => simp at *; exact h₁
   | composeIdId =>
-    cases ht with | tComposeWord _ _ _ n m h₁ h₂ =>
+    cases ht with | tComposeWord _ _ n m h₁ h₂ =>
     cases h₁; cases h₂; exact .tIdentity _
   | tensorLeft hs ih =>
-    cases ht with | tTensorWord _ _ _ n m h₁ h₂ => exact .tTensorWord _ _ _ n m (ih h₁) h₂
+    cases ht with | tTensorWord _ _ n m h₁ h₂ => exact .tTensorWord _ _ _ n m (ih h₁) h₂
   | tensorRight _ hs ih =>
-    cases ht with | tTensorWord _ _ _ n m h₁ h₂ => exact .tTensorWord _ _ _ n m h₁ (ih h₂)
+    cases ht with | tTensorWord _ _ n m h₁ h₂ => exact .tTensorWord _ _ _ n m h₁ (ih h₂)
   | tensorWords =>
-    cases ht with | tTensorWord _ _ _ n m h₁ h₂ =>
+    cases ht with | tTensorWord _ _ n m h₁ h₂ =>
     cases h₁; cases h₂
-    simp [generatorWidth_append, generatorWidth_shift]
-    split
-    · rename_i hempty; subst hempty; simp [generatorWidth, List.foldl]; exact .tBraid _ _
-    · rename_i hne
-      have := HasType.tBraid ([] : Ctx) _
-      simp [generatorWidth_append, generatorWidth_shift, hne] at this ⊢
-      exact .tBraid _ _
+    rename_i gs₁ gs₂
+    have hgoal :
+        generatorWidth (gs₁ ++ shiftGenerators gs₂ (generatorWidth gs₁))
+          = generatorWidth gs₁ + generatorWidth gs₂ := by
+      rw [generatorWidth_append, generatorWidth_shift]
+      by_cases hempty : gs₂ = []
+      · subst hempty; simp [generatorWidth, List.foldl]
+      · simp [hempty]; omega
+    rw [← hgoal]
+    exact .tBraid _ _
   | tensorIdL =>
-    cases ht with | tTensorWord _ _ _ n m h₁ h₂ =>
+    cases ht with | tTensorWord _ _ n m h₁ h₂ =>
     cases h₁ with | tIdentity => simp at *; exact h₂
   | tensorIdR =>
-    cases ht with | tTensorWord _ _ _ n m h₁ h₂ =>
+    cases ht with | tTensorWord _ _ n m h₁ h₂ =>
     cases h₂ with | tIdentity => simp at *; exact h₁
   | tensorIdId =>
-    cases ht with | tTensorWord _ _ _ n m h₁ h₂ =>
+    cases ht with | tTensorWord _ _ n m h₁ h₂ =>
     cases h₁; cases h₂; exact .tIdentity _
-  | pipeline => cases ht with | tPipeline _ _ _ _ h => exact h
-  | closeStep hs ih => cases ht with | tCloseWord _ _ n h => exact .tCloseWord _ _ n (ih h)
+  | pipeline => cases ht with | tPipeline _ _ _ h => exact h
+  | closeStep hs ih => cases ht with | tCloseWord _ n h => exact .tCloseWord _ _ n (ih h)
   | closeWord => cases ht with | tCloseWord => exact .tIdentity _
   | closeId => cases ht with | tCloseWord => exact .tIdentity _
-  | addLeft hs ih => cases ht with | tAddNum _ _ _ h₁ h₂ => exact .tAddNum _ _ _ (ih h₁) h₂
-  | addRight _ hs ih => cases ht with | tAddNum _ _ _ h₁ h₂ => exact .tAddNum _ _ _ h₁ (ih h₂)
+  | addLeft hs ih => cases ht with | tAddNum _ _ h₁ h₂ => exact .tAddNum _ _ _ (ih h₁) h₂
+  | addRight _ hs ih => cases ht with | tAddNum _ _ h₁ h₂ => exact .tAddNum _ _ _ h₁ (ih h₂)
   | addNums => cases ht with | tAddNum => exact .tNum _ _
   | eqLeft hs ih =>
     cases ht with
-    | tEqWord _ _ _ n h₁ h₂ => exact .tEqWord _ _ _ n (ih h₁) h₂
-    | tEqNum _ _ _ h₁ h₂ => exact .tEqNum _ _ _ (ih h₁) h₂
-    | tEqStr _ _ _ h₁ h₂ => exact .tEqStr _ _ _ (ih h₁) h₂
+    | tEqWord _ _ n h₁ h₂ => exact .tEqWord _ _ _ n (ih h₁) h₂
+    | tEqNum _ _ h₁ h₂ => exact .tEqNum _ _ _ (ih h₁) h₂
+    | tEqStr _ _ h₁ h₂ => exact .tEqStr _ _ _ (ih h₁) h₂
   | eqRight _ hs ih =>
     cases ht with
-    | tEqWord _ _ _ n h₁ h₂ => exact .tEqWord _ _ _ n h₁ (ih h₂)
-    | tEqNum _ _ _ h₁ h₂ => exact .tEqNum _ _ _ h₁ (ih h₂)
-    | tEqStr _ _ _ h₁ h₂ => exact .tEqStr _ _ _ h₁ (ih h₂)
+    | tEqWord _ _ n h₁ h₂ => exact .tEqWord _ _ _ n h₁ (ih h₂)
+    | tEqNum _ _ h₁ h₂ => exact .tEqNum _ _ _ h₁ (ih h₂)
+    | tEqStr _ _ h₁ h₂ => exact .tEqStr _ _ _ h₁ (ih h₂)
   | eqNums => cases ht with
     | tEqNum => exact .tBool _ _
     | tEqWord _ _ _ _ h₁ => cases h₁
@@ -423,7 +434,7 @@ theorem determinism : Step e e₁ → Step e e₂ → e₁ = e₂ := by
   intro hs₁ hs₂
   induction hs₁ generalizing e₂ with
   | composeLeft hs ih => cases hs₂ with
-    | composeLeft h => exact congrArg (·.compose _) (ih h)
+    | composeLeft h => rw [ih h]
     | composeRight hv _ => exact absurd hs (value_no_step hv)
     | composeWords => exact absurd hs (value_no_step (.braidLit _))
     | composeIdL => exact absurd hs (value_no_step .identity)
@@ -453,7 +464,7 @@ theorem determinism : Step e e₁ → Step e e₂ → e₁ = e₂ := by
     | composeRight _ h => exact absurd h (value_no_step .identity)
     | composeIdId => rfl
   | tensorLeft hs ih => cases hs₂ with
-    | tensorLeft h => exact congrArg (·.tensor _) (ih h)
+    | tensorLeft h => rw [ih h]
     | tensorRight hv _ => exact absurd hs (value_no_step hv)
     | tensorWords => exact absurd hs (value_no_step (.braidLit _))
     | tensorIdL => exact absurd hs (value_no_step .identity)
@@ -494,7 +505,7 @@ theorem determinism : Step e e₁ → Step e e₂ → e₁ = e₂ := by
     | closeStep h => exact absurd h (value_no_step .identity)
     | closeId => rfl
   | addLeft hs ih => cases hs₂ with
-    | addLeft h => exact congrArg (·.add _) (ih h)
+    | addLeft h => rw [ih h]
     | addRight hv _ => exact absurd hs (value_no_step hv)
     | addNums => exact absurd hs (value_no_step (.num _))
   | addRight hv hs ih => cases hs₂ with
@@ -506,7 +517,7 @@ theorem determinism : Step e e₁ → Step e e₂ → e₁ = e₂ := by
     | addRight _ h => exact absurd h (value_no_step (.num _))
     | addNums => rfl
   | eqLeft hs ih => cases hs₂ with
-    | eqLeft h => exact congrArg (·.eq _) (ih h)
+    | eqLeft h => rw [ih h]
     | eqRight hv _ => exact absurd hs (value_no_step hv)
     | eqNums => exact absurd hs (value_no_step (.num _))
     | eqStrs => exact absurd hs (value_no_step (.str _))
diff --git a/proofs/lean-toolchain b/proofs/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.14.0
