Add ψ≤Ω comparison branch and Ω-index bridge lemmas

Author: hyperpolymath

proofs/agda/Ordinal/Buchholz/Order.agda

@@ -17,7 +17,7 @@
 --   bzero                 │   –   │   ✓    │   ✓   │  ✓
 --   bOmega                │       │   ✓    │       │  ✓ (when μ <Ω ν)
 --   bplus                 │       │        │   ✓   │
---   bpsi                  │       │        │       │  ✓ (when μ <Ω ν)
+--   bpsi                  │       │   ✓    │       │  ✓ (when μ <Ω ν)
 --
 -- Open cases (no constructor yet; must be discharged in follow-ups
 -- before `<ᵇ`-totality and well-foundedness can land):
@@ -26,9 +26,6 @@
 --     between atomic heads and additive normal forms.
 --   * bpsi vs bplus (either direction) — same reason, mediated by
 --     the leading bpsi summand of a bplus in CNF.
---   * bpsi vs bOmega with ν ≤Ω μ — the admissibility condition makes
---     bpsi ν α ≤ᵇ bOmega μ when μ exceeds ν; the exact form is part
---     of the Buchholz 1986 comparison and is deferred.
 --   * Two same-binder sub-cases whose natural shapes run into Agda
 --     2.6.3's `--without-K` restriction on reflexive-equation
 --     elimination and are deferred pending a K-free reformulation:
@@ -43,7 +40,17 @@ module Ordinal.Buchholz.Order where
 
 open import Data.Empty using (⊥)
 
-open import Ordinal.OmegaMarkers using (OmegaIndex; _<Ω_; <Ω-irrefl; <Ω-trans)
+open import Ordinal.OmegaMarkers using
+  ( OmegaIndex
+  ; _≤Ω_
+  ; _<Ω_
+  ; <Ω-irrefl
+  ; <Ω-trans
+  ; <Ω→≤Ω
+  ; ≤Ω-trans
+  ; ≤Ω-<Ω-trans
+  ; <Ω-≤Ω-trans
+  )
 open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
 
 data _<ᵇ_ : BT → BT → Set where
@@ -63,6 +70,7 @@ data _<ᵇ_ : BT → BT → Set where
   -- bpsi comparison by Ω-index only. The same-index sub-case (lex on
   -- the ψ-argument) is deferred pending a K-free formulation.
   <ᵇ-ψΩ  : ∀ {μ ν α β} → μ <Ω ν → bpsi μ α <ᵇ bpsi ν β
+  <ᵇ-ψΩ≤ : ∀ {ν μ α}   → ν ≤Ω μ → bpsi ν α <ᵇ bOmega μ
 
   -- bplus comparison by the left summand. The same-left sub-case
   -- (compare right summands when lefts agree) is deferred for the
@@ -112,8 +120,15 @@ infix 4 _<ᵇ_
 <ᵇ-trans (<ᵇ-Ωψ p)    (<ᵇ-ψΩ q)            = <ᵇ-Ωψ (<Ω-trans p q)
 -- Left leg: <ᵇ-ψΩ (x = bpsi _ _, y = bpsi _ _)
 <ᵇ-trans (<ᵇ-ψΩ p)    (<ᵇ-ψΩ q)            = <ᵇ-ψΩ (<Ω-trans p q)
+<ᵇ-trans (<ᵇ-ψΩ p)    (<ᵇ-ψΩ≤ q)           = <ᵇ-ψΩ≤ (≤Ω-trans (<Ω→≤Ω p) q)
+-- Left leg: <ᵇ-ψΩ≤ (x = bpsi _ _, y = bOmega _)
+<ᵇ-trans (<ᵇ-ψΩ≤ p)   (<ᵇ-ΩΩ q)            = <ᵇ-ψΩ≤ (≤Ω-trans p (<Ω→≤Ω q))
+<ᵇ-trans (<ᵇ-ψΩ≤ p)   (<ᵇ-Ωψ q)            = <ᵇ-ψΩ (≤Ω-<Ω-trans p q)
 -- Left leg: <ᵇ-+1 (x = bplus _ _, y = bplus _ _)
 <ᵇ-trans (<ᵇ-+1 p)    (<ᵇ-+1 q)            = <ᵇ-+1 (<ᵇ-trans p q)
