|
1 | 1 | {-# OPTIONS --safe --without-K #-} |
2 | 2 |
|
3 | | --- Phase 1.3 — STATUS: scaffolding only. The recursive `_≤′_` |
4 | | --- definition lands here, plus `osuc-mono-≤′ p = p` (the bullseye |
5 | | --- lemma). `≤′-refl` for the `olim f` case requires `f-in-lim′`, |
6 | | --- which is the documented obstacle described below. |
7 | | --- |
8 | | --- This module compiles under `--safe --without-K`. Anything that |
9 | | --- depends on the open `f-in-lim′` is left out so the file is honest: |
10 | | --- what's here is provable, what's not here is exactly the work |
11 | | --- remaining. |
12 | | --- |
13 | | --- ## Background |
14 | | --- |
15 | | --- Echidna's SA design-search recommended switching `Ordinal.Brouwer._≤_` |
16 | | --- to a fully-recursive shape (energy [0, 0, 1, 0]; both single-chain |
17 | | --- and 4-agent swarm unanimous). The data-style alternative |
18 | | --- (`data + ≤-cong-suc`) was tested by hand-trace and rejected — the |
19 | | --- new constructor cascades into mutually-recursive `pred-of-osuc` |
20 | | --- proofs that need to be redesigned alongside. |
| 3 | +-- Phase 1.3 — recursive `_≤′_` per Echidna's SA + 4-agent swarm |
| 4 | +-- recommendation (energy [0, 0, 1, 0]; both unanimous). Replaces |
| 5 | +-- the data-style `Ordinal.Brouwer._≤_` for the cases where |
| 6 | +-- `osuc-mono` and structural shape matter, while leaving the |
| 7 | +-- data-style intact so the existing `wf-<` proof keeps composing. |
21 | 8 | -- |
22 | 9 | -- See `echidna/docs/decisions/2026-04-28-corpus-and-design-search.md` |
23 | 10 | -- and `echo-types/docs/echidna-design-search-2026-04-28.adoc` for |
24 | 11 | -- the full design-search log. |
25 | 12 | -- |
26 | | --- ## What's done |
27 | | --- |
28 | | --- * Recursive `_≤′_` defined; passes Agda's coverage + termination |
29 | | --- checks under `--safe --without-K`. |
30 | | --- * `osuc-mono-≤′ p = p` — the Phase-1.3 bullseye is identity. |
31 | | --- * `≤′-zero` — definitional from the `oz ≤ _ = ⊤` clause. |
32 | | --- * `osuc-mono-<′` — strict version, also identity-shaped. |
33 | | --- |
34 | | --- ## What's open |
| 13 | +-- ## What's here |
35 | 14 | -- |
36 | | --- * `≤′-refl` for the `olim f` case is `(n : ℕ) → f n ≤′ olim f`, |
37 | | --- which requires `f-in-lim′ : ∀ f n → f n ≤′ olim f`. The |
38 | | --- `f-in-lim′` proof has three sub-cases (per `f n`'s constructor); |
39 | | --- the `oz` and `osuc α` cases are routine, but the `olim g` case |
40 | | --- (where `f n = olim g`) is the documented obstacle. |
| 15 | +-- * Recursive `_≤′_` and derived `_<′_`. |
| 16 | +-- * `osuc-mono-≤′ p = p`, `osuc-mono-<′ p = p` — the Phase-1.3 |
| 17 | +-- bullseyes collapse to identity under the recursive shape. |
| 18 | +-- * `≤′-zero`, `oz<′osuc` — trivial corollaries. |
| 19 | +-- * `≤′-lim` — the source-side limit-introduction lemma. |
| 20 | +-- * `≤′-refl` — reflexivity, with the `olim f` case discharged by |
| 21 | +-- `≤′-lim n (≤′-refl {f n})`. The recursive call on `f n` is |
| 22 | +-- structurally smaller than `olim f` per Agda's subterm relation |
| 23 | +-- for higher-order inductive constructors. |
| 24 | +-- * `f-in-lim′` — direct corollary `f n ≤′ olim f`, the recursive |
| 25 | +-- analogue of `Ordinal.Brouwer.f-in-lim`. |
| 26 | +-- * `≤′-trans` — transitivity, by lex structural recursion on |
| 27 | +-- `(α, β, γ)`. Together with `≤′-refl` this makes `_≤′_` a |
| 28 | +-- preorder; `_<′_` strict-order companions follow downstream. |
| 29 | +-- * `wf-<′` — well-foundedness of `_<′_`, by structural induction |
| 30 | +-- on `Ord` mirroring `Ordinal.Brouwer.wf-<`. Predecessor lemmas |
| 31 | +-- `pred-of-osuc-<′` and `pred-of-olim-<′` reduce through the |
| 32 | +-- computed shape of `_<′_` rather than constructor pattern-match. |
41 | 33 | -- |
42 | | --- The `olim g` case wants `(m : ℕ) → g m ≤′ olim f`. Termination is |
43 | | --- fine — `g m` is strictly smaller than `f n = olim g`, so structural |
44 | | --- recursion goes through — but Agda's `with f n` pattern loses the |
45 | | --- equation `f n ≡ olim g`, leaving the goal in a shape Foetus can't |
46 | | --- verify is decreasing. |
| 34 | +-- ## Closure of the original obstacle |
47 | 35 | -- |
48 | | --- Two viable closure paths: |
49 | | --- |
50 | | --- 1. Mutual definition with `≤′-trans`. Then the `olim g` case |
51 | | --- becomes `≤′-trans (f-in-lim′ g m) (f-in-lim′ f n)` — both |
52 | | --- calls are structurally smaller, and Foetus accepts mutual |
53 | | --- structural recursion when each call shrinks one of the |
54 | | --- lex-ordered measures. |
55 | | --- |
56 | | --- 2. Strengthen `f-in-lim′` to carry an accessibility witness for |
57 | | --- the limit — `(∀ k → Acc _<′_ (f k)) → f n ≤′ olim f`. This |
58 | | --- makes the recursion structure visible to Foetus directly. |
59 | | --- |
60 | | --- The Phase-1.3 follow-up commit lands either path; for now the |
61 | | --- recursive shape stands up + the bullseye lemma compiles. |
| 36 | +-- The earlier draft deferred `≤′-refl` for `olim f` because the |
| 37 | +-- naïve `f-in-lim′` recursion on `f n`'s constructor lost the |
| 38 | +-- equation `f n ≡ olim g` under `with`, blocking Foetus. The |
| 39 | +-- closure here factors through `≤′-lim`, which recurses on the |
| 40 | +-- source α (not on `f n`). Termination is then immediate: `α` |
| 41 | +-- shrinks structurally on each recursive call, independent of `f`. |
62 | 42 |
|
63 | 43 | module Ordinal.Brouwer.Phase13 where |
64 | 44 |
|
65 | 45 | open import Data.Nat.Base using (ℕ) |
66 | | -open import Data.Product.Base using (Σ) |
| 46 | +open import Data.Product.Base using (Σ; _,_) |
67 | 47 | open import Data.Unit.Base using (⊤; tt) |
68 | | -open import Data.Empty using (⊥) |
| 48 | +open import Data.Empty using (⊥; ⊥-elim) |
| 49 | +open import Induction.WellFounded using (Acc; acc; WellFounded) |
69 | 50 |
|
70 | 51 | open import Ordinal.Brouwer using (Ord; oz; osuc; olim) |
71 | 52 |
|
@@ -116,3 +97,95 @@ osuc-mono-<′ p = p |
116 | 97 |
|
117 | 98 | oz<′osuc : ∀ {α} → oz <′ osuc α |
118 | 99 | oz<′osuc {α} = ≤′-zero {α} |
| 100 | + |
| 101 | +---------------------------------------------------------------------------- |
| 102 | +-- Limit-introduction and reflexivity (Phase-1.3 closure) |
| 103 | +---------------------------------------------------------------------------- |
| 104 | + |
| 105 | +-- Source-side limit introduction. Any α that is `≤′`-below some |
| 106 | +-- branch `f n` is also `≤′`-below the limit `olim f`. Structural |
| 107 | +-- recursion on the source α; the implicit `f` is threaded |
| 108 | +-- unchanged. |
| 109 | +-- |
| 110 | +-- This is the lemma that breaks the original obstacle. The blocked |
| 111 | +-- attempt recursed on `f n`'s constructor, which loses the equation |
| 112 | +-- under `with`. Recursing on α is fine: each constructor of the |
| 113 | +-- source admits a direct construction of the limit-shaped result. |
| 114 | + |
| 115 | +-- `f` is explicit because Agda can't infer it from the value `f n` |
| 116 | +-- (the unification problem `_f_ n = f n` is non-unique — many |
| 117 | +-- functions agree at a single point). Each call site passes the |
| 118 | +-- intended `f` directly. |
| 119 | + |
| 120 | +≤′-lim : ∀ {α} (f : ℕ → Ord) (n : ℕ) → α ≤′ f n → α ≤′ olim f |
| 121 | +≤′-lim {oz} f n p = tt |
| 122 | +≤′-lim {osuc α} f n p = n , p |
| 123 | +≤′-lim {olim g} f n p = λ m → ≤′-lim {α = g m} f n (p m) |
| 124 | + |
| 125 | +-- Reflexivity. Structural recursion on α; the `olim f` case |
| 126 | +-- threads through `≤′-lim` at each branch. |
| 127 | + |
| 128 | +≤′-refl : ∀ {α} → α ≤′ α |
| 129 | +≤′-refl {oz} = tt |
| 130 | +≤′-refl {osuc α} = ≤′-refl {α} |
| 131 | +≤′-refl {olim f} = λ n → ≤′-lim {α = f n} f n (≤′-refl {f n}) |
| 132 | + |
| 133 | +-- Each branch of a limit sits at-or-below it. Recursive analogue |
| 134 | +-- of `Ordinal.Brouwer.f-in-lim`. Falls out of `≤′-lim` plus |
| 135 | +-- reflexivity at the branch. |
| 136 | + |
| 137 | +f-in-lim′ : ∀ f n → f n ≤′ olim f |
| 138 | +f-in-lim′ f n = ≤′-lim {α = f n} f n (≤′-refl {f n}) |
| 139 | + |
| 140 | +---------------------------------------------------------------------------- |
| 141 | +-- Transitivity (Phase-1.3 round-out) |
| 142 | +---------------------------------------------------------------------------- |
| 143 | + |
| 144 | +-- Recursion on (α, β, γ) under the lex order. Each non-base case |
| 145 | +-- either terminates immediately on a ⊥ leg or recurses with one of |
| 146 | +-- the three positions a strict structural subterm and the others |
| 147 | +-- syntactically unchanged. Agda's structural-recursion checker |
| 148 | +-- accepts this as lex-decreasing; no explicit measure annotation |
| 149 | +-- needed. |
| 150 | + |
| 151 | +≤′-trans : ∀ {α β γ} → α ≤′ β → β ≤′ γ → α ≤′ γ |
| 152 | +≤′-trans {oz} _ _ = tt |
| 153 | +≤′-trans {osuc _} {oz} p _ = ⊥-elim p |
| 154 | +≤′-trans {osuc _} {osuc _} {oz} _ q = ⊥-elim q |
| 155 | +≤′-trans {osuc α} {osuc β} {osuc γ} p q = ≤′-trans {α} {β} {γ} p q |
| 156 | +≤′-trans {osuc α} {osuc β} {olim h} p (k , q) = k , ≤′-trans {osuc α} {osuc β} {h k} p q |
| 157 | +≤′-trans {osuc α} {olim g} {γ} (n , p) q = ≤′-trans {osuc α} {g n} {γ} p (q n) |
| 158 | +≤′-trans {olim f} {β} {γ} p q = λ n → ≤′-trans {f n} {β} {γ} (p n) q |
| 159 | + |
| 160 | +---------------------------------------------------------------------------- |
| 161 | +-- Well-foundedness of `_<′_` (path (a) of the handoff) |
| 162 | +---------------------------------------------------------------------------- |
| 163 | + |
| 164 | +-- The data-style `wf-<` proof recurses on the three constructors of |
| 165 | +-- `_≤_`. Here `_≤′_` is recursive — there are no constructors to |
| 166 | +-- pattern-match on — so the predecessor lemmas reduce predecessors |
| 167 | +-- through the computed shape of `_<′_`: |
| 168 | +-- |
| 169 | +-- β <′ osuc α ≡ osuc β ≤′ osuc α ≡ β ≤′ α |
| 170 | +-- β <′ olim f ≡ Σ ℕ (λ n → β <′ f n) |
| 171 | +-- β <′ oz ≡ ⊥ |
| 172 | +-- |
| 173 | +-- so the `osuc` case is "lift hypothetical predecessors of β through |
| 174 | +-- ≤′-trans to predecessors of α", and the `olim` case is the same |
| 175 | +-- branch-selection move as the data-style `pred-of-olim`. |
| 176 | + |
| 177 | +pred-of-osuc-<′ : ∀ {α} → Acc _<′_ α → ∀ {β} → β <′ osuc α → Acc _<′_ β |
| 178 | +pred-of-osuc-<′ {α} (acc rsα) {β} p = |
| 179 | + acc (λ {γ} q → rsα (≤′-trans {osuc γ} {β} {α} q p)) |
| 180 | + |
| 181 | +pred-of-olim-<′ : ∀ {f} → (∀ n → Acc _<′_ (f n)) → ∀ {β} → β <′ olim f → Acc _<′_ β |
| 182 | +pred-of-olim-<′ wfs (n , q) with wfs n |
| 183 | +... | acc rs = rs q |
| 184 | + |
| 185 | +-- Top-level WF: structural induction on `Ord`. Mirrors `wf-<`'s |
| 186 | +-- shape; differs only in the predecessor lemmas above. |
| 187 | + |
| 188 | +wf-<′ : WellFounded _<′_ |
| 189 | +wf-<′ oz = acc (λ {β} ()) |
| 190 | +wf-<′ (osuc α) = acc (pred-of-osuc-<′ (wf-<′ α)) |
| 191 | +wf-<′ (olim f) = acc (pred-of-olim-<′ (λ n → wf-<′ (f n))) |
0 commit comments