|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Stage S0 / Milestone E3 of docs/buchholz-plan.adoc. |
| 4 | +-- |
| 5 | +-- Cantor normal form fragment below ε₀, as pure syntax. |
| 6 | +-- |
| 7 | +-- `CNF` is a nested list: `czero` is the ordinal 0, and `α ∷ r` is |
| 8 | +-- `ω^α + r` with the exponent `α` itself a CNF term. We do *not* yet |
| 9 | +-- impose the weak-descending well-formedness predicate; that is a |
| 10 | +-- downstream normalisation step. The trichotomy theorem only needs |
| 11 | +-- the structural lexicographic order on raw CNF trees, which is the |
| 12 | +-- backbone of every later CNF ordering argument. |
| 13 | +-- |
| 14 | +-- Headline lemma: `cnf-trichotomy` — for any two CNF terms α, β, |
| 15 | +-- exactly one of α <ᶜ β, α ≡ β, β <ᶜ α holds (this module gives the |
| 16 | +-- inclusive form; uniqueness follows from `<ᶜ-irrefl`). |
| 17 | + |
| 18 | +module Ordinal.CNF where |
| 19 | + |
| 20 | +open import Data.Sum.Base using (_⊎_; inj₁; inj₂) |
| 21 | +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂) |
| 22 | +open import Relation.Nullary using (¬_) |
| 23 | + |
| 24 | +-- Syntax. Read `α ∷ r` as the formal sum ω^α + r. |
| 25 | + |
| 26 | +data CNF : Set where |
| 27 | + czero : CNF |
| 28 | + _∷_ : CNF → CNF → CNF |
| 29 | + |
| 30 | +infixr 5 _∷_ |
| 31 | + |
| 32 | +-- Named atoms, used below to exercise the comparison. |
| 33 | + |
| 34 | +one : CNF |
| 35 | +one = czero ∷ czero -- ω^0 + 0 = 1 |
| 36 | + |
| 37 | +two : CNF |
| 38 | +two = czero ∷ (czero ∷ czero) -- ω^0 + ω^0 + 0 = 2 |
| 39 | + |
| 40 | +ω : CNF |
| 41 | +ω = (czero ∷ czero) ∷ czero -- ω^1 + 0 = ω |
| 42 | + |
| 43 | +-- Lexicographic strict order on CNF trees. |
| 44 | +-- |
| 45 | +-- Three rules: |
| 46 | +-- * `<-zero-cons` : 0 is below every non-zero term. |
| 47 | +-- * `<-head` : if heads differ, the head decides. |
| 48 | +-- * `<-tail` : if heads match, the tails decide. |
| 49 | + |
| 50 | +data _<ᶜ_ : CNF → CNF → Set where |
| 51 | + <-zero-cons : ∀ {α r} → czero <ᶜ (α ∷ r) |
| 52 | + <-head : ∀ {α β r s} → α <ᶜ β → (α ∷ r) <ᶜ (β ∷ s) |
| 53 | + <-tail : ∀ {α r s} → r <ᶜ s → (α ∷ r) <ᶜ (α ∷ s) |
| 54 | + |
| 55 | +infix 4 _<ᶜ_ |
| 56 | + |
| 57 | +-- Irreflexivity. No CNF term is strictly below itself. |
| 58 | +-- Note `czero <ᶜ czero` is not derivable: `<-zero-cons` requires a |
| 59 | +-- non-zero right-hand side, so the only cases are the two inductive |
| 60 | +-- ones, both of which recurse on a strictly smaller proof. |
| 61 | + |
| 62 | +data ConsStep (α r β s : CNF) : Set where |
| 63 | + step-head : α <ᶜ β → ConsStep α r β s |
| 64 | + step-tail : α ≡ β → r <ᶜ s → ConsStep α r β s |
| 65 | + |
| 66 | +cons-step : ∀ {α r β s} → (α ∷ r) <ᶜ (β ∷ s) → ConsStep α r β s |
| 67 | +cons-step (<-head α<β) = step-head α<β |
| 68 | +cons-step (<-tail {α = α} r<s) = step-tail refl r<s |
| 69 | + |
| 70 | +<ᶜ-irrefl : ∀ {α} → ¬ (α <ᶜ α) |
| 71 | +<ᶜ-irrefl {czero} () |
| 72 | +<ᶜ-irrefl {α ∷ r} p with cons-step p |
| 73 | +... | step-head α<α = <ᶜ-irrefl α<α |
| 74 | +... | step-tail _ r<r = <ᶜ-irrefl r<r |
| 75 | + |
| 76 | +-- Transitivity. |
| 77 | +-- |
| 78 | +-- Induction on the left derivation, then case-split on the right: |
| 79 | +-- every pairing is determined by the shapes of the two proofs. |
| 80 | + |
| 81 | +<ᶜ-trans : ∀ {α β γ} → α <ᶜ β → β <ᶜ γ → α <ᶜ γ |
| 82 | +<ᶜ-trans <-zero-cons (<-head _) = <-zero-cons |
| 83 | +<ᶜ-trans <-zero-cons (<-tail _) = <-zero-cons |
| 84 | +<ᶜ-trans (<-head a<b) (<-head b<c) = <-head (<ᶜ-trans a<b b<c) |
| 85 | +<ᶜ-trans (<-head a<b) (<-tail _) = <-head a<b |
| 86 | +<ᶜ-trans (<-tail r<s) (<-head a<b) = <-head a<b |
| 87 | +<ᶜ-trans (<-tail r<s) (<-tail s<t) = <-tail (<ᶜ-trans r<s s<t) |
| 88 | + |
| 89 | +-- Headline lemma: CNF trichotomy. |
| 90 | +-- |
| 91 | +-- Double induction on α and β. The `(a ∷ as) , (b ∷ bs)` case first |
| 92 | +-- compares the heads; on equality it recurses on the tails. Every |
| 93 | +-- branch lands in exactly one of the three disjuncts. |
| 94 | + |
| 95 | +cnf-trichotomy : ∀ (α β : CNF) → α <ᶜ β ⊎ α ≡ β ⊎ β <ᶜ α |
| 96 | +cnf-trichotomy czero czero = inj₂ (inj₁ refl) |
| 97 | +cnf-trichotomy czero (b ∷ bs) = inj₁ <-zero-cons |
| 98 | +cnf-trichotomy (a ∷ as) czero = inj₂ (inj₂ <-zero-cons) |
| 99 | +cnf-trichotomy (a ∷ as) (b ∷ bs) with cnf-trichotomy a b |
| 100 | +... | inj₁ a<b = inj₁ (<-head a<b) |
| 101 | +... | inj₂ (inj₂ b<a) = inj₂ (inj₂ (<-head b<a)) |
| 102 | +... | inj₂ (inj₁ refl) with cnf-trichotomy as bs |
| 103 | +... | inj₁ as<bs = inj₁ (<-tail as<bs) |
| 104 | +... | inj₂ (inj₁ refl) = inj₂ (inj₁ refl) |
| 105 | +... | inj₂ (inj₂ bs<as) = inj₂ (inj₂ (<-tail bs<as)) |
| 106 | + |
| 107 | +-- Worked witnesses, to exercise the comparison at small terms. |
| 108 | + |
| 109 | +one<ᶜtwo : one <ᶜ two |
| 110 | +one<ᶜtwo = <-tail <-zero-cons |
| 111 | + |
| 112 | +two<ᶜω : two <ᶜ ω |
| 113 | +two<ᶜω = <-head <-zero-cons |
| 114 | + |
| 115 | +one<ᶜω : one <ᶜ ω |
| 116 | +one<ᶜω = <ᶜ-trans one<ᶜtwo two<ᶜω |
0 commit comments