+-- Right leg: <ᵇ-ψΩ≤ (y = bpsi _ _, z = bOmega _)
+<ᵇ-trans <ᵇ-0-ψ       (<ᵇ-ψΩ≤ _)           = <ᵇ-0-Ω
+<ᵇ-trans (<ᵇ-Ωψ p)    (<ᵇ-ψΩ≤ q)           = <ᵇ-ΩΩ (<Ω-≤Ω-trans p q)
 
 ----------------------------------------------------------------------------
 -- WF-2 open-case inversions (Ω vs +)

proofs/agda/Ordinal/Buchholz/WellFounded.agda

@@ -8,16 +8,21 @@ module Ordinal.Buchholz.WellFounded where
 open import Data.Empty using (⊥; ⊥-elim)
 open import Data.Nat.Base using (ℕ; _<_)
 open import Data.Nat.Induction as NatInd using (<-wellFounded)
+open import Data.Product.Base using (_×_; _,_; proj₁; proj₂)
+open import Data.Sum.Base using (inj₁; inj₂)
 open import Relation.Nullary using (¬_)
+open import Relation.Binary.PropositionalEquality using (refl)
 open import Induction.WellFounded using (Acc; acc; WellFounded; wf⇒asym)
 
 open import Ordinal.OmegaMarkers using
   ( OmegaIndex
+  ; _≤Ω_
   ; fin
   ; ω
   ; _<Ω_
   ; fin<fin
   ; fin<ω
+  ; ≤Ω-split
   )
 open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
 open import Ordinal.Buchholz.Order using
@@ -28,6 +33,7 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ΩΩ
   ; <ᵇ-Ωψ
   ; <ᵇ-ψΩ
+  ; <ᵇ-ψΩ≤
   ; <ᵇ-+1
   )
 
@@ -52,44 +58,47 @@ open import Ordinal.Buchholz.Order using
 <ᵇ-acc-bzero : Acc _<ᵇ_ bzero
 <ᵇ-acc-bzero = acc <ᵇ-pred-bzero
 
-mutual
+ΩBundle : OmegaIndex → Set
+ΩBundle μ = Acc _<ᵇ_ (bOmega μ) × ((α : BT) → Acc _<ᵇ_ (bpsi μ α))
 
-  <ᵇ-pred-bOmega-fromΩ : ∀ {μ x} → Acc _<Ω_ μ → x <ᵇ bOmega μ → Acc _<ᵇ_ x
-  <ᵇ-pred-bOmega-fromΩ _              <ᵇ-0-Ω         = <ᵇ-acc-bzero
-  <ᵇ-pred-bOmega-fromΩ (acc rsμ)      (<ᵇ-ΩΩ κ<μ)    = <ᵇ-acc-bOmega-fromΩ (rsμ κ<μ)
+<ᵇ-bundle-fromΩ : ∀ {μ} → Acc _<Ω_ μ → ΩBundle μ
+<ᵇ-bundle-fromΩ {μ} aμ@(acc rsμ) = omegaAcc , psiAcc
+  where
+  mutual
 
-  <ᵇ-acc-bOmega-fromΩ : ∀ {μ} → Acc _<Ω_ μ → Acc _<ᵇ_ (bOmega μ)
-  <ᵇ-acc-bOmega-fromΩ aμ = acc (<ᵇ-pred-bOmega-fromΩ aμ)
+    omegaAcc : Acc _<ᵇ_ (bOmega μ)
+    omegaAcc = acc predOmega
 
