From 7dc7cd72359a7792cd120e402362fb9076323521 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 22 Jul 2026 09:38:08 +0100 Subject: [PATCH] =?UTF-8?q?proofs(lean4):=20close=20ET-2=20=E2=80=94=20L1?= =?UTF-8?q?=20conversion=20is=20decidable?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Completes the MECH-1 milestone that Conversion.lean recorded as open. Purely additive: four new modules under Systemet/L1/, plus append-only entries in Systemet.lean, MANIFEST and Audit.lean. Syntax/Normal/Hsub/ Conversion.lean are untouched. Landed (all statements verbatim from the ET-2 ledger entry): SubstLemmas.lean substitution/weakening exchange family, incl. nf_substTy — normalization commutes with hereditary substitution (the beta case's whole content) Soundness.lean soundness : DefEq t (embNf (nf t)) Completeness.lean completeness : DefEq t u -> nf t = nf u defEq_iff_nf : DefEq t u <-> nf t = nf u Decidable.lean decEqNf / decEqSp (hand-rolled mutual DecidableEq -- `deriving` does not work across the Nf/Sp pair) decDefEq : (t u : Ty G k) -> Decidable (DefEq t u) Method: exchange coordinates (swp/remSwap) with an Eq.rec cast toolkit whose push lemmas are all `by subst h; rfl`, so definitional proof irrelevance makes diagonal casts vanish. The subst/subst exchange needs a SUM measure (kindSize k + kindSize b, tag, size) because the miss-then-hit case folds appSp at the second kind. Evidence (measured, not asserted): clean rebuild from scratch Build completed successfully (16 jobs) scripts/check-proofs.sh PASS, 20/20 headline items in trusted base scripts/scan-dangerous.sh PASS scripts/check-proof-status PASS after the doc update below #print axioms on soundness, completeness, defEq_iff_nf, decDefEq, decEqNf, decEqSp, nf_substTy -> [propext, Quot.sound] only; no sorryAx, no user axioms, no Classical.choice. Scope, stated honestly: DefEq here is beta + equivalence + congruence. eta is NOT included and remains an OPEN row, so ET-3 is unaffected -- its eta and model directions stay open. PROOF-STATUS.adoc moves ET-2 to proven *for the L1 core calculus* under the file's existing core-vs-full- theory caveat, and the now-satisfied "ET-2 (finish)" OPEN row is removed. Co-Authored-By: Claude Fable 5 --- docs/status/PROOF-STATUS.adoc | 31 +- verification/proofs/lean4/MANIFEST | 4 + verification/proofs/lean4/Systemet.lean | 4 + verification/proofs/lean4/Systemet/Audit.lean | 10 + .../lean4/Systemet/L1/Completeness.lean | 45 ++ .../proofs/lean4/Systemet/L1/Decidable.lean | 88 +++ .../proofs/lean4/Systemet/L1/Soundness.lean | 133 ++++ .../proofs/lean4/Systemet/L1/SubstLemmas.lean | 699 ++++++++++++++++++ 8 files changed, 1000 insertions(+), 14 deletions(-) create mode 100644 verification/proofs/lean4/Systemet/L1/Completeness.lean create mode 100644 verification/proofs/lean4/Systemet/L1/Decidable.lean create mode 100644 verification/proofs/lean4/Systemet/L1/Soundness.lean create mode 100644 verification/proofs/lean4/Systemet/L1/SubstLemmas.lean diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 9a80953..ea51414 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=11 quarantined=0 +// gate:lean4 gated=15 quarantined=0 == Summary @@ -20,7 +20,7 @@ summary from the per-prover MANIFESTs and fails if this file disagrees. |=== | Track | Total | Done | In progress | Open -| ET obligations (DOM — the theory itself) | 15 | 1 | 3 | 11 +| ET obligations (DOM — the theory itself) | 15 | 2 | 2 | 11 | MECH-1: L1 conversion, Lean4 (covers ET-1, ET-2, part of ET-3) | 1 | — | in progress | — | MECH-2: L2 grade algebras, Lean4 (covers ET-4, ET-5) | 1 | 1 | — | — |=== @@ -46,11 +46,15 @@ every theorem depends on nothing outside Lean's three-axiom trusted base normalizer, total by a `(kindSize, tag, size)` lexicographic measure | *Proven* (totality is by construction; the measure is the proof) -| ET-2 (equality is conversion) — partial -| `Systemet.L1.DefEq` (β + equivalence + congruence) stated; - `Systemet.L1.nf_emb : nf (embNf n) = n` — normal forms are fixed points - of the normalizer (stability) -| *Stability proven*; soundness/completeness OPEN (below) +| ET-2 (equality is conversion; decidability) +| `Systemet.L1.nf_emb` (stability), `nf_substTy` (normalization commutes + with substitution — the beta case), `soundness : DefEq t (embNf (nf t))`, + `completeness : DefEq t u → nf t = nf u`, + `defEq_iff_nf : DefEq t u ↔ nf t = nf u`, `decEqNf` / `decEqSp` + (hand-rolled mutual decidable equality on normal forms), and + `decDefEq : (t u : Ty Γ k) → Decidable (DefEq t u)` +| *Proven* for the L1 core calculus — `DefEq` here is β + equivalence + + congruence; η is **not** included (tracked as an OPEN row below) | ET-4 (grade algebras: the law set) | `Systemet.L2.GradeAlgebra` — ordered-semiring law set (16 laws) as a @@ -73,12 +77,12 @@ every theorem depends on nothing outside Lean's three-axiom trusted base | Slot | Headline artefact | Covers | File target | MECH-1 -| `defEq_iff_nf : DefEq t u ↔ nf t = nf u` + `decDefEq` (β-fragment). - Landed so far: totality core + stability. Remaining: soundness - (`DefEq t (embNf (nf t))`), completeness (`DefEq t u → nf t = nf u`), - decidable equality of `Nf` — all rest on the substitution-commutation - lemma; statements recorded in `Systemet/L1/Conversion.lean`. -| ET-1 ✓, ET-2 (partial), syntactic core of ET-3 +| `defEq_iff_nf : DefEq t u ↔ nf t = nf u` + `decDefEq` (β-fragment) — + *landed*. Totality core, stability, the substitution-commutation family + (`SubstLemmas.lean`), soundness, completeness, and decidable `Nf` + equality all compile and pass the axiom audit. Remaining for this slot: + the η extension and the model direction of ET-3. +| ET-1 ✓, ET-2 ✓ (β-fragment), syntactic core of ET-3 | `verification/proofs/lean4/Systemet/L1/` | MECH-2 @@ -95,7 +99,6 @@ 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-2 (finish) | soundness + completeness + `defEq_iff_nf` + `decDefEq` (MECH-1 milestone 2) | ET-1..3 (η) | η-laws / η-long normal forms extension of MECH-1 | ET-1..3 (NAT) | type-level ℕ + recursor via NbE (stretch; research-adjacent) | ET-6, ET-7 | Structural Gate soundness + refusal characterization diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST index b754b5e..d2f2a9d 100644 --- a/verification/proofs/lean4/MANIFEST +++ b/verification/proofs/lean4/MANIFEST @@ -12,3 +12,7 @@ verification/proofs/lean4|Systemet/L2/Instances/Tropical.lean|gated|MECH-2: Cost verification/proofs/lean4|Systemet/L2/Instances/Lattice.lean|gated|MECH-2: bounded distributive lattice => grade algebra; Level verification/proofs/lean4|Systemet/L2/Instances/Product.lean|gated|MECH-2: componentwise product algebra (ET-5) verification/proofs/lean4|Systemet/Audit.lean|gated|axiom audit (#print axioms per headline) +verification/proofs/lean4|Systemet/L1/SubstLemmas.lean|gated|MECH-1: ET-2 commutation toolkit (exchange laws, nf_substTy) +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) diff --git a/verification/proofs/lean4/Systemet.lean b/verification/proofs/lean4/Systemet.lean index ee0f2db..b3bc33d 100644 --- a/verification/proofs/lean4/Systemet.lean +++ b/verification/proofs/lean4/Systemet.lean @@ -7,3 +7,7 @@ import Systemet.L2.Instances.Affine import Systemet.L2.Instances.Tropical import Systemet.L2.Instances.Lattice import Systemet.L2.Instances.Product +import Systemet.L1.SubstLemmas +import Systemet.L1.Soundness +import Systemet.L1.Completeness +import Systemet.L1.Decidable diff --git a/verification/proofs/lean4/Systemet/Audit.lean b/verification/proofs/lean4/Systemet/Audit.lean index d902d30..93cab37 100644 --- a/verification/proofs/lean4/Systemet/Audit.lean +++ b/verification/proofs/lean4/Systemet/Audit.lean @@ -26,3 +26,13 @@ not in a status document. Update the PROOF-STATUS ledger when adding lines. #print axioms Systemet.L2.BoundedDistLattice.grade #print axioms Systemet.L2.Level.lattice #print axioms Systemet.L2.prodGrade + +-- MECH-1 (L1) milestone 2: ET-2 — conversion is decidable +#print axioms Systemet.L1.nf_substTy +#print axioms Systemet.L1.substNf_substNf +#print axioms Systemet.L1.defEq_substTy_embNf +#print axioms Systemet.L1.soundness +#print axioms Systemet.L1.completeness +#print axioms Systemet.L1.defEq_iff_nf +#print axioms Systemet.L1.decEqNf +#print axioms Systemet.L1.decDefEq diff --git a/verification/proofs/lean4/Systemet/L1/Completeness.lean b/verification/proofs/lean4/Systemet/L1/Completeness.lean new file mode 100644 index 0000000..4f99cdd --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/Completeness.lean @@ -0,0 +1,45 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.Soundness +/-! +# L1 completeness and `defEq_iff_nf` (ET-2) + +Completeness — convertible terms have equal normal forms — by induction on +the conversion derivation; the β-case is exactly the commutation equation +`nf_substTy`. Together with soundness this gives the ET-2 headline +`defEq_iff_nf : DefEq t u ↔ nf t = nf u`. +-/ + +namespace Systemet.L1 + +/-- **Completeness**: `nf` respects conversion. -/ +theorem completeness : {Γ : Ctx} → {k : Kind} → {t u : Ty Γ k} → + DefEq t u → nf t = nf u := by + intro Γ k t u h + induction h with + | refl => rfl + | symm _ ih => exact ih.symm + | trans _ _ ih₁ ih₂ => exact ih₁.trans ih₂ + | beta b u => + show nf (.app (.lam b) u) = nf (subst0 b u) + simp only [nf, napp] + exact (nf_substTy b .vz u).symm + | arrowCong _ _ ih₁ ih₂ => + simp only [nf] + rw [ih₁, ih₂] + | lamCong _ ih => + simp only [nf] + rw [ih] + | appCong _ _ ih₁ ih₂ => + simp only [nf] + rw [ih₁, ih₂] + +/-- **ET-2, headline**: conversion is normalize-then-compare. -/ +theorem defEq_iff_nf {Γ : Ctx} {k : Kind} {t u : Ty Γ k} : + DefEq t u ↔ nf t = nf u := + ⟨completeness, fun h => + (soundness t).trans (by + rw [congrArg embNf h] + exact (soundness u).symm)⟩ + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/Decidable.lean b/verification/proofs/lean4/Systemet/L1/Decidable.lean new file mode 100644 index 0000000..a8f1676 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/Decidable.lean @@ -0,0 +1,88 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.Completeness +/-! +# L1 decidability of conversion (ET-2) + +Hand-rolled decidable equality for the mutual pair `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. With +`defEq_iff_nf` this closes ET-2: `decDefEq` decides conversion by +normalize-then-compare. +-/ + +namespace Systemet.L1 + +mutual + /-- Decidable equality on normal forms. -/ + def decEqNf : {Γ : Ctx} → {k : Kind} → (m n : Nf Γ k) → Decidable (m = n) + | _, _, .lam b₁, .lam b₂ => + match decEqNf b₁ b₂ with + | .isTrue h => .isTrue (by rw [h]) + | .isFalse h => .isFalse fun e => h (by injection e) + | _, _, .lam _, .ne _ _ => .isFalse fun e => by injection e + | _, _, .ne _ _, .lam _ => .isFalse fun e => 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 decEqNf a₁ a₂ with + | .isFalse h₁ => .isFalse fun e => h₁ (by injection e) + | .isTrue h₁ => + match decEqNf 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 decEqSp 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 _ => nfSize m + decreasing_by all_goals (simp only [nfSize]; omega) + + /-- Decidable equality on spines. -/ + def decEqSp : {Γ : Ctx} → {a j : Kind} → (s t : Sp Γ 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 decEqSp sp₁ sp₂ with + | .isFalse h₁ => .isFalse fun e => h₁ (by injection e) + | .isTrue h₁ => + match decEqNf 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 _ => spSize s + decreasing_by all_goals (simp only [spSize]; omega) +end + +instance : DecidableEq (Nf Γ k) := decEqNf + +instance : DecidableEq (Sp Γ a j) := decEqSp + +/-- **ET-2, closure**: conversion is decidable — normalize and compare. -/ +def decDefEq (t u : Ty Γ k) : Decidable (DefEq t u) := + match decEqNf (nf t) (nf u) with + | .isTrue h => .isTrue (defEq_iff_nf.mpr h) + | .isFalse h => .isFalse fun d => h (defEq_iff_nf.mp d) + +instance : Decidable (DefEq t u) := decDefEq t u + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/Soundness.lean b/verification/proofs/lean4/Systemet/L1/Soundness.lean new file mode 100644 index 0000000..0304409 --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/Soundness.lean @@ -0,0 +1,133 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.SubstLemmas +/-! +# L1 soundness: `DefEq t (embNf (nf t))` (ET-2, milestone 2 of MECH-1) + +The substitution-commutation family at the `DefEq` level — the lemma named +in Conversion.lean's docstring, +`DefEq (substTy (embNf t) x (embNf u)) (embNf (substNf t x u))` — proved by +the same `(kindSize, tag, size)` lexicographic induction as `substNf` +itself. `DefEq`'s β-rule absorbs all the β-work `appSp` performs, so this +direction needs no equational commutation of substitutions. Soundness of +the normalizer follows by structural induction. +-/ + +namespace Systemet.L1 + +mutual + /-- Substitution commutes with embedding, up to conversion: the + Keller–Altenkirch commutation lemma at the `DefEq` level. -/ + theorem defEq_substTy_embNf : {Γ : Ctx} → {j k : Kind} → (t : Nf Γ j) → + (x : Var Γ k) → (u : Nf (rem x) k) → + DefEq (substTy (embNf t) x (embNf u)) (embNf (substNf t x u)) + | _, _, _, .lam (k₁ := k₁) b, x, u => by + have ih := defEq_substTy_embNf b (Var.vs (k' := k₁) x) (wkNf .vz u) + rw [embNf_wkNf] at ih + simp only [embNf, substNf, substTy] + exact ih.lamCong + | _, _, _, .base n, _, _ => by + simp only [embNf, substNf, substTy] + exact .refl + | _, _, _, .arrow a b, x, u => by + simp only [embNf, substNf, substTy] + exact (defEq_substTy_embNf a x u).arrowCong (defEq_substTy_embNf b x u) + | _, _, _, .ne (k := c) z sp, x, u => + match c, z, sp, eqv x z with + | _, _, sp, .same => by + simp only [embNf, substNf_ne_self] + exact (defEq_substTy_embSp sp x u (.var x) (embNf u) + (by simp only [substTy, eqv_refl]; exact .refl)).trans + (defEq_embSp_appSp u (substSp sp x u)) + | _, _, sp, .diff _ z' => by + simp only [embNf, substNf_ne_wkv] + exact defEq_substTy_embSp sp x u (.var (wkv x z')) (.var z') + (by simp only [substTy, eqv_wkv]; exact .refl) + termination_by _ _ k t _ _ => (kindSize k, 1, nfSize t) + decreasing_by + all_goals simp only [nfSize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.right; apply Prod.Lex.left; omega) + + /-- Spine form of `defEq_substTy_embNf`, threading a converted head. -/ + theorem defEq_substTy_embSp : {Γ : Ctx} → {a j k : Kind} → (sp : Sp Γ a j) → + (x : Var Γ k) → (u : Nf (rem x) k) → (h : Ty Γ a) → (h' : Ty (rem x) a) → + DefEq (substTy h x (embNf u)) h' → + DefEq (substTy (embSp h sp) x (embNf u)) (embSp h' (substSp sp x u)) + | _, _, _, _, .nil, _, _, _, _, hh => by + simp only [embSp, substSp] + exact hh + | _, _, _, _, .cons sp v, x, u, h, h', hh => by + simp only [embSp, substSp, substTy] + exact (defEq_substTy_embSp sp x u h h' hh).appCong + (defEq_substTy_embNf v x u) + termination_by _ _ _ k sp _ _ _ _ _ => (kindSize k, 1, spSize sp) + decreasing_by + all_goals simp only [spSize] + all_goals (apply Prod.Lex.right; apply Prod.Lex.right; omega) + + /-- Folding a normal form through a spine, embedded: `appSp` is + conversion-compatible. -/ + theorem defEq_embSp_appSp : {Γ : Ctx} → {a j : Kind} → (F : Nf Γ a) → + (SP : Sp Γ a j) → DefEq (embSp (embNf F) SP) (embNf (appSp F SP)) + | _, _, _, F, .nil => by + simp only [embSp, appSp] + exact .refl + | _, _, _, F, .cons SP v => by + rw [appSp_cons] + have s1 := (defEq_embSp_appSp F SP).appCong (DefEq.refl (t := embNf v)) + cases hG : appSp F SP with + | lam T => + rw [hG] at s1 + simp only [embSp, embNf, napp] at s1 ⊢ + exact s1.trans ((DefEq.beta (embNf T) (embNf v)).trans + (defEq_substTy_embNf T .vz v)) + | ne y sp' => + rw [hG] at s1 + simp only [embSp, embNf, napp] at s1 ⊢ + exact s1 + termination_by _ a _ _ SP => (kindSize a, 0, spSize SP) + decreasing_by + all_goals simp only [spSize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.left + have h := spKindLe SP + simp only [kindSize] at h ⊢ + omega) +end + +/-- One-step β-application, embedded: `napp` is conversion-compatible. -/ +theorem defEq_embNf_napp : {Γ : Ctx} → {a b : Kind} → (F : Nf Γ (.arr a b)) → + (A : Nf Γ a) → DefEq (.app (embNf F) (embNf A)) (embNf (napp F A)) + | _, _, _, .lam T, A => by + simp only [embNf, napp] + exact (DefEq.beta (embNf T) (embNf A)).trans (defEq_substTy_embNf T .vz A) + | _, _, _, .ne y sp, A => by + simp only [embNf, napp, embSp] + exact .refl + +/-- **Soundness**: every type-level term converts to its normal form. + With stability (`nf_emb`) this makes `nf` a normalizer for `DefEq`. -/ +theorem soundness : {Γ : Ctx} → {k : Kind} → (t : Ty Γ k) → DefEq t (embNf (nf t)) + | _, _, .var x => by + simp only [nf, embNf, embSp] + exact .refl + | _, _, .base n => by + simp only [nf, embNf] + exact .refl + | _, _, .arrow a b => by + simp only [nf, embNf] + exact (soundness a).arrowCong (soundness b) + | _, _, .lam b => by + simp only [nf, embNf] + exact (soundness b).lamCong + | _, _, .app f a => by + simp only [nf] + exact ((soundness f).appCong (soundness a)).trans + (defEq_embNf_napp (nf f) (nf a)) +termination_by _ _ t => tySize t +decreasing_by all_goals (simp only [tySize]; first | exact Nat.lt_succ_self _ | omega) + +end Systemet.L1 diff --git a/verification/proofs/lean4/Systemet/L1/SubstLemmas.lean b/verification/proofs/lean4/Systemet/L1/SubstLemmas.lean new file mode 100644 index 0000000..44bb59d --- /dev/null +++ b/verification/proofs/lean4/Systemet/L1/SubstLemmas.lean @@ -0,0 +1,699 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +import Systemet.L1.Conversion +/-! +# L1 substitution-commutation toolkit (ET-2, milestone 2 of MECH-1) + +Keller–Altenkirch's commutation-lemma base, ported. Variable-level +computation laws for `eqv`/`wkv`, the exchange coordinates `swp`/`remSwap`, +the spine-application unrolling `appSp_cons`, commutation of the embeddings +with weakening, and the cancellation law `substNf (wkNf x t) x u = t`. +These feed both directions of `defEq_iff_nf`: soundness +(`Systemet.L1.Soundness`) and completeness (`Systemet.L1.Completeness`). + +Matches on arguments whose type mentions `rem x` are pushed into term-level +`match`es after `x`'s constructor is known (the Syntax.lean idiom). Where a +`.vs`/`.vz` is written in a term whose `rem` index must reduce during +elaboration, the slot kind and context are pinned explicitly +(`Var.vs (k' := c) x`) — matcher reduction is blocked by metavariables. -/ + +namespace Systemet.L1 + +/-! ## Variable-level computation laws -/ + +/-- `eqv` at the diagonal computes to `same`. -/ +theorem eqv_refl : {Γ : Ctx} → {k : Kind} → (x : Var Γ k) → eqv x x = .same + | _ :: _, _, .vz => rfl + | _ :: _, _, .vs x => by simp [eqv, eqv_refl x] + +/-- `eqv` against a variable weakened past the slot computes to `diff`: + substitution misses a variable that avoids the substituted slot. -/ +theorem eqv_wkv : {Γ : Ctx} → {k j : Kind} → (x : Var Γ k) → (y : Var (rem x) j) → + eqv x (wkv x y) = .diff x y + | _ :: _, _, _, .vz => fun _ => rfl + | c :: _, _, _, .vs x => fun y => + match y with + | .vz => rfl + | .vs y => by + show eqv (Var.vs (k' := c) x) (Var.vs (wkv x y)) = _ + simp [eqv, eqv_wkv x y] + +/-- `wkv x` skips `x`'s slot, so it never produces `x` itself. -/ +theorem wkv_ne : {Γ : Ctx} → {k : Kind} → (x : Var Γ k) → (y : Var (rem x) k) → + wkv x y ≠ x + | _ :: _, _, .vz => fun _ h => by injection h + | _ :: _, _, .vs x => fun y h => by + cases y with + | vz => injection h + | vs y => exact wkv_ne x y (by injection h) + +/-- `wkv x` is injective. -/ +theorem wkv_inj : {Γ : Ctx} → {k j : Kind} → (x : Var Γ k) → + (y z : Var (rem x) j) → wkv x y = wkv x z → y = z + | _ :: _, _, _, .vz => fun _ _ h => by injection h + | _ :: _, _, _, .vs x => fun y z => + match y, z with + | .vz, .vz => fun _ => rfl + | .vz, .vs _ => fun h => by injection h + | .vs _, .vz => fun h => by injection h + | .vs y, .vs z => fun h => by + have h' : wkv x y = wkv x z := by injection h + rw [wkv_inj x y z h'] + +/-! ## The exchange coordinates: `swp` and `remSwap` + +Two distinct slots of `Γ` are canonically presented as a pair +`x : Var Γ k`, `y : Var (rem x) j`. Deleting them in the other order goes +through `wkv x y : Var Γ j`; `swp x y` is `x`'s position after that +deletion, and `remSwap` says both orders delete to the same context. -/ + +/-- `x`'s slot, as a position of `rem (wkv x y)`. -/ +def swp : {Γ : Ctx} → {k j : Kind} → (x : Var Γ k) → (y : Var (rem x) j) → + Var (rem (wkv x y)) k + | _ :: _, _, _, .vz => fun _ => .vz + | _ :: _, _, _, .vs x => fun y => + match y with + | .vz => x + | .vs y => .vs (swp x y) + +/-- Both deletion orders reach the same context. -/ +theorem remSwap : {Γ : Ctx} → {k j : Kind} → (x : Var Γ k) → (y : Var (rem x) j) → + rem (swp x y) = rem y + | _ :: _, _, _, .vz => fun _ => rfl + | c :: _, _, _, .vs x => fun y => + match y with + | .vz => rfl + | .vs y => congrArg (c :: ·) (remSwap x y) + +/-- Weakening `x` back past the other slot recovers `x`. -/ +theorem wkv_swp : {Γ : Ctx} → {k j : Kind} → (x : Var Γ k) → (y : Var (rem x) j) → + wkv (wkv x y) (swp x y) = x + | _ :: _, _, _, .vz => fun _ => rfl + | c :: _, _, _, .vs x => fun y => + match y with + | .vz => rfl + | .vs y => by + show Var.vs (wkv (wkv x y) (swp x y)) = Var.vs (k' := c) x + rw [wkv_swp x y] + +/-! ## Spine application unrolling -/ + +/-- `appSp` peels its last argument through `napp`. -/ +theorem appSp_cons (u : Nf Γ a) (sp : Sp Γ a (.arr b c)) (v : Nf Γ b) : + appSp u (.cons sp v) = napp (appSp u sp) v := by + cases h : appSp u sp with + | lam t => simp [appSp, napp, h] + | ne y sp' => simp [appSp, napp, h] + +/-- `substNf` at the substituted head: hand off to the spine fold. -/ +theorem substNf_ne_self (x : Var Γ k) (sp : Sp Γ k j) (u : Nf (rem x) k) : + substNf (.ne x sp) x u = appSp u (substSp sp x u) := by + simp [substNf, eqv_refl] + +/-- `substNf` at a missed head: keep the neutral. -/ +theorem substNf_ne_wkv (x : Var Γ k) (y : Var (rem x) c) (sp : Sp Γ c j) + (u : Nf (rem x) k) : + substNf (.ne (wkv x y) sp) x u = .ne y (substSp sp x u) := by + simp [substNf, eqv_wkv] + +/-! ## Embedding commutes with weakening -/ + +mutual + /-- Embedding a weakened normal form is weakening the embedding. -/ + theorem embNf_wkNf : {Γ : Ctx} → {c j : Kind} → (x : Var Γ c) → (t : Nf (rem x) j) → + embNf (wkNf x t) = wkTy x (embNf t) + | _, _, _, x, .lam (k₁ := k₁) b => by + simp only [wkNf, embNf, wkTy] + exact congrArg Ty.lam (embNf_wkNf (Var.vs (k' := k₁) x) b) + | _, _, _, _, .base n => by simp [wkNf, embNf, wkTy] + | _, _, _, x, .arrow a b => by + simp [wkNf, embNf, wkTy, embNf_wkNf x a, embNf_wkNf x b] + | _, _, _, x, .ne y sp => by + have h := embSp_wkSp x (.var y) sp + simp only [wkTy] at h + simp [wkNf, embNf, h] + termination_by _ _ _ _ t => nfSize t + decreasing_by all_goals (simp only [nfSize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Spine form of `embNf_wkNf`. -/ + theorem embSp_wkSp : {Γ : Ctx} → {c a j : Kind} → (x : Var Γ c) → (h : Ty (rem x) a) → + (sp : Sp (rem x) a j) → embSp (wkTy x h) (wkSp x sp) = wkTy x (embSp h sp) + | _, _, _, _, _, _, .nil => by simp [wkSp, embSp] + | _, _, _, _, x, h, .cons sp v => by + simp [wkSp, embSp, wkTy, embSp_wkSp x h sp, embNf_wkNf x v] + termination_by _ _ _ _ _ _ sp => spSize sp + decreasing_by all_goals (simp only [spSize]; omega) +end + +/-! ## Cancellation: substituting a freshly weakened term -/ + +mutual + /-- Substituting at a slot the term was just weakened past is the identity. -/ + theorem substNf_wkNf_cancel : {Γ : Ctx} → {k j : Kind} → (x : Var Γ k) → + (t : Nf (rem x) j) → (u : Nf (rem x) k) → substNf (wkNf x t) x u = t + | _, _, _, x, .lam (k₁ := k₁) b, u => by + simp only [wkNf, substNf] + exact congrArg Nf.lam + (substNf_wkNf_cancel (Var.vs (k' := k₁) x) b (wkNf .vz u)) + | _, _, _, _, .base n, _ => by simp [wkNf, substNf] + | _, _, _, x, .arrow a b, u => by + simp [wkNf, substNf, substNf_wkNf_cancel x a u, substNf_wkNf_cancel x b u] + | _, _, _, x, .ne y sp, u => by + simp [wkNf, substNf_ne_wkv, substSp_wkSp_cancel x sp u] + termination_by _ _ _ _ t _ => nfSize t + decreasing_by all_goals (simp only [nfSize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Spine form of `substNf_wkNf_cancel`. -/ + theorem substSp_wkSp_cancel : {Γ : Ctx} → {k a j : Kind} → (x : Var Γ k) → + (sp : Sp (rem x) a j) → (u : Nf (rem x) k) → substSp (wkSp x sp) x u = sp + | _, _, _, _, _, .nil, _ => by simp [wkSp, substSp] + | _, _, _, _, x, .cons sp v, u => by + simp [wkSp, substSp, substSp_wkSp_cancel x sp u, substNf_wkNf_cancel x v u] + termination_by _ _ _ _ _ sp _ => spSize sp + decreasing_by all_goals (simp only [spSize]; omega) +end + +/-! ## Context-cast toolkit + +The exchange laws relate removals performed in both orders; `remSwap` +equates the resulting contexts propositionally, so terms are carried +across by `Eq.rec`. Lean's definitional proof irrelevance makes every +diagonal cast vanish (`castNf_diag` is `rfl`), so instances of the +exchange laws whose contexts agree definitionally are cast-free. -/ + +/-- Transport a variable along a context equality. -/ +def castV (h : Δ = Δ') (v : Var Δ j) : Var Δ' j := h ▸ v + +/-- Transport a normal form along a context equality. -/ +def castNf (h : Δ = Δ') (t : Nf Δ j) : Nf Δ' j := h ▸ t + +/-- Transport a spine along a context equality. -/ +def castSp (h : Δ = Δ') (s : Sp Δ a j) : Sp Δ' a j := h ▸ s + +theorem castV_diag (e : Δ = Δ) (v : Var Δ j) : castV e v = v := rfl + +theorem castNf_diag (e : Δ = Δ) (t : Nf Δ j) : castNf e t = t := rfl + +theorem castSp_diag (e : Δ = Δ) (s : Sp Δ a j) : castSp e s = s := rfl + +theorem castV_vz (e : (c :: Δ : Ctx) = c :: Δ') : + castV e (.vz (k := c) (Γ := Δ)) = .vz := by + have h : Δ = Δ' := by injection e + subst h; rfl + +theorem castV_vs (e : (c :: Δ : Ctx) = c :: Δ') (h : Δ = Δ') (v : Var Δ j) : + castV e (.vs v) = .vs (castV h v) := by + subst h; rfl + +theorem castNf_lam (h : Δ = Δ') (b : Nf (k₁ :: Δ) k₂) : + castNf h (.lam b) = .lam (castNf (congrArg (k₁ :: ·) h) b) := by + subst h; rfl + +theorem castNf_base (h : Δ = Δ') (n : Nat) : + castNf h (.base n) = .base n := by + subst h; rfl + +theorem castNf_arrow (h : Δ = Δ') (a b : Nf Δ .star) : + castNf h (.arrow a b) = .arrow (castNf h a) (castNf h b) := by + subst h; rfl + +theorem castNf_ne (h : Δ = Δ') (y : Var Δ c) (sp : Sp Δ c j) : + castNf h (.ne y sp) = .ne (castV h y) (castSp h sp) := by + subst h; rfl + +theorem castSp_nil (h : Δ = Δ') : + castSp h (.nil (Γ := Δ) (k := a)) = .nil := by + subst h; rfl + +theorem castSp_cons (h : Δ = Δ') (sp : Sp Δ a (.arr b c)) (v : Nf Δ b) : + castSp h (.cons sp v) = .cons (castSp h sp) (castNf h v) := by + subst h; rfl + +theorem castNf_appSp (h : Δ = Δ') (F : Nf Δ a) (SP : Sp Δ a j) : + castNf h (appSp F SP) = appSp (castNf h F) (castSp h SP) := by + subst h; rfl + +theorem castNf_castNf (e : Δ = Δ') (e' : Δ' = Δ'') (t : Nf Δ j) : + castNf e' (castNf e t) = castNf (e.trans e') t := by + subst e; subst e'; rfl + +/-- Transporting past a fresh top slot commutes with weakening at `vz`. -/ +theorem castNf_wkNf_vz (h : Δ = Δ') (e : (c :: Δ : Ctx) = c :: Δ') (t : Nf Δ j) : + castNf e (wkNf (.vz (k := c) (Γ := Δ)) t) = wkNf .vz (castNf h t) := by + subst h; rfl + +/-- Spine form of `castNf_wkNf_vz`. -/ +theorem castSp_wkSp_vz (h : Δ = Δ') (e : (c :: Δ : Ctx) = c :: Δ') (sp : Sp Δ a j) : + castSp e (wkSp (.vz (k := c) (Γ := Δ)) sp) = wkSp .vz (castSp h sp) := by + subst h; rfl + +/-! ## Exchange of weakenings -/ + +/-- Variable-level exchange of weakenings. -/ +theorem wkv_wkv : {Γ : Ctx} → {k c j : Kind} → (x : Var Γ k) → (y : Var (rem x) c) → + (v : Var (rem y) j) → + wkv x (wkv y v) = wkv (wkv x y) (wkv (swp x y) (castV (remSwap x y).symm v)) + | _ :: _, _, _, _, .vz => fun _ _ => rfl + | c₀ :: _, _, _, _, .vs x => fun y => + match y with + | .vz => fun _ => rfl + | .vs y => fun v => + match v with + | .vz => by + have h : castV (remSwap (Var.vs (k' := c₀) x) (Var.vs (k' := c₀) y)).symm + (Var.vz (k := c₀) (Γ := rem y)) = Var.vz := castV_vz _ + rw [h] + rfl + | .vs v => by + have h : castV (remSwap (Var.vs (k' := c₀) x) (Var.vs (k' := c₀) y)).symm + (Var.vs (k' := c₀) v) = Var.vs (castV (remSwap x y).symm v) := + castV_vs _ _ v + rw [h] + show Var.vs (wkv x (wkv y v)) = _ + rw [wkv_wkv x y v] + rfl + +mutual + /-- Exchange of weakenings on normal forms. -/ + theorem wkNf_wkNf : {Γ : Ctx} → {k c j : Kind} → (x : Var Γ k) → + (y : Var (rem x) c) → (t : Nf (rem y) j) → + wkNf x (wkNf y t) = + wkNf (wkv x y) (wkNf (swp x y) (castNf (remSwap x y).symm t)) + | _, _, _, _, x, y, .lam (k₁ := k₁) b => by + rw [castNf_lam] + simp only [wkNf] + exact congrArg Nf.lam + (wkNf_wkNf (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y) b) + | _, _, _, _, x, y, .base n => by + rw [castNf_base] + simp [wkNf] + | _, _, _, _, x, y, .arrow a b => by + rw [castNf_arrow] + simp only [wkNf] + rw [wkNf_wkNf x y a, wkNf_wkNf x y b] + | _, _, _, _, x, y, .ne z sp => by + rw [castNf_ne] + simp only [wkNf] + rw [wkv_wkv x y z, wkSp_wkSp x y sp] + termination_by _ _ _ _ _ _ t => nfSize t + decreasing_by all_goals (simp only [nfSize]; first | exact Nat.lt_succ_self _ | omega) + + /-- Exchange of weakenings on spines. -/ + theorem wkSp_wkSp : {Γ : Ctx} → {k c a j : Kind} → (x : Var Γ k) → + (y : Var (rem x) c) → (sp : Sp (rem y) a j) → + wkSp x (wkSp y sp) = + wkSp (wkv x y) (wkSp (swp x y) (castSp (remSwap x y).symm sp)) + | _, _, _, _, _, x, y, .nil => by + rw [castSp_nil] + simp [wkSp] + | _, _, _, _, _, x, y, .cons sp v => by + rw [castSp_cons] + simp only [wkSp] + rw [wkSp_wkSp x y sp, wkNf_wkNf x y v] + termination_by _ _ _ _ _ _ _ sp => spSize sp + decreasing_by all_goals (simp only [spSize]; omega) +end + +/-- `substNf` at the other slot of an exchange pair: the head misses, and + the surviving position is `swp x y`. -/ +theorem substNf_ne_wkv' (x : Var Γ k) (y : Var (rem x) b) (sp : Sp Γ k j) + (W : Nf (rem (wkv x y)) b) : + substNf (.ne x sp) (wkv x y) W = .ne (swp x y) (substSp sp (wkv x y) W) := by + rw [show (Nf.ne x sp : Nf Γ j) = .ne (wkv (wkv x y) (swp x y)) sp from by + rw [wkv_swp]] + exact substNf_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 normal form. -/ + theorem substNf_wkNf : {Γ : Ctx} → {k b j : Kind} → (x : Var Γ k) → + (y : Var (rem x) b) → (s : Nf (rem x) j) → (v : Nf (rem y) b) → + (W : Nf (rem (wkv x y)) b) → + W = wkNf (swp x y) (castNf (remSwap x y).symm v) → + substNf (wkNf x s) (wkv x y) W + = wkNf (swp x y) (castNf (remSwap x y).symm (substNf s y v)) + | _, _, _, _, x, y, .lam (k₁ := k₁) s₀, v, W, hW => by + subst hW + have h1 := substNf_wkNf (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y) s₀ + (wkNf (Var.vz (k := k₁) (Γ := rem y)) v) + (wkNf (.vz (k := k₁) (Γ := rem (wkv x y))) + (wkNf (swp x y) (castNf (remSwap x y).symm v))) + ((wkNf_wkNf (Var.vz (k := k₁) (Γ := rem (wkv x y))) (swp x y) + (castNf (remSwap x y).symm v)).trans + (congrArg (wkNf (swp (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y))) + (castNf_wkNf_vz (remSwap x y).symm + (remSwap (Var.vs (k' := k₁) x) + (Var.vs (k' := k₁) y)).symm v)).symm) + simp only [wkNf, substNf] + rw [castNf_lam] + simp only [wkNf] + exact congrArg Nf.lam h1 + | _, _, _, _, x, y, .base n, v, W, hW => by + subst hW + simp only [wkNf, substNf] + rw [castNf_base] + simp [wkNf] + | _, _, _, _, x, y, .arrow a₀ b₀, v, W, hW => by + subst hW + simp only [wkNf, substNf] + rw [castNf_arrow] + simp only [wkNf] + rw [substNf_wkNf x y a₀ v _ rfl, substNf_wkNf 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 [wkNf] + rw [substNf_ne_self, substNf_ne_self, + substSp_wkSp x y sp v _ rfl, + ← wkNf_appSp (swp x y) (castNf (remSwap x y).symm v) + (castSp (remSwap x y).symm (substSp sp y v)), + ← castNf_appSp (remSwap x y).symm v (substSp sp y v)] + | _, _, sp, .diff _ z' => by + subst hW + simp only [wkNf] + rw [wkv_wkv x y z', substNf_ne_wkv, substNf_ne_wkv, + castNf_ne (remSwap x y).symm z' (substSp sp y v)] + simp only [wkNf] + rw [substSp_wkSp x y sp v _ rfl] + termination_by _ _ b _ _ _ s _ _ _ => (kindSize b, 1, nfSize s) + decreasing_by + all_goals simp only [nfSize] + 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 `substNf_wkNf`. -/ + theorem substSp_wkSp : {Γ : Ctx} → {k b a j : Kind} → (x : Var Γ k) → + (y : Var (rem x) b) → (sp : Sp (rem x) a j) → (v : Nf (rem y) b) → + (W : Nf (rem (wkv x y)) b) → + W = wkNf (swp x y) (castNf (remSwap x y).symm v) → + substSp (wkSp x sp) (wkv x y) W + = wkSp (swp x y) (castSp (remSwap x y).symm (substSp sp y v)) + | _, _, _, _, _, x, y, .nil, v, W, hW => by + subst hW + simp only [wkSp, substSp] + rw [castSp_nil] + simp [wkSp] + | _, _, _, _, _, x, y, .cons sp₀ v₀, v, W, hW => by + subst hW + simp only [wkSp, substSp] + rw [castSp_cons] + simp only [wkSp] + rw [substSp_wkSp x y sp₀ v _ rfl, substNf_wkNf x y v₀ v _ rfl] + termination_by _ _ b _ _ _ _ sp _ _ _ => (kindSize b, 1, spSize sp) + decreasing_by + all_goals simp only [spSize] + all_goals (apply Prod.Lex.right; apply Prod.Lex.right; omega) + + /-- Weakening distributes over the spine fold. -/ + theorem wkNf_appSp : {Γ : Ctx} → {cw aH j : Kind} → (w : Var Γ cw) → + (F : Nf (rem w) aH) → (SP : Sp (rem w) aH j) → + wkNf w (appSp F SP) = appSp (wkNf w F) (wkSp w SP) + | _, _, _, _, w, F, .nil => by simp [wkSp, appSp] + | _, _, _, _, w, F, .cons (b := bT) SP v => by + rw [appSp_cons] + simp only [wkSp] + rw [appSp_cons, ← wkNf_appSp w F SP] + cases appSp F SP with + | lam T => + simp only [napp, wkNf] + exact (substNf_wkNf (Var.vs (k' := bT) w) .vz T v (wkNf w v) rfl).symm + | ne yh sph => + simp [napp, wkNf, wkSp] + termination_by _ _ aH _ _ _ SP => (kindSize aH, 0, spSize SP) + decreasing_by + all_goals simp only [spSize] + all_goals first + | (apply Prod.Lex.right; apply Prod.Lex.right; omega) + | (apply Prod.Lex.left + have h := spKindLe SP + simp only [kindSize] at h ⊢ + omega) +end + +/-- Weakening distributes over `napp`. -/ +theorem wkNf_napp : {Γ : Ctx} → {cw a b : Kind} → (w : Var Γ cw) → + (F : Nf (rem w) (.arr a b)) → (A : Nf (rem w) a) → + wkNf w (napp F A) = napp (wkNf w F) (wkNf w A) + | _, _, a, _, w, .lam T, A => by + simp only [napp, wkNf] + exact (substNf_wkNf (Var.vs (k' := a) w) .vz T A (wkNf w A) rfl).symm + | _, _, _, _, w, .ne y sp, A => by + simp [napp, wkNf, wkSp] + +/-- Normalization commutes with weakening. -/ +theorem nf_wkTy : {Γ : Ctx} → {c j : Kind} → (x : Var Γ c) → (t : Ty (rem x) j) → + nf (wkTy x t) = wkNf x (nf t) + | _, _, _, x, .var y => by simp [wkTy, nf, wkNf, wkSp] + | _, _, _, x, .base n => by simp [wkTy, nf, wkNf] + | _, _, _, x, .arrow a b => by simp [wkTy, nf, wkNf, nf_wkTy x a, nf_wkTy x b] + | _, _, _, x, .lam (k₁ := k₁) b => by + simp only [wkTy, nf, wkNf] + exact congrArg Nf.lam (nf_wkTy (Var.vs (k' := k₁) x) b) + | _, _, _, x, .app f a => by + simp only [wkTy, nf] + rw [nf_wkTy x f, nf_wkTy x a, wkNf_napp] +termination_by _ _ _ _ t => tySize t +decreasing_by all_goals (simp only [tySize]; first | exact Nat.lt_succ_self _ | omega) + + +theorem castV_symm_cancel (e : Δ = Δ') (v : Var Δ' j) : + castV e (castV e.symm v) = v := by + subst e; rfl + +theorem castNf_symm_cancel (e : Δ = Δ') (t : Nf Δ' j) : + castNf e (castNf e.symm t) = t := by + subst e; rfl + +theorem castSp_symm_cancel (e : Δ = Δ') (sp : Sp Δ' a j) : + castSp e (castSp e.symm sp) = sp := by + subst e; rfl + +/-! ## Lexicographic-descent helpers + +`apply Prod.Lex.right` unifies first components syntactically, which fails +when they are equal only up to arithmetic (the sum measure below). These +intros take the comparisons as arithmetic side goals instead. -/ + +theorem lex3_lt {a₁ a₂ b₁ b₂ c₁ c₂ : Nat} (h : a₁ < a₂) : + Prod.Lex (· < ·) (Prod.Lex (· < ·) (· < ·)) (a₁, b₁, c₁) (a₂, b₂, c₂) := + Prod.Lex.left _ _ h + +theorem lex3_eq_lt {a₁ a₂ b₁ b₂ c₁ c₂ : Nat} (h : a₁ = a₂) (hb : b₁ < b₂) : + Prod.Lex (· < ·) (Prod.Lex (· < ·) (· < ·)) (a₁, b₁, c₁) (a₂, b₂, c₂) := by + subst h; exact Prod.Lex.right _ (Prod.Lex.left _ _ hb) + +theorem lex3_eq_eq_lt {a₁ a₂ b₁ b₂ c₁ c₂ : Nat} (h : a₁ = a₂) (hb : b₁ = b₂) + (hc : c₁ < c₂) : + Prod.Lex (· < ·) (Prod.Lex (· < ·) (· < ·)) (a₁, b₁, c₁) (a₂, b₂, c₂) := by + subst h; subst hb; exact Prod.Lex.right _ (Prod.Lex.right _ hc) + +/-! ## Exchange of substitutions (the substitution lemma) -/ + +mutual + /-- Exchange of hereditary substitutions: the substitution lemma. -/ + theorem substNf_substNf : {Γ : Ctx} → {k b j : Kind} → (x : Var Γ k) → + (y : Var (rem x) b) → (t : Nf Γ j) → (u : Nf (rem x) k) → + (a : Nf (rem y) b) → (W : Nf (rem (wkv x y)) b) → + W = wkNf (swp x y) (castNf (remSwap x y).symm a) → + substNf (substNf t x u) y a + = castNf (remSwap x y) + (substNf (substNf t (wkv x y) W) (swp x y) + (castNf (remSwap x y).symm (substNf u y a))) + | _, _, _, _, x, y, .lam (k₁ := k₁) t₀, u, a, W, hW => by + subst hW + have hγ : castNf (remSwap (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y)).symm + (substNf (wkNf (Var.vz (k := k₁) (Γ := rem x)) u) (Var.vs (k' := k₁) y) + (wkNf (Var.vz (k := k₁) (Γ := rem y)) a)) + = wkNf (Var.vz (k := k₁) (Γ := rem (swp x y))) + (castNf (remSwap x y).symm (substNf u y a)) := + (congrArg + (castNf (remSwap (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y)).symm) + (substNf_wkNf (Var.vz (k := k₁) (Γ := rem x)) y u a + (wkNf (Var.vz (k := k₁) (Γ := rem y)) a) rfl)).trans + (castNf_wkNf_vz (remSwap x y).symm + (remSwap (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y)).symm + (substNf u y a)) + have h1 := substNf_substNf (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y) t₀ + (wkNf (Var.vz (k := k₁) (Γ := rem x)) u) + (wkNf (Var.vz (k := k₁) (Γ := rem y)) a) + (wkNf (Var.vz (k := k₁) (Γ := rem (wkv x y))) + (wkNf (swp x y) (castNf (remSwap x y).symm a))) + ((wkNf_wkNf (Var.vz (k := k₁) (Γ := rem (wkv x y))) (swp x y) + (castNf (remSwap x y).symm a)).trans + (congrArg (wkNf (swp (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y))) + (castNf_wkNf_vz (remSwap x y).symm + (remSwap (Var.vs (k' := k₁) x) + (Var.vs (k' := k₁) y)).symm a)).symm) + simp only [substNf] + rw [castNf_lam] + exact congrArg Nf.lam (h1.trans (congrArg + (castNf (remSwap (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y))) + (congrArg + (substNf (substNf t₀ (wkv (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y)) + (wkNf (Var.vz (k := k₁) (Γ := rem (wkv x y))) + (wkNf (swp x y) (castNf (remSwap x y).symm a)))) + (swp (Var.vs (k' := k₁) x) (Var.vs (k' := k₁) y))) + hγ))) + | _, _, _, _, x, y, .base n, u, a, W, hW => by + subst hW + simp only [substNf] + rw [castNf_base] + | _, _, _, _, x, y, .arrow a₀ b₀, u, a, W, hW => by + subst hW + simp only [substNf] + rw [castNf_arrow] + rw [substNf_substNf x y a₀ u a _ rfl, substNf_substNf x y b₀ u a _ rfl] + | _, _, _, _, x, y, .ne (k := c) z sp, u, a, W, hW => + match c, z, sp, eqv x z with + | _, _, sp, .same => by + subst hW + rw [substNf_ne_self, substNf_appSp u (substSp sp x u) y a, + substSp_substSp x y sp u a _ rfl, + substNf_ne_wkv', substNf_ne_self, castNf_appSp, + castNf_symm_cancel] + | _, _, sp, .diff _ z' => + match c, z', sp, eqv y z' with + | _, _, sp, .same => by + subst hW + rw [substNf_ne_wkv, substNf_ne_self, substNf_ne_self, + substSp_substSp x y sp u a _ rfl, + substNf_appSp _ _ (swp x y) _, + substNf_wkNf_cancel, castNf_appSp, castNf_symm_cancel] + | _, _, sp, .diff _ z'' => by + subst hW + rw [substNf_ne_wkv, substNf_ne_wkv, + substSp_substSp x y sp u a _ rfl, + wkv_wkv x y z'', substNf_ne_wkv, substNf_ne_wkv, + castNf_ne, castV_symm_cancel] + termination_by _ k b _ x y t _ _ _ _ => (kindSize k + kindSize b, 1, nfSize t) + decreasing_by + all_goals simp only [nfSize] + all_goals first + | exact lex3_eq_eq_lt (by omega) rfl + (by first | omega | exact Nat.lt_succ_self _) + | exact lex3_eq_lt (by omega) (by omega) + + /-- Spine form of the substitution lemma. -/ + theorem substSp_substSp : {Γ : Ctx} → {k b aS j : Kind} → (x : Var Γ k) → + (y : Var (rem x) b) → (sp : Sp Γ aS j) → (u : Nf (rem x) k) → + (a : Nf (rem y) b) → (W : Nf (rem (wkv x y)) b) → + W = wkNf (swp x y) (castNf (remSwap x y).symm a) → + substSp (substSp sp x u) y a + = castSp (remSwap x y) + (substSp (substSp sp (wkv x y) W) (swp x y) + (castNf (remSwap x y).symm (substNf u y a))) + | _, _, _, _, _, x, y, .nil, u, a, W, hW => by + subst hW + simp only [substSp] + rw [castSp_nil] + | _, _, _, _, _, x, y, .cons sp₀ v₀, u, a, W, hW => by + subst hW + simp only [substSp] + rw [castSp_cons] + rw [substSp_substSp x y sp₀ u a _ rfl, substNf_substNf x y v₀ u a _ rfl] + termination_by _ k b _ _ x y sp _ _ _ _ => (kindSize k + kindSize b, 1, spSize sp) + decreasing_by + all_goals simp only [spSize] + all_goals first + | exact lex3_eq_eq_lt (by omega) rfl + (by first | omega | exact Nat.lt_succ_self _) + | exact lex3_eq_lt (by omega) (by omega) + + /-- Hereditary substitution distributes over the spine fold. -/ + theorem substNf_appSp : {Δ : Ctx} → {aH kq j : Kind} → (F : Nf Δ aH) → + (SP : Sp Δ aH j) → (q : Var Δ kq) → (w : Nf (rem q) kq) → + substNf (appSp F SP) q w = appSp (substNf F q w) (substSp SP q w) + | _, _, _, _, F, .nil, q, w => by simp [appSp, substSp] + | Δ, _, _, _, F, .cons (b := bT) SP v, q, w => by + rw [appSp_cons] + simp only [substSp] + rw [appSp_cons, ← substNf_appSp F SP q w] + cases appSp F SP with + | lam T => + simp only [napp, substNf] + exact substNf_substNf (Var.vz (k := bT) (Γ := Δ)) q T v w + (wkNf (Var.vz (k := bT) (Γ := rem q)) w) rfl + | ne yh sph => + cases eqv q yh with + | same => + simp only [napp] + rw [substNf_ne_self, substNf_ne_self] + simp only [substSp] + rw [appSp_cons] + rfl + | diff _ qz => + simp only [napp] + rw [substNf_ne_wkv, substNf_ne_wkv] + simp only [substSp] + termination_by _ aH kq _ _ SP _ _ => (kindSize aH + kindSize kq, 0, spSize SP) + decreasing_by + all_goals simp only [spSize] + all_goals first + | exact lex3_eq_eq_lt (by omega) rfl + (by first | omega | exact Nat.lt_succ_self _) + | exact lex3_eq_lt (by omega) (by omega) + | exact lex3_lt (by + have h := spKindLe SP + simp only [kindSize] at h ⊢ + omega) +end + + +/-- Hereditary substitution distributes over `napp`. -/ +theorem substNf_napp : {Γ : Ctx} → {a b kq : Kind} → (F : Nf Γ (.arr a b)) → + (A : Nf Γ a) → (q : Var Γ kq) → (w : Nf (rem q) kq) → + substNf (napp F A) q w = napp (substNf F q w) (substNf A q w) + | Γ, a, _, _, .lam T, A, q, w => by + simp only [napp, substNf] + exact substNf_substNf (Var.vz (k := a) (Γ := Γ)) q T A w + (wkNf (Var.vz (k := a) (Γ := rem q)) w) rfl + | _, _, _, _, .ne yh sph, A, q, w => by + cases eqv q yh with + | same => + simp only [napp] + rw [substNf_ne_self, substNf_ne_self] + simp only [substSp] + rw [appSp_cons] + rfl + | diff _ qz => + simp only [napp] + rw [substNf_ne_wkv, substNf_ne_wkv] + simp only [substSp] + +/-- Normalization commutes with syntactic substitution — the main + Keller-Altenkirch commutation equation for ET-2. -/ +theorem nf_substTy : {Γ : Ctx} → {j k : Kind} → (t : Ty Γ j) → (x : Var Γ k) → + (u : Ty (rem x) k) → nf (substTy t x u) = substNf (nf t) x (nf u) + | _, j, _, .var z, x, u => + match j, z, eqv x z with + | _, _, .same => by + simp only [nf] + rw [substNf_ne_self] + simp [substTy, eqv_refl, appSp, substSp] + | _, _, .diff _ z' => by + simp only [nf] + rw [substNf_ne_wkv] + simp [substTy, eqv_wkv, substSp, nf] + | _, _, _, .base n, x, u => by simp [substTy, nf, substNf] + | _, _, _, .arrow a b, x, u => by + simp only [substTy, nf, substNf] + rw [nf_substTy a x u, nf_substTy b x u] + | _, _, _, .lam (k₁ := k₁) b, x, u => by + simp only [substTy, nf, substNf] + exact congrArg Nf.lam + ((nf_substTy b (Var.vs (k' := k₁) x) + (wkTy (Var.vz (k := k₁) (Γ := rem x)) u)).trans + (congrArg (substNf (nf b) (Var.vs (k' := k₁) x)) + (nf_wkTy (Var.vz (k := k₁) (Γ := rem x)) u))) + | _, _, _, .app f a, x, u => by + simp only [substTy, nf] + rw [nf_substTy f x u, nf_substTy a x u, substNf_napp] +termination_by _ _ _ t _ _ => tySize t +decreasing_by all_goals (simp only [tySize]; first | exact Nat.lt_succ_self _ | omega) + +end Systemet.L1