|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Phase 1.2 of the Option B programme (see `docs/buchholz-plan.adoc`). |
| 4 | +-- |
| 5 | +-- Ordinal arithmetic on Brouwer notations: *definitions* only. |
| 6 | +-- All non-trivial monotonicity proofs are scheduled for Phase 1.3, |
| 7 | +-- where they may drive a small redesign of `_≤_` in the base |
| 8 | +-- `Ordinal.Brouwer` module (the current data-type axiomatisation |
| 9 | +-- proves key lemmas like `osuc-mono-≤` only with some care, and |
| 10 | +-- the Phase 1.3 work will decide whether to add constructors or |
| 11 | +-- switch to a recursive `_≤_`). |
| 12 | +-- |
| 13 | +-- Contents: |
| 14 | +-- |
| 15 | +-- * `_⊕_` — left-recursive naive ordinal sum. Not Hessenberg; the |
| 16 | +-- full natural-sum definition (commutative + bi-monotonic) needs |
| 17 | +-- more machinery than pays off for the rank we actually need. |
| 18 | +-- This is the cheapest sum that still lets `psi-rank` propagate |
| 19 | +-- ordinal-argument descent via right-monotonicity, which is the |
| 20 | +-- only direction we need for Phase 2.2. |
| 21 | +-- * `nat-to-ord` — the standard successor-stack encoding of ℕ. |
| 22 | +-- * `ω-rank : OmegaIndex → Ord` — rank for Ω-markers. `fin n` maps |
| 23 | +-- to `osuc^(n+1) oz`, `ω` maps to the canonical Brouwer ω. |
| 24 | +-- * `psi-rank : OmegaIndex → Ord → Ord` — rank for ψ-terms, shape |
| 25 | +-- `osuc (ω-rank ν ⊕ α)`. The outer successor guarantees |
| 26 | +-- `ω-rank ν < psi-rank ν α` regardless of α; the `⊕ α` tail |
| 27 | +-- carries the ψ-argument's rank so that `<ᵇ-ψα α<β` descends |
| 28 | +-- via right-monotonicity of `⊕`. |
| 29 | + |
| 30 | +module Ordinal.Brouwer.Arithmetic where |
| 31 | + |
| 32 | +open import Data.Nat.Base using (ℕ; zero; suc) |
| 33 | + |
| 34 | +open import Ordinal.OmegaMarkers using (OmegaIndex; fin; ω) |
| 35 | +open import Ordinal.Brouwer using (Ord; oz; osuc; olim) |
| 36 | + |
| 37 | +---------------------------------------------------------------------------- |
| 38 | +-- Naive ordinal sum |
| 39 | +---------------------------------------------------------------------------- |
| 40 | + |
| 41 | +-- Left-recursive: zero on the left is the unit definitionally, |
| 42 | +-- successor on the left lifts the successor past the sum, limit on |
| 43 | +-- the left distributes under the sum. |
| 44 | + |
| 45 | +infixl 6 _⊕_ |
| 46 | + |
| 47 | +_⊕_ : Ord → Ord → Ord |
| 48 | +oz ⊕ β = β |
| 49 | +osuc α ⊕ β = osuc (α ⊕ β) |
| 50 | +olim f ⊕ β = olim (λ n → f n ⊕ β) |
| 51 | + |
| 52 | +---------------------------------------------------------------------------- |
| 53 | +-- Rank target for Ω-indices |
| 54 | +---------------------------------------------------------------------------- |
| 55 | + |
| 56 | +-- Standard encoding of ℕ into Ord as a successor stack. |
| 57 | + |
| 58 | +nat-to-ord : ℕ → Ord |
| 59 | +nat-to-ord zero = oz |
| 60 | +nat-to-ord (suc n) = osuc (nat-to-ord n) |
| 61 | + |
| 62 | +-- Rank of an Ω-marker. `fin n` goes to a successor stack of length |
| 63 | +-- `n + 1`; `ω` goes to the canonical Brouwer ω. The `+ 1` offset |
| 64 | +-- keeps `ω-rank (fin 0)` strictly above `oz = rank bzero` so the |
| 65 | +-- `<ᵇ-0-Ω` constructor descends into `<Ord` in Phase 2.2. |
| 66 | + |
| 67 | +ω-rank : OmegaIndex → Ord |
| 68 | +ω-rank (fin n) = nat-to-ord (suc n) |
| 69 | +ω-rank ω = olim nat-to-ord |
| 70 | + |
| 71 | +---------------------------------------------------------------------------- |
| 72 | +-- Rank target for ψ-terms |
| 73 | +---------------------------------------------------------------------------- |
| 74 | + |
| 75 | +-- `psi-rank ν α = osuc (ω-rank ν ⊕ α)`. The outer `osuc` is what |
| 76 | +-- `<ᵇ-0-ψ` / `<ᵇ-ψΩ≤` need (strict domination of bzero / Ω-rank); |
| 77 | +-- the `⊕ α` tail is what `<ᵇ-ψα` needs (right-monotonic descent on |
| 78 | +-- the ψ-argument). |
| 79 | + |
| 80 | +psi-rank : OmegaIndex → Ord → Ord |
| 81 | +psi-rank ν α = osuc (ω-rank ν ⊕ α) |
| 82 | + |
| 83 | +---------------------------------------------------------------------------- |
| 84 | +-- Definitional sanity checks (no proofs, just unit tests via ≡) |
| 85 | +---------------------------------------------------------------------------- |
| 86 | + |
| 87 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl) |
| 88 | +open import Ordinal.Brouwer using (one; two) |
| 89 | + |
| 90 | +-- The smallest Ω-rank is strictly above zero. |
| 91 | + |
| 92 | +ω-rank-fin0 : ω-rank (fin 0) ≡ one |
| 93 | +ω-rank-fin0 = refl |
| 94 | + |
| 95 | +ω-rank-fin1 : ω-rank (fin 1) ≡ two |
| 96 | +ω-rank-fin1 = refl |
| 97 | + |
| 98 | +-- `psi-rank ν oz = osuc (ω-rank ν ⊕ oz)`. Since `⊕`'s right-identity |
| 99 | +-- is only up to `≤` (proved in Phase 1.3), we don't state `≡` here. |
| 100 | + |
| 101 | +-- Left-unit of `⊕` is definitional. |
| 102 | + |
| 103 | +⊕-oz-left : ∀ β → oz ⊕ β ≡ β |
| 104 | +⊕-oz-left _ = refl |
0 commit comments