-mutual
+    predOmega : ∀ {x} → x <ᵇ bOmega μ → Acc _<ᵇ_ x
+    predOmega <ᵇ-0-Ω = <ᵇ-acc-bzero
+    predOmega (<ᵇ-ΩΩ κ<μ) = proj₁ (<ᵇ-bundle-fromΩ (rsμ κ<μ))
+    predOmega (<ᵇ-ψΩ≤ {α = α} ν≤μ) with ≤Ω-split ν≤μ
+    ... | inj₁ ν<μ = proj₂ (<ᵇ-bundle-fromΩ (rsμ ν<μ)) α
+    ... | inj₂ refl = psiAcc α
 
-  <ᵇ-pred-bplus-from : ∀ {α β x} → Acc _<ᵇ_ α → x <ᵇ bplus α β → Acc _<ᵇ_ x
-  <ᵇ-pred-bplus-from _               <ᵇ-0-+                    = <ᵇ-acc-bzero
-  <ᵇ-pred-bplus-from (acc rsα)       (<ᵇ-+1 {x₂ = x₂} x₁<α)    = <ᵇ-acc-bplus-from (rsα x₁<α) x₂
-
-  <ᵇ-acc-bplus-from : ∀ {α} → Acc _<ᵇ_ α → (β : BT) → Acc _<ᵇ_ (bplus α β)
-  <ᵇ-acc-bplus-from aα β = acc (<ᵇ-pred-bplus-from aα)
+    psiAcc : (α : BT) → Acc _<ᵇ_ (bpsi μ α)
+    psiAcc α = acc λ where
+      <ᵇ-0-ψ               → <ᵇ-acc-bzero
+      (<ᵇ-Ωψ κ<μ)          → proj₁ (<ᵇ-bundle-fromΩ (rsμ κ<μ))
+      (<ᵇ-ψΩ {α = β} κ<μ)  → proj₂ (<ᵇ-bundle-fromΩ (rsμ κ<μ)) β
 
 mutual
 
-  <ᵇ-pred-bpsi-fromΩ : ∀ {μ α x} → Acc _<Ω_ μ → x <ᵇ bpsi μ α → Acc _<ᵇ_ x
-  <ᵇ-pred-bpsi-fromΩ _              <ᵇ-0-ψ                 = <ᵇ-acc-bzero
-  <ᵇ-pred-bpsi-fromΩ (acc rsμ)      (<ᵇ-Ωψ κ<μ)            = <ᵇ-acc-bOmega-fromΩ (rsμ κ<μ)
-  <ᵇ-pred-bpsi-fromΩ (acc rsμ)      (<ᵇ-ψΩ {α = β} κ<μ)    = <ᵇ-acc-bpsi-fromΩ (rsμ κ<μ) β
-
-  <ᵇ-acc-bpsi-fromΩ : ∀ {μ} → Acc _<Ω_ μ → (α : BT) → Acc _<ᵇ_ (bpsi μ α)
-  <ᵇ-acc-bpsi-fromΩ aμ α = acc (<ᵇ-pred-bpsi-fromΩ aμ)
+  <ᵇ-acc-bOmega : (μ : OmegaIndex) → Acc _<ᵇ_ (bOmega μ)
+  <ᵇ-acc-bOmega μ = proj₁ (<ᵇ-bundle-fromΩ (<Ω-wf μ))
 
-mutual
+  <ᵇ-pred-bplus-from : ∀ {α β x} → Acc _<ᵇ_ α → x <ᵇ bplus α β → Acc _<ᵇ_ x
+  <ᵇ-pred-bplus-from _          <ᵇ-0-+                  = <ᵇ-acc-bzero
+  <ᵇ-pred-bplus-from (acc rsα)  (<ᵇ-+1 {x₂ = x₂} x₁<α)  = <ᵇ-acc-bplus-from (rsα x₁<α) x₂
 
