From 93e9869435a2f484e8606fb94ea36eacb5dedf26 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 28 Jul 2026 16:28:22 +0100 Subject: [PATCH] proofs(lean4): land the green half of the eta extension (PARTIAL, ET-1..3 eta) Salvaged from a campaign whose four attempts all died on a spend limit before reporting. One attempt had written six modules; five build green and are landed here. The sixth (EtaExpand) is NOT included -- see below. Landed, axiom-audited [propext, Quot.sound]: EtaNormal eta-long normal forms NfE/SpE. The core design point: `ne` is restricted to `.star` (`ne : Var G k -> SpE G k .star -> NfE G .star`), so every arrow-kinded normal form is a `lam` -- the discipline the beta-only `Nf` deliberately lacks. Plus spEKindLe. EtaConversion DefEqE = all DefEq rules PLUS a genuine eta rule `DefEqE t (.lam (.app (wkTy .vz t) (.var .vz)))`, and defEq_to_defEqE : DefEq t u -> DefEqE t u (eta extends beta). EtaSubstLemmas 26 theorems: cast/exchange toolkit for NfE/SpE. EtaHsub hereditary substitution on eta-long forms. EtaDecEq DecidableEq instances for NfE and SpE. NOT landed, and why: EtaExpand.lean fails to compile because the agent stubbed two cases of `adjWkv` (a weakening-exchange lemma for adjacent variable pairs) with the identifier `sorryAx_placeholder`, which does not exist. That is an honest failure -- it cannot masquerade as proven -- but it means goal 2 (the eta-long normalizer nfE) is genuinely unproven, so the file is excluded rather than shipped unlisted (an unMANIFESTed proof file is one of the failure modes this repo's gate deliberately catches). Scope, stated so nothing drifts: this does NOT close the "ET-1..3 (eta)" OPEN row. Landed = goals 1, 3, and the DecidableEq half of 7. Still open = the normalizer, soundness, completeness, defEqE_iff_nfE, decDefEqE, and the anti-vacuity example. PROOF-STATUS records exactly that. Verified: cold rebuild green (21 jobs); check-proofs.sh and scan-dangerous.sh real exit 0; check-proof-status.sh real exit 0 after the gated 15->20 update. Co-Authored-By: Claude Opus 5 --- docs/status/PROOF-STATUS.adoc | 4 +- verification/proofs/lean4/MANIFEST | 5 + verification/proofs/lean4/Systemet.lean | 5 + verification/proofs/lean4/Systemet/Audit.lean | 4 + .../lean4/Systemet/L1/EtaConversion.lean | 46 +++ .../proofs/lean4/Systemet/L1/EtaDecEq.lean | 77 ++++ .../proofs/lean4/Systemet/L1/EtaHsub.lean | 104 +++++ .../proofs/lean4/Systemet/L1/EtaNormal.lean | 86 ++++ .../lean4/Systemet/L1/EtaSubstLemmas.lean | 368 ++++++++++++++++++ 9 files changed, 697 insertions(+), 2 deletions(-) create mode 100644 verification/proofs/lean4/Systemet/L1/EtaConversion.lean create mode 100644 verification/proofs/lean4/Systemet/L1/EtaDecEq.lean create mode 100644 verification/proofs/lean4/Systemet/L1/EtaHsub.lean create mode 100644 verification/proofs/lean4/Systemet/L1/EtaNormal.lean create mode 100644 verification/proofs/lean4/Systemet/L1/EtaSubstLemmas.lean diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index ea51414..1e42c46 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -12,7 +12,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees. // Machine-readable ground-truth markers — checked by scripts/check-proof-status.sh. // Do not edit by hand without changing the MANIFEST accordingly. -// gate:lean4 gated=15 quarantined=0 +// gate:lean4 gated=20 quarantined=0 == Summary @@ -99,7 +99,7 @@ every theorem depends on nothing outside Lean's three-axiom trusted base | ID | Target | ET-14 | *TEA erasure — the headline open problem. Never cite as proven.* -| ET-1..3 (η) | η-laws / η-long normal forms extension of MECH-1 +| ET-1..3 (η) | η-laws / η-long normal forms extension of MECH-1 — **PARTIAL**: η-long forms `NfE`/`SpE` (neutrals at `★` only), `DefEqE` (β+η) with `defEq_to_defEqE`, `DecidableEq` for `NfE`/`SpE`, and a cast/exchange toolkit are landed and axiom-clean. **Still open: the η-long normalizer `nfE` (blocked on an `adjWkv` weakening-exchange lemma), soundness, completeness, `defEqE_iff_nfE`, `decDefEqE`, and the anti-vacuity example.** See issue #32 | ET-1..3 (NAT) | type-level ℕ + recursor via NbE (stretch; research-adjacent) | ET-6, ET-7 | Structural Gate soundness + refusal characterization | ET-8, ET-9 | Polarity Gate blame accounting + no-laundering diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST index d2f2a9d..e655a0e 100644 --- a/verification/proofs/lean4/MANIFEST +++ b/verification/proofs/lean4/MANIFEST @@ -16,3 +16,8 @@ verification/proofs/lean4|Systemet/L1/SubstLemmas.lean|gated|MECH-1: ET-2 commut verification/proofs/lean4|Systemet/L1/Soundness.lean|gated|MECH-1: ET-2 soundness (DefEq t (embNf (nf t))) verification/proofs/lean4|Systemet/L1/Completeness.lean|gated|MECH-1: ET-2 completeness + defEq_iff_nf verification/proofs/lean4|Systemet/L1/Decidable.lean|gated|MECH-1: ET-2 decEqNf/decDefEq (decidability of conversion) +verification/proofs/lean4|Systemet/L1/EtaNormal.lean|gated|MECH-1 eta: eta-long normal forms NfE/SpE (neutrals only at star) +verification/proofs/lean4|Systemet/L1/EtaConversion.lean|gated|MECH-1 eta: DefEqE (beta+eta) + defEq_to_defEqE embedding +verification/proofs/lean4|Systemet/L1/EtaSubstLemmas.lean|gated|MECH-1 eta: cast/exchange toolkit for NfE/SpE +verification/proofs/lean4|Systemet/L1/EtaHsub.lean|gated|MECH-1 eta: hereditary substitution on eta-long forms +verification/proofs/lean4|Systemet/L1/EtaDecEq.lean|gated|MECH-1 eta: DecidableEq for NfE/SpE diff --git a/verification/proofs/lean4/Systemet.lean b/verification/proofs/lean4/Systemet.lean index b3bc33d..a20b75b 100644 --- a/verification/proofs/lean4/Systemet.lean +++ b/verification/proofs/lean4/Systemet.lean @@ -11,3 +11,8 @@ import Systemet.L1.SubstLemmas import Systemet.L1.Soundness import Systemet.L1.Completeness import Systemet.L1.Decidable +import Systemet.L1.EtaNormal +import Systemet.L1.EtaConversion +import Systemet.L1.EtaSubstLemmas +import Systemet.L1.EtaHsub +import Systemet.L1.EtaDecEq diff --git a/verification/proofs/lean4/Systemet/Audit.lean b/verification/proofs/lean4/Systemet/Audit.lean index 21830b7..fc917bd 100644 --- a/verification/proofs/lean4/Systemet/Audit.lean +++ b/verification/proofs/lean4/Systemet/Audit.lean @@ -36,3 +36,7 @@ not in a status document. Update the PROOF-STATUS ledger when adding lines. #print axioms Systemet.L1.defEq_iff_nf #print axioms Systemet.L1.decEqNf #print axioms Systemet.L1.decDefEq + +-- MECH-1 (L1) eta extension: PARTIAL (goals 1,3 and DecidableEq only) +#print axioms Systemet.L1.spEKindLe +#print axioms Systemet.L1.defEq_to_defEqE diff --git a/verification/proofs/lean4/Systemet/L1/EtaConversion.lean b/verification/proofs/lean4/Systemet/L1/EtaConversion.lean new file mode 100644 index 0000000..2c327dd --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/EtaConversion.lean @@ -0,0 +1,46 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.EtaHsub +import Systemet.L1.Conversion +/-! +# L1 βη-conversion (ET-η: the extended primitive relation) + +`DefEqE` is `DefEq` plus the η-rule: a term `t` at kind `k₁ ⇒ k₂` is +convertible with `λ. (↑t) a₀` — its η-expansion, where `↑` is weakening by +the fresh slot (`wkTy .vz`) and `a₀` is the fresh variable (`.var .vz`). +The rules are otherwise verbatim `DefEq`, so `DefEqE` is again the least +congruent equivalence containing β — now also containing η. + +`defEq_to_defEqE` embeds the β-theory: η strictly extends it. +-/ + +namespace Systemet.L1 + +/-- Declarative βη-conversion: the least congruent equivalence containing + β and η. -/ +inductive DefEqE : {Γ : Ctx} → {k : Kind} → Ty Γ k → Ty Γ k → Prop where + | refl : DefEqE t t + | symm : DefEqE t u → DefEqE u t + | trans : DefEqE t u → DefEqE u v → DefEqE t v + | beta : (b : Ty (k₁ :: Γ) k₂) → (u : Ty Γ k₁) → + DefEqE (.app (.lam b) u) (subst0 b u) + | eta : (t : Ty Γ (.arr k₁ k₂)) → + DefEqE t (.lam (.app (wkTy .vz t) (.var .vz))) + | arrowCong : DefEqE a a' → DefEqE b b' → DefEqE (.arrow a b) (.arrow a' b') + | lamCong : DefEqE b b' → DefEqE (.lam b) (.lam b') + | appCong : DefEqE f f' → DefEqE a a' → DefEqE (.app f a) (.app f' a') + +/-- β-conversion embeds into βη-conversion: η strictly extends β. -/ +theorem defEq_to_defEqE {Γ : Ctx} {k : Kind} {t u : Ty Γ k} : + DefEq t u → DefEqE t u := by + intro h + induction h with + | refl => exact .refl + | symm _ ih => exact ih.symm + | trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂ + | beta b u => exact .beta b u + | arrowCong _ _ ih₁ ih₂ => exact ih₁.arrowCong ih₂ + | lamCong _ ih => exact ih.lamCong + | appCong _ _ ih₁ ih₂ => exact ih₁.appCong ih₂ + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/EtaDecEq.lean b/verification/proofs/lean4/Systemet/L1/EtaDecEq.lean new file mode 100644 index 0000000..39fe89b --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/EtaDecEq.lean @@ -0,0 +1,77 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.EtaNormal +/-! +# L1 decidable equality of η-long normal forms + +Hand-rolled decidable equality for the mutual pair `NfE`/`SpE` — as with +`Nf`/`Sp`, `deriving DecidableEq` cannot handle the mutual inductives, and +`.ne`/`.cons` hide a head/argument kind that must be compared first (with +`Kind`'s decidable equality) before the pieces can be compared +componentwise. +-/ + +namespace Systemet.L1 + +mutual + /-- Decidable equality on η-long normal forms. -/ + def decEqNfE : {Γ : Ctx} → {k : Kind} → (m n : NfE Γ k) → Decidable (m = n) + | _, _, .lam b₁, .lam b₂ => + match decEqNfE b₁ b₂ with + | .isTrue h => .isTrue (by rw [h]) + | .isFalse h => .isFalse fun e => h (by injection e) + | _, _, .base n₁, .base n₂ => + match Nat.decEq n₁ n₂ with + | .isTrue h => .isTrue (by rw [h]) + | .isFalse h => .isFalse fun e => h (by injection e) + | _, _, .base _, .arrow _ _ => .isFalse fun e => by injection e + | _, _, .base _, .ne _ _ => .isFalse fun e => by injection e + | _, _, .arrow _ _, .base _ => .isFalse fun e => by injection e + | _, _, .arrow a₁ b₁, .arrow a₂ b₂ => + match decEqNfE a₁ a₂ with + | .isFalse h₁ => .isFalse fun e => h₁ (by injection e) + | .isTrue h₁ => + match decEqNfE b₁ b₂ with + | .isTrue h₂ => .isTrue (by rw [h₁, h₂]) + | .isFalse h₂ => .isFalse fun e => h₂ (by injection e) + | _, _, .arrow _ _, .ne _ _ => .isFalse fun e => by injection e + | _, _, .ne _ _, .base _ => .isFalse fun e => by injection e + | _, _, .ne _ _, .arrow _ _ => .isFalse fun e => by injection e + | _, _, .ne (k := c₁) y₁ sp₁, .ne (k := c₂) y₂ sp₂ => + if hc : c₁ = c₂ then by + subst hc + exact + if hy : y₁ = y₂ then + match decEqSpE sp₁ sp₂ with + | .isTrue hs => .isTrue (by rw [hy, hs]) + | .isFalse hs => .isFalse fun e => hs (by injection e) + else .isFalse fun e => hy (by injection e) + else .isFalse fun e => hc (by injection e) + termination_by _ _ m _ => nfESize m + decreasing_by all_goals (simp only [nfESize]; omega) + + /-- Decidable equality on spines of η-long forms. -/ + def decEqSpE : {Γ : Ctx} → {a j : Kind} → (s t : SpE Γ a j) → Decidable (s = t) + | _, _, _, .nil, .nil => .isTrue rfl + | _, _, _, .nil, .cons _ _ => .isFalse fun e => by injection e + | _, _, _, .cons _ _, .nil => .isFalse fun e => by injection e + | _, _, _, .cons (b := b₁) sp₁ v₁, .cons (b := b₂) sp₂ v₂ => + if hb : b₁ = b₂ then by + subst hb + exact + match decEqSpE sp₁ sp₂ with + | .isFalse h₁ => .isFalse fun e => h₁ (by injection e) + | .isTrue h₁ => + match decEqNfE v₁ v₂ with + | .isTrue h₂ => .isTrue (by rw [h₁, h₂]) + | .isFalse h₂ => .isFalse fun e => h₂ (by injection e) + else .isFalse fun e => hb (by injection e) + termination_by _ _ _ s _ => spESize s + decreasing_by all_goals (simp only [spESize]; omega) +end + +instance : DecidableEq (NfE Γ k) := decEqNfE + +instance : DecidableEq (SpE Γ a j) := decEqSpE + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/EtaHsub.lean b/verification/proofs/lean4/Systemet/L1/EtaHsub.lean new file mode 100644 index 0000000..87b95d9 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/EtaHsub.lean @@ -0,0 +1,104 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.EtaNormal +/-! +# L1 hereditary substitution on η-long forms and the η-long normalizer + +The Keller–Altenkirch hereditary substitution, verbatim in structure from +`Hsub.lean` but on η-long forms. Totality is by the same +`(kindSize, tag, size)` lexicographic measure. The η-restriction *shrinks* +the definition: a normal form at an arrow kind is always a `lam`, so +`nappE` and the `cons` case of `appSpE` have a single, exhaustive clause — +the neutral branch of β-application is impossible by typing. + +`nfE` normalizes every `Ty` in one structural pass; variables are +η-expanded on the way in (`etaVarE`), which is exactly what makes the +result η-long. The embeddings `embNfE`/`embSpE` read η-long forms back as +terms. +-/ + +namespace Systemet.L1 + +mutual + /-- Hereditary substitution on η-long normal forms. -/ + def substNfE : {Γ : Ctx} → {j : Kind} → NfE Γ j → (x : Var Γ k) → NfE (rem x) k → NfE (rem x) j + | _, _, .lam b, x, u => .lam (substNfE b (.vs x) (wkNfE .vz u)) + | _, _, .base n, _, _ => .base n + | _, _, .arrow a b, x, u => .arrow (substNfE a x u) (substNfE b x u) + | _, _, .ne y sp, x, u => + match eqv x y with + | .same => appSpE u (substSpE sp x u) + | .diff _ y' => .ne y' (substSpE sp x u) + termination_by _ _ t _ _ => (kindSize k, 1, nfESize t) + decreasing_by + all_goals simp only [nfESize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.right; apply Prod.Lex.left; omega) + | (apply Prod.Lex.left + have h := spEKindLe sp + simp only [kindSize] at h ⊢ + omega) + + /-- Hereditary substitution on spines of η-long forms. -/ + def substSpE : {Γ : Ctx} → {a j : Kind} → SpE Γ a j → (x : Var Γ k) → NfE (rem x) k → SpE (rem x) a j + | _, _, _, .nil, _, _ => .nil + | _, _, _, .cons sp v, x, u => .cons (substSpE sp x u) (substNfE v x u) + termination_by _ _ _ sp _ _ => (kindSize k, 1, spESize sp) + decreasing_by + all_goals simp only [spESize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.right; apply Prod.Lex.left; omega) + + /-- Fold an η-long form through a spine, β-reducing at each step. The + intermediate form is at an arrow kind, hence a `lam` — the single + clause is exhaustive. -/ + def appSpE : {Γ : Ctx} → {a j : Kind} → NfE Γ a → SpE Γ a j → NfE Γ j + | _, _, _, u, .nil => u + | _, _, _, u, .cons sp v => + match appSpE u sp with + | .lam t => substNfE t .vz v + termination_by _ a _ _ sp => (kindSize a, 0, spESize sp) + decreasing_by + all_goals simp only [spESize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.left + have h := spEKindLe sp + simp only [kindSize] at h ⊢ + omega) +end + +/-- Single β-application of η-long forms: the function is always a `lam`. -/ +def nappE : NfE Γ (.arr a b) → NfE Γ a → NfE Γ b + | .lam t, v => substNfE t .vz v + +/-- The η-long normalizer: one structural pass, η-expanding variables. -/ +def nfE : {Γ : Ctx} → {k : Kind} → Ty Γ k → NfE Γ k + | _, _, .var x => etaVarE x + | _, _, .base n => .base n + | _, _, .arrow a b => .arrow (nfE a) (nfE b) + | _, _, .lam b => .lam (nfE b) + | _, _, .app f a => nappE (nfE f) (nfE a) +termination_by structural _ _ t => t + +mutual + /-- Embed an η-long normal form back into raw terms. -/ + def embNfE : {Γ : Ctx} → {k : Kind} → NfE Γ k → Ty Γ k + | _, _, .lam b => .lam (embNfE b) + | _, _, .base n => .base n + | _, _, .arrow a b => .arrow (embNfE a) (embNfE b) + | _, _, .ne x sp => embSpE (.var x) sp + termination_by _ _ t => nfESize t + decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Embed a spine, folding applications around a head term. -/ + def embSpE : {Γ : Ctx} → {a j : Kind} → Ty Γ a → SpE Γ a j → Ty Γ j + | _, _, _, t, .nil => t + | _, _, _, t, .cons sp v => .app (embSpE t sp) (embNfE v) + termination_by _ _ _ _ sp => spESize sp + decreasing_by all_goals (simp only [spESize]; omega) +end + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/EtaNormal.lean b/verification/proofs/lean4/Systemet/L1/EtaNormal.lean new file mode 100644 index 0000000..9149ea1 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/EtaNormal.lean @@ -0,0 +1,86 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.Normal +/-! +# L1 η-long normal forms (ET-η, extending MECH-1) + +η-long normal forms `NfE` and neutral spines `SpE`, after Keller–Altenkirch +("Hereditary Substitutions for Simple Types", MSFP 2010), whose development +is natively η-long: a neutral `ne x sp` is a normal form **only at the base +kind `★`**, so every η-long form at kind `k₁ ⇒ k₂` is a `lam`. + +`etaNe` is η-expansion of a neutral (a head variable applied through a +spine) by *structural recursion on the result kind*: at `★` the neutral is +already normal; at `b ⇒ c` we go under a binder, weaken the spine, append +the η-expanded fresh variable, and recurse at `c` (the fresh variable is +itself expanded at the strictly smaller kind `b`). +-/ + +namespace Systemet.L1 + +mutual + /-- η-long β-normal forms: neutrals are admitted **only at `★`**. -/ + inductive NfE : Ctx → Kind → Type where + | lam : NfE (k₁ :: Γ) k₂ → NfE Γ (.arr k₁ k₂) + | base : Nat → NfE Γ .star + | arrow : NfE Γ .star → NfE Γ .star → NfE Γ .star + | ne : Var Γ k → SpE Γ k .star → NfE Γ .star + + /-- Spines of η-long forms, left-nested (`cons sp v` appends the *last* + argument), exactly as `Sp`. -/ + inductive SpE : Ctx → Kind → Kind → Type where + | nil : SpE Γ k k + | cons : SpE Γ a (.arr b c) → NfE Γ b → SpE Γ a c +end + +mutual + /-- Index-independent size of an η-long form (termination measure). -/ + def nfESize : {Γ : Ctx} → {k : Kind} → NfE Γ k → Nat + | _, _, .lam b => nfESize b + 1 + | _, _, .base _ => 1 + | _, _, .arrow a b => nfESize a + nfESize b + 1 + | _, _, .ne _ sp => spESize sp + 1 + + /-- Index-independent size of a spine (termination measure). -/ + def spESize : {Γ : Ctx} → {a j : Kind} → SpE Γ a j → Nat + | _, _, _, .nil => 0 + | _, _, _, .cons sp v => spESize sp + nfESize v + 1 +end + +/-- The end kind of a spine is no larger than its head kind. -/ +theorem spEKindLe : {Γ : Ctx} → {a j : Kind} → SpE Γ a j → kindSize j ≤ kindSize a + | _, _, _, .nil => Nat.le_refl _ + | _, _, _, .cons sp _ => + Nat.le_trans (by simp [kindSize]; omega) (spEKindLe sp) + +mutual + /-- Weakening of η-long forms along one skipped slot. -/ + def wkNfE : {Γ : Ctx} → (x : Var Γ k) → NfE (rem x) j → NfE Γ j + | _, x, .lam b => .lam (wkNfE (.vs x) b) + | _, _, .base n => .base n + | _, x, .arrow a b => .arrow (wkNfE x a) (wkNfE x b) + | _, x, .ne y sp => .ne (wkv x y) (wkSpE x sp) + termination_by _ _ t => nfESize t + decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Weakening of spines along one skipped slot. -/ + def wkSpE : {Γ : Ctx} → (x : Var Γ k) → SpE (rem x) a j → SpE Γ a j + | _, _, .nil => .nil + | _, x, .cons sp v => .cons (wkSpE x sp) (wkNfE x v) + termination_by _ _ sp => spESize sp + decreasing_by all_goals (simp only [spESize]; omega) +end + +/-- η-expansion of a neutral, by structural recursion on the result kind: + at `★` keep the neutral; at `b ⇒ c` bind a fresh variable of kind `b`, + weaken, append the η-expanded fresh variable, and recurse at `c`. -/ +def etaNe : (j : Kind) → {Γ : Ctx} → {a : Kind} → Var Γ a → SpE Γ a j → NfE Γ j + | .star, _, _, x, sp => .ne x sp + | .arr b c, _, _, x, sp => + .lam (etaNe c (.vs x) (.cons (wkSpE .vz sp) (etaNe b .vz .nil))) +termination_by structural j => j + +/-- η-expansion of a variable: the η-long normal form of `.var x`. -/ +abbrev etaVarE {Γ : Ctx} {a : Kind} (x : Var Γ a) : NfE Γ a := etaNe a x .nil + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/EtaSubstLemmas.lean b/verification/proofs/lean4/Systemet/L1/EtaSubstLemmas.lean new file mode 100644 index 0000000..d30c1b6 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/EtaSubstLemmas.lean @@ -0,0 +1,368 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.EtaHsub +import Systemet.L1.SubstLemmas +/-! +# L1 substitution-commutation toolkit for η-long forms + +The Keller–Altenkirch commutation-lemma base of `SubstLemmas.lean`, ported +to `NfE`/`SpE`. The variable-level laws (`eqv_refl`, `eqv_wkv`, `swp`, +`remSwap`, `wkv_wkv`, the `castV` kit and the lexicographic-descent +helpers) are *reused* from `SubstLemmas.lean` — they mention only `Var`. +What is ported here: the `castNfE`/`castSpE` transport kit, the spine +computation laws, commutation of the embeddings with weakening, the +cancellation law, the exchange of weakenings, and the +weakening/substitution exchange. The η-restriction only shrinks proofs: +`appSpE`'s intermediate forms at arrow kinds are always `lam`s, so every +neutral-function branch of the β-fold disappears. +-/ + +namespace Systemet.L1 + +/-! ## Spine application unrolling -/ + +/-- `appSpE` peels its last argument through `nappE`. -/ +theorem appSpE_cons (u : NfE Γ a) (sp : SpE Γ a (.arr b c)) (v : NfE Γ b) : + appSpE u (.cons sp v) = nappE (appSpE u sp) v := by + cases h : appSpE u sp with + | lam t => simp [appSpE, nappE, h] + +/-- `substNfE` at the substituted head: hand off to the spine fold. -/ +theorem substNfE_ne_self (x : Var Γ k) (sp : SpE Γ k .star) (u : NfE (rem x) k) : + substNfE (.ne x sp) x u = appSpE u (substSpE sp x u) := by + simp [substNfE, eqv_refl] + +/-- `substNfE` at a missed head: keep the neutral. -/ +theorem substNfE_ne_wkv (x : Var Γ k) (y : Var (rem x) c) (sp : SpE Γ c .star) + (u : NfE (rem x) k) : + substNfE (.ne (wkv x y) sp) x u = .ne y (substSpE sp x u) := by + simp [substNfE, eqv_wkv] + +/-! ## Embedding commutes with weakening -/ + +mutual + /-- Embedding a weakened η-long form is weakening the embedding. -/ + theorem embNfE_wkNfE : {Γ : Ctx} → {c j : Kind} → (x : Var Γ c) → (t : NfE (rem x) j) → + embNfE (wkNfE x t) = wkTy x (embNfE t) + | _, _, _, x, .lam (k₁ := k₁) b => by + simp only [wkNfE, embNfE, wkTy] + exact congrArg Ty.lam (embNfE_wkNfE (Var.vs (k' := k₁) x) b) + | _, _, _, _, .base n => by simp [wkNfE, embNfE, wkTy] + | _, _, _, x, .arrow a b => by + simp [wkNfE, embNfE, wkTy, embNfE_wkNfE x a, embNfE_wkNfE x b] + | _, _, _, x, .ne y sp => by + have h := embSpE_wkSpE x (.var y) sp + simp only [wkTy] at h + simp [wkNfE, embNfE, h] + termination_by _ _ _ _ t => nfESize t + decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Spine form of `embNfE_wkNfE`. -/ + theorem embSpE_wkSpE : {Γ : Ctx} → {c a j : Kind} → (x : Var Γ c) → (h : Ty (rem x) a) → + (sp : SpE (rem x) a j) → embSpE (wkTy x h) (wkSpE x sp) = wkTy x (embSpE h sp) + | _, _, _, _, _, _, .nil => by simp [wkSpE, embSpE] + | _, _, _, _, x, h, .cons sp v => by + simp [wkSpE, embSpE, wkTy, embSpE_wkSpE x h sp, embNfE_wkNfE x v] + termination_by _ _ _ _ _ _ sp => spESize sp + decreasing_by all_goals (simp only [spESize]; omega) +end + +/-! ## Cancellation: substituting a freshly weakened form -/ + +mutual + /-- Substituting at a slot the form was just weakened past is the identity. -/ + theorem substNfE_wkNfE_cancel : {Γ : Ctx} → {k j : Kind} → (x : Var Γ k) → + (t : NfE (rem x) j) → (u : NfE (rem x) k) → substNfE (wkNfE x t) x u = t + | _, _, _, x, .lam (k₁ := k₁) b, u => by + simp only [wkNfE, substNfE] + exact congrArg NfE.lam + (substNfE_wkNfE_cancel (Var.vs (k' := k₁) x) b (wkNfE .vz u)) + | _, _, _, _, .base n, _ => by simp [wkNfE, substNfE] + | _, _, _, x, .arrow a b, u => by + simp [wkNfE, substNfE, substNfE_wkNfE_cancel x a u, substNfE_wkNfE_cancel x b u] + | _, _, _, x, .ne y sp, u => by + simp [wkNfE, substNfE_ne_wkv, substSpE_wkSpE_cancel x sp u] + termination_by _ _ _ _ t _ => nfESize t + decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Spine form of `substNfE_wkNfE_cancel`. -/ + theorem substSpE_wkSpE_cancel : {Γ : Ctx} → {k a j : Kind} → (x : Var Γ k) → + (sp : SpE (rem x) a j) → (u : NfE (rem x) k) → substSpE (wkSpE x sp) x u = sp + | _, _, _, _, _, .nil, _ => by simp [wkSpE, substSpE] + | _, _, _, _, x, .cons sp v, u => by + simp [wkSpE, substSpE, substSpE_wkSpE_cancel x sp u, substNfE_wkNfE_cancel x v u] + termination_by _ _ _ _ _ sp _ => spESize sp + decreasing_by all_goals (simp only [spESize]; omega) +end + +/-! ## Context-cast toolkit for η-long forms -/ + +/-- Transport an η-long form along a context equality. -/ +def castNfE (h : Δ = Δ') (t : NfE Δ j) : NfE Δ' j := h ▸ t + +/-- Transport a spine along a context equality. -/ +def castSpE (h : Δ = Δ') (s : SpE Δ a j) : SpE Δ' a j := h ▸ s + +theorem castNfE_diag (e : Δ = Δ) (t : NfE Δ j) : castNfE e t = t := rfl + +theorem castSpE_diag (e : Δ = Δ) (s : SpE Δ a j) : castSpE e s = s := rfl + +theorem castNfE_lam (h : Δ = Δ') (b : NfE (k₁ :: Δ) k₂) : + castNfE h (.lam b) = .lam (castNfE (congrArg (k₁ :: ·) h) b) := by + subst h; rfl + +theorem castNfE_base (h : Δ = Δ') (n : Nat) : + castNfE h (.base n) = .base n := by + subst h; rfl + +theorem castNfE_arrow (h : Δ = Δ') (a b : NfE Δ .star) : + castNfE h (.arrow a b) = .arrow (castNfE h a) (castNfE h b) := by + subst h; rfl + +theorem castNfE_ne (h : Δ = Δ') (y : Var Δ c) (sp : SpE Δ c .star) : + castNfE h (.ne y sp) = .ne (castV h y) (castSpE h sp) := by + subst h; rfl + +theorem castSpE_nil (h : Δ = Δ') : + castSpE h (.nil (Γ := Δ) (k := a)) = .nil := by + subst h; rfl + +theorem castSpE_cons (h : Δ = Δ') (sp : SpE Δ a (.arr b c)) (v : NfE Δ b) : + castSpE h (.cons sp v) = .cons (castSpE h sp) (castNfE h v) := by + subst h; rfl + +theorem castNfE_appSpE (h : Δ = Δ') (F : NfE Δ a) (SP : SpE Δ a j) : + castNfE h (appSpE F SP) = appSpE (castNfE h F) (castSpE h SP) := by + subst h; rfl + +theorem castNfE_castNfE (e : Δ = Δ') (e' : Δ' = Δ'') (t : NfE Δ j) : + castNfE e' (castNfE e t) = castNfE (e.trans e') t := by + subst e; subst e'; rfl + +/-- Transporting past a fresh top slot commutes with weakening at `vz`. -/ +theorem castNfE_wkNfE_vz (h : Δ = Δ') (e : (c :: Δ : Ctx) = c :: Δ') (t : NfE Δ j) : + castNfE e (wkNfE (.vz (k := c) (Γ := Δ)) t) = wkNfE .vz (castNfE h t) := by + subst h; rfl + +/-- Spine form of `castNfE_wkNfE_vz`. -/ +theorem castSpE_wkSpE_vz (h : Δ = Δ') (e : (c :: Δ : Ctx) = c :: Δ') (sp : SpE Δ a j) : + castSpE e (wkSpE (.vz (k := c) (Γ := Δ)) sp) = wkSpE .vz (castSpE h sp) := by + subst h; rfl + +theorem castNfE_symm_cancel (e : Δ = Δ') (t : NfE Δ' j) : + castNfE e (castNfE e.symm t) = t := by + subst e; rfl + +theorem castSpE_symm_cancel (e : Δ = Δ') (sp : SpE Δ' a j) : + castSpE e (castSpE e.symm sp) = sp := by + subst e; rfl + +/-- η-expansion transports along a context equality. -/ +theorem castNfE_etaNe (h : Δ = Δ') (j : Kind) (x : Var Δ a) (sp : SpE Δ a j) : + castNfE h (etaNe j x sp) = etaNe j (castV h x) (castSpE h sp) := by + subst h; rfl + +/-! ## Exchange of weakenings -/ + +mutual + /-- Exchange of weakenings on η-long forms. -/ + theorem wkNfE_wkNfE : {Γ : Ctx} → {k c j : Kind} → (x : Var Γ k) → + (y : Var (rem x) c) → (t : NfE (rem y) j) → + wkNfE x (wkNfE y t) = + wkNfE (wkv x y) (wkNfE (swp x y) (castNfE (remSwap x y).symm t)) + | _, _, _, _, x, y, .lam (k₁ := k₁) b => by + rw [castNfE_lam] + simp only [wkNfE] + exact congrArg NfE.lam + (wkNfE_wkNfE (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y) b) + | _, _, _, _, x, y, .base n => by + rw [castNfE_base] + simp [wkNfE] + | _, _, _, _, x, y, .arrow a b => by + rw [castNfE_arrow] + simp only [wkNfE] + rw [wkNfE_wkNfE x y a, wkNfE_wkNfE x y b] + | _, _, _, _, x, y, .ne z sp => by + rw [castNfE_ne] + simp only [wkNfE] + rw [wkv_wkv x y z, wkSpE_wkSpE x y sp] + termination_by _ _ _ _ _ _ t => nfESize t + decreasing_by all_goals (simp only [nfESize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Exchange of weakenings on spines. -/ + theorem wkSpE_wkSpE : {Γ : Ctx} → {k c a j : Kind} → (x : Var Γ k) → + (y : Var (rem x) c) → (sp : SpE (rem y) a j) → + wkSpE x (wkSpE y sp) = + wkSpE (wkv x y) (wkSpE (swp x y) (castSpE (remSwap x y).symm sp)) + | _, _, _, _, _, x, y, .nil => by + rw [castSpE_nil] + simp [wkSpE] + | _, _, _, _, _, x, y, .cons sp v => by + rw [castSpE_cons] + simp only [wkSpE] + rw [wkSpE_wkSpE x y sp, wkNfE_wkNfE x y v] + termination_by _ _ _ _ _ _ _ sp => spESize sp + decreasing_by all_goals (simp only [spESize]; omega) +end + +/-- `substNfE` at the other slot of an exchange pair: the head misses, and + the surviving position is `swp x y`. -/ +theorem substNfE_ne_wkv' (x : Var Γ k) (y : Var (rem x) b) (sp : SpE Γ k .star) + (W : NfE (rem (wkv x y)) b) : + substNfE (.ne x sp) (wkv x y) W = .ne (swp x y) (substSpE sp (wkv x y) W) := by + rw [show (NfE.ne x sp : NfE Γ .star) = .ne (wkv (wkv x y) (swp x y)) sp from by + rw [wkv_swp]] + exact substNfE_ne_wkv (wkv x y) (swp x y) sp W + +/-! ## Weakening / substitution exchange -/ + +mutual + /-- Weakening exchanges with hereditary substitution: substituting the + other slot of an exchange pair into a weakened η-long form. -/ + theorem substNfE_wkNfE : {Γ : Ctx} → {k b j : Kind} → (x : Var Γ k) → + (y : Var (rem x) b) → (s : NfE (rem x) j) → (v : NfE (rem y) b) → + (W : NfE (rem (wkv x y)) b) → + W = wkNfE (swp x y) (castNfE (remSwap x y).symm v) → + substNfE (wkNfE x s) (wkv x y) W + = wkNfE (swp x y) (castNfE (remSwap x y).symm (substNfE s y v)) + | _, _, _, _, x, y, .lam (k₁ := k₁) s₀, v, W, hW => by + subst hW + have h1 := substNfE_wkNfE (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y) s₀ + (wkNfE (Var.vz (k := k₁) (Γ := rem y)) v) + (wkNfE (.vz (k := k₁) (Γ := rem (wkv x y))) + (wkNfE (swp x y) (castNfE (remSwap x y).symm v))) + ((wkNfE_wkNfE (Var.vz (k := k₁) (Γ := rem (wkv x y))) (swp x y) + (castNfE (remSwap x y).symm v)).trans + (congrArg (wkNfE (swp (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y))) + (castNfE_wkNfE_vz (remSwap x y).symm + (remSwap (Var.vs (k' := k₁) x) + (Var.vs (k' := k₁) y)).symm v)).symm) + simp only [wkNfE, substNfE] + rw [castNfE_lam] + simp only [wkNfE] + exact congrArg NfE.lam h1 + | _, _, _, _, x, y, .base n, v, W, hW => by + subst hW + simp only [wkNfE, substNfE] + rw [castNfE_base] + simp [wkNfE] + | _, _, _, _, x, y, .arrow a₀ b₀, v, W, hW => by + subst hW + simp only [wkNfE, substNfE] + rw [castNfE_arrow] + simp only [wkNfE] + rw [substNfE_wkNfE x y a₀ v _ rfl, substNfE_wkNfE x y b₀ v _ rfl] + | _, _, _, _, x, y, .ne (k := c) z sp, v, W, hW => + match c, z, sp, eqv y z with + | _, _, sp, .same => by + subst hW + simp only [wkNfE] + rw [substNfE_ne_self, substNfE_ne_self, + substSpE_wkSpE x y sp v _ rfl, + ← wkNfE_appSpE (swp x y) (castNfE (remSwap x y).symm v) + (castSpE (remSwap x y).symm (substSpE sp y v)), + ← castNfE_appSpE (remSwap x y).symm v (substSpE sp y v)] + | _, _, sp, .diff _ z' => by + subst hW + simp only [wkNfE] + rw [wkv_wkv x y z', substNfE_ne_wkv, substNfE_ne_wkv, + castNfE_ne (remSwap x y).symm z' (substSpE sp y v)] + simp only [wkNfE] + rw [substSpE_wkSpE x y sp v _ rfl] + termination_by _ _ b _ _ _ s _ _ _ => (kindSize b, 1, nfESize s) + decreasing_by + all_goals simp only [nfESize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; + first | omega | exact Nat.lt_succ_self _) + | (apply Prod.Lex.right; apply Prod.Lex.left; omega) + + /-- Spine form of `substNfE_wkNfE`. -/ + theorem substSpE_wkSpE : {Γ : Ctx} → {k b a j : Kind} → (x : Var Γ k) → + (y : Var (rem x) b) → (sp : SpE (rem x) a j) → (v : NfE (rem y) b) → + (W : NfE (rem (wkv x y)) b) → + W = wkNfE (swp x y) (castNfE (remSwap x y).symm v) → + substSpE (wkSpE x sp) (wkv x y) W + = wkSpE (swp x y) (castSpE (remSwap x y).symm (substSpE sp y v)) + | _, _, _, _, _, x, y, .nil, v, W, hW => by + subst hW + simp only [wkSpE, substSpE] + rw [castSpE_nil] + simp [wkSpE] + | _, _, _, _, _, x, y, .cons sp₀ v₀, v, W, hW => by + subst hW + simp only [wkSpE, substSpE] + rw [castSpE_cons] + simp only [wkSpE] + rw [substSpE_wkSpE x y sp₀ v _ rfl, substNfE_wkNfE x y v₀ v _ rfl] + termination_by _ _ b _ _ _ _ sp _ _ _ => (kindSize b, 1, spESize sp) + decreasing_by + all_goals simp only [spESize] + all_goals (apply Prod.Lex.right; apply Prod.Lex.right; omega) + + /-- Weakening distributes over the spine fold. -/ + theorem wkNfE_appSpE : {Γ : Ctx} → {cw aH j : Kind} → (w : Var Γ cw) → + (F : NfE (rem w) aH) → (SP : SpE (rem w) aH j) → + wkNfE w (appSpE F SP) = appSpE (wkNfE w F) (wkSpE w SP) + | _, _, _, _, w, F, .nil => by simp [wkSpE, appSpE] + | _, _, _, _, w, F, .cons (b := bT) SP v => by + rw [appSpE_cons] + simp only [wkSpE] + rw [appSpE_cons, ← wkNfE_appSpE w F SP] + cases appSpE F SP with + | lam T => + simp only [nappE, wkNfE] + exact (substNfE_wkNfE (Var.vs (k' := bT) w) .vz T v (wkNfE w v) rfl).symm + termination_by _ _ aH _ _ _ SP => (kindSize aH, 0, spESize SP) + decreasing_by + all_goals simp only [spESize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.left + have h := spEKindLe SP + simp only [kindSize] at h ⊢ + omega) +end + +/-- Weakening distributes over `nappE`. -/ +theorem wkNfE_nappE : {Γ : Ctx} → {cw a b : Kind} → (w : Var Γ cw) → + (F : NfE (rem w) (.arr a b)) → (A : NfE (rem w) a) → + wkNfE w (nappE F A) = nappE (wkNfE w F) (wkNfE w A) + | _, _, a, _, w, .lam T, A => by + simp only [nappE, wkNfE] + exact (substNfE_wkNfE (Var.vs (k' := a) w) .vz T A (wkNfE w A) rfl).symm + +/-- The `vz`-instance of the exchange: substituting past a fresh top slot. + Both casts are diagonal (`remSwap .vz y` relates `rem y` to itself), so + the statement is cast-free. -/ +theorem substNfE_wkNfE_vz {Γ : Ctx} {c k j : Kind} (X : Var Γ k) (s : NfE Γ j) + (u : NfE (rem X) k) : + substNfE (wkNfE (.vz (k := c) (Γ := Γ)) s) (.vs X) + (wkNfE (.vz (k := c) (Γ := rem X)) u) + = wkNfE (.vz (k := c) (Γ := rem X)) (substNfE s X u) := + substNfE_wkNfE (.vz (k := c) (Γ := Γ)) X s u + (wkNfE (.vz (k := c) (Γ := rem X)) u) rfl + +/-- Spine form of `substNfE_wkNfE_vz`. -/ +theorem substSpE_wkSpE_vz {Γ : Ctx} {c k a j : Kind} (X : Var Γ k) (sp : SpE Γ a j) + (u : NfE (rem X) k) : + substSpE (wkSpE (.vz (k := c) (Γ := Γ)) sp) (.vs X) + (wkNfE (.vz (k := c) (Γ := rem X)) u) + = wkSpE (.vz (k := c) (Γ := rem X)) (substSpE sp X u) := + substSpE_wkSpE (.vz (k := c) (Γ := Γ)) X sp u + (wkNfE (.vz (k := c) (Γ := rem X)) u) rfl + +/-- The `vz`-instance of the weakening exchange: pulling a fresh top slot + out past an arbitrary weakening. Both casts are diagonal. -/ +theorem wkNfE_wkNfE_vz {Γ : Ctx} {c k j : Kind} (w : Var Γ k) (t : NfE (rem w) j) : + wkNfE (.vs (k' := c) w) (wkNfE (.vz (k := c) (Γ := rem w)) t) + = wkNfE (.vz (k := c) (Γ := Γ)) (wkNfE w t) := + wkNfE_wkNfE (.vs (k' := c) w) .vz t + +/-- Spine form of `wkNfE_wkNfE_vz`. -/ +theorem wkSpE_wkSpE_vz {Γ : Ctx} {c k a j : Kind} (w : Var Γ k) (sp : SpE (rem w) a j) : + wkSpE (.vs (k' := c) w) (wkSpE (.vz (k := c) (Γ := rem w)) sp) + = wkSpE (.vz (k := c) (Γ := Γ)) (wkSpE w sp) := + wkSpE_wkSpE (.vs (k' := c) w) .vz sp + +end Systemet.L1