-
-
Notifications
You must be signed in to change notification settings - Fork 0
proofs(lean4): land the green half of the η extension (PARTIAL — ET-1..3 η) #34
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,46 @@ | ||
| -- SPDX-License-Identifier: MPL-2.0 | ||
| -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> | ||
| 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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,77 @@ | ||
| -- SPDX-License-Identifier: MPL-2.0 | ||
| -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> | ||
| 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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,104 @@ | ||
| -- SPDX-License-Identifier: MPL-2.0 | ||
| -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> | ||
| 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 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,86 @@ | ||
| -- SPDX-License-Identifier: MPL-2.0 | ||
| -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> | ||
| 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 |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.