E5: make ν operational and add Buchholz example/smoke modules

proofs/agda/All.agda

@@ -28,5 +28,7 @@ open import Ordinal.OmegaMarkers
 open import Ordinal.Buchholz.Syntax
 open import Ordinal.Buchholz.Closure
 open import Ordinal.Buchholz.Psi
+open import Ordinal.Buchholz.Examples
+open import Ordinal.Buchholz.Smoke
 
 open import Smoke

proofs/agda/Ordinal/Buchholz/Closure.agda

@@ -12,19 +12,19 @@ module Ordinal.Buchholz.Closure where
 open import Data.Nat.Base using (ℕ; _≤_; _<_)
 open import Data.Nat.Properties using (≤-trans)
 
-open import Ordinal.OmegaMarkers using (OmegaIndex)
+open import Ordinal.OmegaMarkers using (OmegaIndex; _≤Ω_)
 open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
 
 data Cν (ν : OmegaIndex) : ℕ → BT → Set where
   cν-zero  : ∀ {m} → Cν ν m bzero
-  cν-omega : ∀ {m μ} → Cν ν m (bOmega μ)
+  cν-omega : ∀ {m μ} → μ ≤Ω ν → Cν ν m (bOmega μ)
   cν-plus  : ∀ {m x y} → Cν ν m x → Cν ν m y → Cν ν m (bplus x y)
-  cν-psi   : ∀ {m k μ β} → k < m → Cν ν k β → Cν ν m (bpsi μ β)
+  cν-psi   : ∀ {m k μ β} → μ ≤Ω ν → k < m → Cν ν k β → Cν ν m (bpsi μ β)
 
 -- Headline E5 structural lemma: raising the stage keeps derivability.
 
 Cν-monotone : ∀ {ν m n t} → m ≤ n → Cν ν m t → Cν ν n t
 Cν-monotone _   cν-zero          = cν-zero
-Cν-monotone _   cν-omega         = cν-omega
+Cν-monotone _   (cν-omega μ≤ν)   = cν-omega μ≤ν
 Cν-monotone m≤n (cν-plus cx cy)  = cν-plus (Cν-monotone m≤n cx) (Cν-monotone m≤n cy)
-Cν-monotone m≤n (cν-psi k<m ck)  = cν-psi (≤-trans k<m m≤n) ck
+Cν-monotone m≤n (cν-psi μ≤ν k<m ck) = cν-psi μ≤ν (≤-trans k<m m≤n) ck

proofs/agda/Ordinal/Buchholz/Examples.agda

@@ -0,0 +1,35 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Stage S1/S2 scaffolding for docs/buchholz-plan.adoc.
+--
+-- Small concrete Buchholz terms and closure witnesses used as smoke
+-- examples while the full ordering/normal-form development is pending.
+
+module Ordinal.Buchholz.Examples where
+
+open import Data.Nat.Base using (z≤n; s≤s)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Nullary using (¬_)
+
+open import Ordinal.OmegaMarkers using (Omega0; Omega1; Omegaω; fin≤ω)
+open import Ordinal.Buchholz.Syntax using (BT; bOmega; bpsi; psi0)
+open import Ordinal.Buchholz.Closure using (Cν; cν-omega; cν-psi)
+open import Ordinal.Buchholz.Psi using (psiν-notin-Cν)
+
+bh-psi0-omega1 : BT
+bh-psi0-omega1 = bpsi Omega0 (bOmega Omega1)
+
+bh-psi0-omegaω : BT
+bh-psi0-omegaω = bpsi Omega0 (bOmega Omegaω)
+
+psi0-expands : psi0 (bOmega Omega1) ≡ bh-psi0-omega1
+psi0-expands = refl
+
+omega1-in-Cω-at-0 : Cν Omegaω 0 (bOmega Omega1)
+omega1-in-Cω-at-0 = cν-omega fin≤ω
+
+psi0-omega1-at-1 : Cν Omegaω 1 bh-psi0-omega1
+psi0-omega1-at-1 = cν-psi fin≤ω (s≤s z≤n) omega1-in-Cω-at-0
+
+psi0-omega1-not-at-0 : ¬ Cν Omegaω 0 bh-psi0-omega1
+psi0-omega1-not-at-0 = psiν-notin-Cν

proofs/agda/Ordinal/Buchholz/Psi.agda

@@ -17,9 +17,9 @@ open import Ordinal.Buchholz.Syntax using (BT; bpsi)
 open import Ordinal.Buchholz.Closure using (Cν; cν-psi)
 
 psiν-notin-Cν : ∀ {ν μ β} → ¬ Cν ν 0 (bpsi μ β)
