|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Stage WF-0 of the Buchholz well-foundedness workstream |
| 4 | +-- (docs/buchholz-plan.adoc, follow-up to E5–E7). |
| 5 | +-- |
| 6 | +-- Defines the binary strict order `_<ᵇ_` on Buchholz terms (BT) and |
| 7 | +-- establishes irreflexivity and transitivity across the cases that |
| 8 | +-- the term heads naturally determine. Totality is *not* proved here |
| 9 | +-- and neither is well-foundedness; those are WF-1 and WF-2. |
| 10 | +-- |
| 11 | +-- Scope of this module. The 7 constructors below cover the head |
| 12 | +-- pairs marked ✓ in the matrix, with the lex-on-left-summand case |
| 13 | +-- for bplus and the lex-on-Ω-index case for bpsi: |
| 14 | +-- |
| 15 | +-- head of x \ head of y │ bzero │ bOmega │ bplus │ bpsi |
| 16 | +-- ──────────────────────┼───────┼────────┼───────┼────── |
| 17 | +-- bzero │ – │ ✓ │ ✓ │ ✓ |
| 18 | +-- bOmega │ │ ✓ │ │ ✓ (when μ <Ω ν) |
| 19 | +-- bplus │ │ │ ✓ │ |
| 20 | +-- bpsi │ │ │ │ ✓ (when μ <Ω ν) |
| 21 | +-- |
| 22 | +-- Open cases (no constructor yet; must be discharged in follow-ups |
| 23 | +-- before `<ᵇ`-totality and well-foundedness can land): |
| 24 | +-- |
| 25 | +-- * bOmega vs bplus (either direction) — requires a comparison |
| 26 | +-- between atomic heads and additive normal forms. |
| 27 | +-- * bpsi vs bplus (either direction) — same reason, mediated by |
| 28 | +-- the leading bpsi summand of a bplus in CNF. |
| 29 | +-- * bpsi vs bOmega with ν ≤Ω μ — the admissibility condition makes |
| 30 | +-- bpsi ν α ≤ᵇ bOmega μ when μ exceeds ν; the exact form is part |
| 31 | +-- of the Buchholz 1986 comparison and is deferred. |
| 32 | +-- * Two same-binder sub-cases whose natural shapes run into Agda |
| 33 | +-- 2.6.3's `--without-K` restriction on reflexive-equation |
| 34 | +-- elimination and are deferred pending a K-free reformulation: |
| 35 | +-- - bpsi ν α <ᵇ bpsi ν β with α <ᵇ β (same Ω-index ν). |
| 36 | +-- - bplus x y₂ <ᵇ bplus x z₂ with y₂ <ᵇ z₂ (same left summand). |
| 37 | +-- In both cases the constructor shares a binder between the two |
| 38 | +-- sides of `<ᵇ`, which `<ᵇ-irrefl`'s pattern unification cannot |
| 39 | +-- reduce. A rank-embedding or heterogeneous-equality formulation |
| 40 | +-- is the next follow-up on top of WF-0. |
| 41 | + |
| 42 | +module Ordinal.Buchholz.Order where |
| 43 | + |
| 44 | +open import Data.Empty using (⊥) |
| 45 | + |
| 46 | +open import Ordinal.OmegaMarkers using (OmegaIndex; _<Ω_; <Ω-irrefl; <Ω-trans) |
| 47 | +open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi) |
| 48 | + |
| 49 | +data _<ᵇ_ : BT → BT → Set where |
| 50 | + -- bzero is minimum against every non-bzero head. |
| 51 | + <ᵇ-0-Ω : ∀ {μ} → bzero <ᵇ bOmega μ |
| 52 | + <ᵇ-0-+ : ∀ {x y} → bzero <ᵇ bplus x y |
| 53 | + <ᵇ-0-ψ : ∀ {ν α} → bzero <ᵇ bpsi ν α |
| 54 | + |
| 55 | + -- bOmega ordering by Ω-index. |
| 56 | + <ᵇ-ΩΩ : ∀ {μ ν} → μ <Ω ν → bOmega μ <ᵇ bOmega ν |
| 57 | + |
| 58 | + -- Ω_μ < ψ_ν(α) whenever μ <Ω ν. This is the admissibility side: |
| 59 | + -- ψ-terms at higher index dominate Ω-markers at lower index. The |
| 60 | + -- reverse direction (bpsi ν α <ᵇ bOmega μ with ν ≤Ω μ) is deferred. |
| 61 | + <ᵇ-Ωψ : ∀ {μ ν α} → μ <Ω ν → bOmega μ <ᵇ bpsi ν α |
| 62 | + |
| 63 | + -- bpsi comparison by Ω-index only. The same-index sub-case (lex on |
| 64 | + -- the ψ-argument) is deferred pending a K-free formulation. |
| 65 | + <ᵇ-ψΩ : ∀ {μ ν α β} → μ <Ω ν → bpsi μ α <ᵇ bpsi ν β |
| 66 | + |
| 67 | + -- bplus comparison by the left summand. The same-left sub-case |
| 68 | + -- (compare right summands when lefts agree) is deferred for the |
| 69 | + -- same `--without-K` reason as `<ᵇ-ψα` above: its natural shape |
| 70 | + -- `bplus x y₂ <ᵇ bplus x z₂` shares the binder `x` on both sides. |
| 71 | + <ᵇ-+1 : ∀ {x₁ x₂ y₁ y₂} → x₁ <ᵇ y₁ → bplus x₁ x₂ <ᵇ bplus y₁ y₂ |
| 72 | + |
| 73 | +infix 4 _<ᵇ_ |
| 74 | + |
| 75 | +---------------------------------------------------------------------------- |
| 76 | +-- Irreflexivity |
| 77 | +---------------------------------------------------------------------------- |
| 78 | + |
| 79 | +-- Every constructor of `_<ᵇ_` with equal LHS and RHS reduces to a |
| 80 | +-- witness of irreflexivity at a strictly smaller structure (either |
| 81 | +-- `_<Ω_` or `_<ᵇ_` on a subterm). Explicit binds on the `{x}` ensure |
| 82 | +-- the K-free unifier does not get stuck on reflexive equations at the |
| 83 | +-- shared Ω-index of `<ᵇ-ψα`. |
| 84 | + |
| 85 | +<ᵇ-irrefl : ∀ {x} → x <ᵇ x → ⊥ |
| 86 | +<ᵇ-irrefl (<ᵇ-ΩΩ μ<μ) = <Ω-irrefl μ<μ |
| 87 | +<ᵇ-irrefl (<ᵇ-ψΩ μ<μ) = <Ω-irrefl μ<μ |
| 88 | +<ᵇ-irrefl (<ᵇ-+1 x<x) = <ᵇ-irrefl x<x |
| 89 | + |
| 90 | +---------------------------------------------------------------------------- |
| 91 | +-- Transitivity |
| 92 | +---------------------------------------------------------------------------- |
| 93 | + |
| 94 | +-- Case analysis on the two ordering derivations, recursing on |
| 95 | +-- `_<Ω_` or `_<ᵇ_` subterms as needed. Covers every pair of |
| 96 | +-- constructors whose middle term has a compatible head; pairs with |
| 97 | +-- incompatible middle heads are absurd by construction (no |
| 98 | +-- constructor witnesses them). |
| 99 | + |
| 100 | +<ᵇ-trans : ∀ {x y z} → x <ᵇ y → y <ᵇ z → x <ᵇ z |
| 101 | +-- Left leg: <ᵇ-0-Ω (x = bzero, y = bOmega _) |
| 102 | +<ᵇ-trans <ᵇ-0-Ω (<ᵇ-ΩΩ _) = <ᵇ-0-Ω |
| 103 | +<ᵇ-trans <ᵇ-0-Ω (<ᵇ-Ωψ _) = <ᵇ-0-ψ |
| 104 | +-- Left leg: <ᵇ-0-+ (x = bzero, y = bplus _ _) |
| 105 | +<ᵇ-trans <ᵇ-0-+ (<ᵇ-+1 _) = <ᵇ-0-+ |
| 106 | +-- Left leg: <ᵇ-0-ψ (x = bzero, y = bpsi _ _) |
| 107 | +<ᵇ-trans <ᵇ-0-ψ (<ᵇ-ψΩ _) = <ᵇ-0-ψ |
| 108 | +-- Left leg: <ᵇ-ΩΩ (x = bOmega _, y = bOmega _) |
| 109 | +<ᵇ-trans (<ᵇ-ΩΩ p) (<ᵇ-ΩΩ q) = <ᵇ-ΩΩ (<Ω-trans p q) |
| 110 | +<ᵇ-trans (<ᵇ-ΩΩ p) (<ᵇ-Ωψ q) = <ᵇ-Ωψ (<Ω-trans p q) |
| 111 | +-- Left leg: <ᵇ-Ωψ (x = bOmega _, y = bpsi _ _) |
| 112 | +<ᵇ-trans (<ᵇ-Ωψ p) (<ᵇ-ψΩ q) = <ᵇ-Ωψ (<Ω-trans p q) |
| 113 | +-- Left leg: <ᵇ-ψΩ (x = bpsi _ _, y = bpsi _ _) |
| 114 | +<ᵇ-trans (<ᵇ-ψΩ p) (<ᵇ-ψΩ q) = <ᵇ-ψΩ (<Ω-trans p q) |
| 115 | +-- Left leg: <ᵇ-+1 (x = bplus _ _, y = bplus _ _) |
| 116 | +<ᵇ-trans (<ᵇ-+1 p) (<ᵇ-+1 q) = <ᵇ-+1 (<ᵇ-trans p q) |
| 117 | + |
| 118 | +---------------------------------------------------------------------------- |
| 119 | +-- Strict-below-ψ examples, for downstream ordering checks |
| 120 | +---------------------------------------------------------------------------- |
| 121 | + |
| 122 | +-- These use the pinned `Omega*` constants from OmegaMarkers to keep |
| 123 | +-- the Buchholz example terms in a strict chain: bzero <ᵇ Ω₀ <ᵇ Ω₁ |
| 124 | +-- <ᵇ Ω_ω <ᵇ ψ_ω(bzero). The last strict inequality uses the cross- |
| 125 | +-- constructor <ᵇ-Ωψ since ω <Ω ω is absent (ω is top). |
| 126 | + |
| 127 | +open import Ordinal.OmegaMarkers using |
| 128 | + ( Omega0 |
| 129 | + ; Omega1 |
| 130 | + ; Omegaω |
| 131 | + ; Omega0<Omega1 |
| 132 | + ; Omega0<Omegaω |
| 133 | + ; Omega1<Omegaω |
| 134 | + ) |
| 135 | + |
| 136 | +bzero<Ω0 : bzero <ᵇ bOmega Omega0 |
| 137 | +bzero<Ω0 = <ᵇ-0-Ω |
| 138 | + |
| 139 | +Ω0<Ω1 : bOmega Omega0 <ᵇ bOmega Omega1 |
| 140 | +Ω0<Ω1 = <ᵇ-ΩΩ Omega0<Omega1 |
| 141 | + |
| 142 | +Ω1<Ωω : bOmega Omega1 <ᵇ bOmega Omegaω |
| 143 | +Ω1<Ωω = <ᵇ-ΩΩ Omega1<Omegaω |
| 144 | + |
| 145 | +Ω0<ψ1-zero : bOmega Omega0 <ᵇ bpsi Omega1 bzero |
| 146 | +Ω0<ψ1-zero = <ᵇ-Ωψ Omega0<Omega1 |
0 commit comments