-  <ᵇ-acc-bOmega : (μ : OmegaIndex) → Acc _<ᵇ_ (bOmega μ)
-  <ᵇ-acc-bOmega μ = <ᵇ-acc-bOmega-fromΩ (<Ω-wf μ)
+  <ᵇ-acc-bplus-from : ∀ {α} → Acc _<ᵇ_ α → (β : BT) → Acc _<ᵇ_ (bplus α β)
+  <ᵇ-acc-bplus-from aα β = acc (<ᵇ-pred-bplus-from aα)
 
   <ᵇ-acc-bplus : (α β : BT) → Acc _<ᵇ_ (bplus α β)
   <ᵇ-acc-bplus α β = <ᵇ-acc-bplus-from (wf-<ᵇ α) β
 
   <ᵇ-acc-bpsi : (μ : OmegaIndex) (α : BT) → Acc _<ᵇ_ (bpsi μ α)
-  <ᵇ-acc-bpsi μ α = <ᵇ-acc-bpsi-fromΩ (<Ω-wf μ) α
+  <ᵇ-acc-bpsi μ α = proj₂ (<ᵇ-bundle-fromΩ (<Ω-wf μ)) α
 
   wf-<ᵇ : WellFounded _<ᵇ_
   wf-<ᵇ bzero       = <ᵇ-acc-bzero

proofs/agda/Ordinal/OmegaMarkers.agda

@@ -10,7 +10,16 @@ module Ordinal.OmegaMarkers where
 
 open import Data.Empty using (⊥)
 open import Data.Nat.Base using (ℕ; _≤_; _<_; z≤n; s≤s; zero; suc)
-open import Data.Nat.Properties using (≤-refl; ≤-trans; <-irrefl; <-trans)
+open import Data.Sum.Base using (_⊎_; inj₁; inj₂)
+open import Data.Nat.Properties using
+  ( ≤-refl
+  ; ≤-trans
+  ; <-irrefl
+  ; <-trans
+  ; ≤-<-trans
+  ; <-≤-trans
+  ; m≤n⇒m<n∨m≡n
+  )
 open import Relation.Binary.PropositionalEquality using (_≡_; refl)
 
 data OmegaIndex : Set where
@@ -66,6 +75,26 @@ infix 4 _<Ω_
     <→≤ (s≤s (s≤s m<n)) = s≤s (<→≤ (s≤s m<n))
 <Ω→≤Ω fin<ω = fin≤ω
 
+-- Mixed transitivity lemmas used by Buchholz order composition.
+
+≤Ω-<Ω-trans : ∀ {α β γ} → α ≤Ω β → β <Ω γ → α <Ω γ
+≤Ω-<Ω-trans (fin≤fin m≤n) (fin<fin n<k) = fin<fin (≤-<-trans m≤n n<k)
+≤Ω-<Ω-trans (fin≤fin _)   fin<ω         = fin<ω
+≤Ω-<Ω-trans fin≤ω         ()
+≤Ω-<Ω-trans ω≤ω           ()
+
+<Ω-≤Ω-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<ω
+
+≤Ω-split : ∀ {ν μ} → ν ≤Ω μ → ν <Ω μ ⊎ ν ≡ μ
+≤Ω-split (fin≤fin m≤n) with m≤n⇒m<n∨m≡n m≤n
+... | inj₁ m<n = inj₁ (fin<fin m<n)
+... | inj₂ refl = inj₂ refl
+≤Ω-split fin≤ω = inj₁ fin<ω
+≤Ω-split ω≤ω   = inj₂ refl
+
 Omega0 : OmegaIndex
 Omega0 = fin zero
 

proofs/agda/Smoke.agda

@@ -178,6 +178,7 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ΩΩ
   ; <ᵇ-Ωψ
   ; <ᵇ-ψΩ
+  ; <ᵇ-ψΩ≤
   ; <ᵇ-+1
   ; <ᵇ-irrefl
   ; <ᵇ-trans