-psiν-notin-Cν (cν-psi () _)
+psiν-notin-Cν (cν-psi _ () _)
 
 -- Useful companion: any derivation of `ψ_μ β` lives at stage at least 1.
 
 psiν-stage-lb : ∀ {ν μ β m} → Cν ν m (bpsi μ β) → 1 ≤ m
-psiν-stage-lb (cν-psi k<m _) = ≤-trans (s≤s z≤n) k<m
+psiν-stage-lb (cν-psi _ k<m _) = ≤-trans (s≤s z≤n) k<m

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -0,0 +1,53 @@
+{-# OPTIONS --safe --without-K #-}
+
+-- Buchholz-layer manifest. Keeps load-bearing names pinned so that
+-- accidental renames fail quickly in a focused module.
+
+module Ordinal.Buchholz.Smoke where
+
+open import Ordinal.OmegaMarkers using
+  ( OmegaIndex
+  ; fin
+  ; ω
+  ; _≤Ω_
+  ; fin≤fin
+  ; fin≤ω
+  ; ω≤ω
+  ; ≤Ω-refl
+  ; ≤Ω-trans
+  ; Omega0
+  ; Omega1
+  ; Omegaω
+  )
+
+open import Ordinal.Buchholz.Syntax using
+  ( BT
+  ; bzero
+  ; bOmega
+  ; bplus
+  ; bpsi
+  ; psi0
+  )
+
+open import Ordinal.Buchholz.Closure using
+  ( Cν
+  ; cν-zero
+  ; cν-omega
+  ; cν-plus
+  ; cν-psi
+  ; Cν-monotone
+  )
+
+open import Ordinal.Buchholz.Psi using
+  ( psiν-notin-Cν
+  ; psiν-stage-lb
+  )
+
+open import Ordinal.Buchholz.Examples using
+  ( bh-psi0-omega1
+  ; bh-psi0-omegaω
+  ; psi0-expands
+  ; omega1-in-Cω-at-0
+  ; psi0-omega1-at-1
+  ; psi0-omega1-not-at-0
+  )

proofs/agda/Ordinal/OmegaMarkers.agda

@@ -8,12 +8,34 @@
 
 module Ordinal.OmegaMarkers where
 
-open import Data.Nat.Base using (ℕ; zero; suc)
+open import Data.Nat.Base using (ℕ; _≤_; zero; suc)
+open import Data.Nat.Properties using (≤-refl; ≤-trans)
 
 data OmegaIndex : Set where
   fin : ℕ → OmegaIndex
   ω   : OmegaIndex
 
+-- Structural preorder on Ω-markers used as side conditions in Buchholz
+-- closure rules: finite indices compare by `ℕ` order, every finite
+-- index is below `ω`, and `ω` is only below itself.
+
+data _≤Ω_ : OmegaIndex → OmegaIndex → Set where
+  fin≤fin : ∀ {m n} → m ≤ n → fin m ≤Ω fin n
+  fin≤ω   : ∀ {m}   → fin m ≤Ω ω
+  ω≤ω     : ω ≤Ω ω
+
+infix 4 _≤Ω_
+
+≤Ω-refl : ∀ {ν} → ν ≤Ω ν
+≤Ω-refl {fin n} = fin≤fin ≤-refl
+≤Ω-refl {ω}     = ω≤ω
+
+≤Ω-trans : ∀ {α β γ} → α ≤Ω β → β ≤Ω γ → α ≤Ω γ
+≤Ω-trans (fin≤fin m≤n) (fin≤fin n≤k) = fin≤fin (≤-trans m≤n n≤k)
+≤Ω-trans (fin≤fin _)   fin≤ω         = fin≤ω
+≤Ω-trans fin≤ω         ω≤ω           = fin≤ω
+≤Ω-trans ω≤ω           ω≤ω           = ω≤ω
+
 Omega0 : OmegaIndex
 Omega0 = fin zero
 

proofs/agda/Smoke.agda

@@ -102,6 +102,12 @@ open import Ordinal.OmegaMarkers using
   ( OmegaIndex
   ; fin
   ; ω
+  ; _≤Ω_
+  ; fin≤fin
+  ; fin≤ω
+  ; ω≤ω
+  ; ≤Ω-refl
+  ; ≤Ω-trans
   ; Omega0
   ; Omega1
   ; Omegaω
@@ -128,3 +134,14 @@ open import Ordinal.Buchholz.Closure using
 open import Ordinal.Buchholz.Psi using
   ( psiν-notin-Cν
   )
+
+open import Ordinal.Buchholz.Examples using
+  ( bh-psi0-omega1
+  ; bh-psi0-omegaω
+  ; psi0-expands
+  ; omega1-in-Cω-at-0
+  ; psi0-omega1-at-1
+  ; psi0-omega1-not-at-0
+  )
+
+open import Ordinal.Buchholz.Smoke using ()