|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Leading-Ω-index head function for Buchholz terms. First slice of the |
| 4 | +-- planned closure of the last open per-constructor case `<ᵇ-+1` |
| 5 | +-- joint-bplus in the Buchholz rank-monotonicity matrix |
| 6 | +-- (`docs/echo-types/buchholz-rank-obstruction.adoc` §"What remains |
| 7 | +-- open"). |
| 8 | +-- |
| 9 | +-- ## The closure plan (option A from RankPow.agda's preamble) |
| 10 | +-- |
| 11 | +-- The `<ᵇ-+1` joint-bplus case fails to discharge under `rank-pow` |
| 12 | +-- alone because `rank-pow (bplus z₁ z₂)` is not additive principal in |
| 13 | +-- general — `rank-pow y₁` (the left summand of the *target*) need not |
| 14 | +-- close ⊕-sums of subterm ranks. The recommended unblock per the |
| 15 | +-- obstruction doc is to dominate `rank-pow t` by an additive-principal |
| 16 | +-- ω-power indexed by the leading Ω-marker of `t`, and then discharge |
| 17 | +-- `<ᵇ-+1` via head-Ω inversion + additive-principal at head-Ω's |
| 18 | +-- successor. |
| 19 | +-- |
| 20 | +-- This module lands the *head-Ω function itself* and its definitional |
| 21 | +-- sanity lemmas. The downstream rank-mono / domination work is |
| 22 | +-- deferred to follow-on slices, so that the head-Ω abstraction stands |
| 23 | +-- on its own merits before any rank consumer pulls on it. |
| 24 | +-- |
| 25 | +-- ## What lands in this slice |
| 26 | +-- |
| 27 | +-- * `head-Ω : BT → OmegaIndex` — the leading-Ω-index head function. |
| 28 | +-- Returns the leftmost-deepest Ω marker carried by the term, with |
| 29 | +-- `fin 0` as the default for `bzero` (which has none — the future |
| 30 | +-- rank-mono lemma will guard this case explicitly via a non-bzero |
| 31 | +-- premise). |
| 32 | +-- * `head-Ω-bzero`, `head-Ω-bOmega`, `head-Ω-bplus`, `head-Ω-bpsi` — |
| 33 | +-- definitional sanity lemmas, one per `BT` constructor. These |
| 34 | +-- lemmas are `refl` (the equations are the definition); they exist |
| 35 | +-- so downstream code can rewrite by them without unfolding |
| 36 | +-- `head-Ω` directly. |
| 37 | +-- |
| 38 | +-- ## What is deferred to follow-on slices |
| 39 | +-- |
| 40 | +-- * `head-Ω-mono` family (head-Ω respecting WfCNF / WfAdm structural |
| 41 | +-- bounds). Needs the rank-domination lemma to be stated first. |
| 42 | +-- * `rank-pow-dominated-by-head-Ω : (t : BT) → NonBzero t → WfCNF t → |
| 43 | +-- rank-pow t <′ ω-rank-pow-succ (head-Ω t)` (the load-bearing |
| 44 | +-- domination lemma). Needs an `ω-rank-pow-succ : OmegaIndex → |
| 45 | +-- Ord` (one option: `ω-rank-pow-succ (fin n) = ω^(suc (suc n))`, |
| 46 | +-- `ω-rank-pow-succ ω = olim (λ n → ω^(suc (suc n)))`) plus a |
| 47 | +-- structural recursion on `WfCNF t` using |
| 48 | +-- `rank-pow-bplus-into-ω-rank-pow` at each `bplus` step. |
| 49 | +-- * `rank-mono-<ᵇ-+1-via-head-Ω` (the headline discharge). Builds |
| 50 | +-- on the domination lemma + `rank-mono-<ᵇ-+1-via-target` from |
| 51 | +-- `RankPow.agda`. |
| 52 | + |
| 53 | +module Ordinal.Buchholz.HeadOmega where |
| 54 | + |
| 55 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 56 | + |
| 57 | +open import Ordinal.OmegaMarkers using (OmegaIndex; fin; ω) |
| 58 | +open import Ordinal.Buchholz.Syntax using |
| 59 | + ( BT |
| 60 | + ; bzero |
| 61 | + ; bOmega |
| 62 | + ; bplus |
| 63 | + ; bpsi |
| 64 | + ) |
| 65 | + |
| 66 | +---------------------------------------------------------------------- |
| 67 | +-- `head-Ω : BT → OmegaIndex` — leading-Ω-index head function |
| 68 | +---------------------------------------------------------------------- |
| 69 | + |
| 70 | +-- The leftmost-deepest Ω marker carried by the term. |
| 71 | +-- |
| 72 | +-- * `bzero` ↦ `fin 0` (default; bzero has no Ω marker — the |
| 73 | +-- future rank-mono lemma will require a |
| 74 | +-- non-bzero premise so this default is never |
| 75 | +-- consumed in proofs). |
| 76 | +-- * `bOmega ν` ↦ `ν` (the Ω marker IS ν). |
| 77 | +-- * `bplus x y` ↦ `head-Ω x` (leftmost — the WfCNF tail bound |
| 78 | +-- `y ≤ᵇ x` means y's leading Ω is dominated by |
| 79 | +-- x's, so the leftmost is also the deepest). |
| 80 | +-- * `bpsi ν α` ↦ `ν` (the ψ-binder's Ω-index dominates the |
| 81 | +-- argument α, mirroring the provisional |
| 82 | +-- `rank-pow (bpsi ν α) = ω-rank-pow ν` shape in |
| 83 | +-- `RankPow.agda`). |
| 84 | +-- |
| 85 | +-- Termination is structural (size-decreasing on the first argument |
| 86 | +-- of `bplus`), no decreasing measure needed. |
| 87 | + |
| 88 | +head-Ω : BT → OmegaIndex |
| 89 | +head-Ω bzero = fin 0 |
| 90 | +head-Ω (bOmega ν) = ν |
| 91 | +head-Ω (bplus x _) = head-Ω x |
| 92 | +head-Ω (bpsi ν _) = ν |
| 93 | + |
| 94 | +---------------------------------------------------------------------- |
| 95 | +-- Definitional sanity, one lemma per `BT` constructor |
| 96 | +---------------------------------------------------------------------- |
| 97 | + |
| 98 | +-- These are all `refl` — they record the defining equations so that |
| 99 | +-- downstream slices can rewrite by them at consumer sites without |
| 100 | +-- unfolding `head-Ω` (or, equivalently, naming the equations |
| 101 | +-- explicitly when the unfolding is inconvenient in tactic position). |
| 102 | + |
| 103 | +head-Ω-bzero : head-Ω bzero ≡ fin 0 |
| 104 | +head-Ω-bzero = refl |
| 105 | + |
| 106 | +head-Ω-bOmega : ∀ ν → head-Ω (bOmega ν) ≡ ν |
| 107 | +head-Ω-bOmega _ = refl |
| 108 | + |
| 109 | +head-Ω-bplus : ∀ x y → head-Ω (bplus x y) ≡ head-Ω x |
| 110 | +head-Ω-bplus _ _ = refl |
| 111 | + |
| 112 | +head-Ω-bpsi : ∀ ν α → head-Ω (bpsi ν α) ≡ ν |
| 113 | +head-Ω-bpsi _ _ = refl |
| 114 | + |
| 115 | +---------------------------------------------------------------------- |
| 116 | +-- Compositional convenience |
| 117 | +---------------------------------------------------------------------- |
| 118 | + |
| 119 | +-- `head-Ω` of a left-leaning `bplus` chain bottoms out at the |
| 120 | +-- leftmost atom's leading Ω. Direct consequence of `head-Ω-bplus` |
| 121 | +-- applied twice; provided as a named lemma because the two-level |
| 122 | +-- pattern recurs in any rank-mono discharge that walks the WfCNF |
| 123 | +-- left spine of a `bplus`. |
| 124 | + |
| 125 | +head-Ω-bplus-left : ∀ x y z → head-Ω (bplus (bplus x y) z) ≡ head-Ω x |
| 126 | +head-Ω-bplus-left _ _ _ = refl |
0 commit comments