|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | + |
| 3 | +-- Veblen-route interface for Buchholz WF follow-up work. |
| 4 | +-- |
| 5 | +-- This module is intentionally small: it does not implement a concrete |
| 6 | +-- measure. Instead it states, in one place, the obligations required |
| 7 | +-- to prove `WellFounded _<ᵇ_` via a measure into a well-founded target. |
| 8 | +-- |
| 9 | +-- The final two fields (`dec-ψα`, `dec-+2`) are the deferred same-binder |
| 10 | +-- obligations corresponding to the blocked shared-binder shapes. |
| 11 | + |
| 12 | +module Ordinal.Buchholz.VeblenInterface where |
| 13 | + |
| 14 | +open import Agda.Primitive using (Level; lsuc; _⊔_) |
| 15 | +open import Function.Base using (_on_) |
| 16 | +open import Relation.Binary.Core using (Rel; _⇒_) |
| 17 | +open import Induction.WellFounded as WF using (WellFounded; module Subrelation) |
| 18 | +open import Relation.Binary.Construct.On as On using (wellFounded) |
| 19 | + |
| 20 | +open import Ordinal.OmegaMarkers using (OmegaIndex; _<Ω_; _≤Ω_; ω) |
| 21 | +open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi) |
| 22 | +open import Ordinal.Buchholz.Order using |
| 23 | + ( _<ᵇ_ |
| 24 | + ; <ᵇ-0-Ω |
| 25 | + ; <ᵇ-0-+ |
| 26 | + ; <ᵇ-0-ψ |
| 27 | + ; <ᵇ-ΩΩ |
| 28 | + ; <ᵇ-Ωψ |
| 29 | + ; <ᵇ-ψΩ |
| 30 | + ; <ᵇ-ψΩ≤ |
| 31 | + ; <ᵇ-+ω |
| 32 | + ; <ᵇ-+ψω |
| 33 | + ; <ᵇ-+1 |
| 34 | + ) |
| 35 | + |
| 36 | +record VeblenWFInterface {ℓm ℓr : Level} |
| 37 | + (M : Set ℓm) |
| 38 | + (_≺_ : Rel M ℓr) |
| 39 | + : Set (lsuc (ℓm ⊔ ℓr)) where |
| 40 | + field |
| 41 | + measure : BT → M |
| 42 | + ≺-wf : WellFounded _≺_ |
| 43 | + |
| 44 | + -- Constructor-by-constructor decrease obligations for the current core. |
| 45 | + dec-0-Ω : ∀ {μ} → measure bzero ≺ measure (bOmega μ) |
| 46 | + dec-0-+ : ∀ {x y} → measure bzero ≺ measure (bplus x y) |
| 47 | + dec-0-ψ : ∀ {ν α} → measure bzero ≺ measure (bpsi ν α) |
| 48 | + |
| 49 | + dec-ΩΩ : ∀ {μ ν} → μ <Ω ν → measure (bOmega μ) ≺ measure (bOmega ν) |
| 50 | + dec-Ωψ : ∀ {μ ν α} → μ <Ω ν → measure (bOmega μ) ≺ measure (bpsi ν α) |
| 51 | + dec-ψΩ : ∀ {μ ν α β} → μ <Ω ν → measure (bpsi μ α) ≺ measure (bpsi ν β) |
| 52 | + dec-ψΩ≤ : ∀ {ν μ α} → ν ≤Ω μ → measure (bpsi ν α) ≺ measure (bOmega μ) |
| 53 | + |
| 54 | + dec-+ω : ∀ {x y} → x <ᵇ bOmega ω → measure (bplus x y) ≺ measure (bOmega ω) |
| 55 | + dec-+ψω : ∀ {x y α} → x <ᵇ bpsi ω α → measure (bplus x y) ≺ measure (bpsi ω α) |
| 56 | + dec-+1 : ∀ {x₁ x₂ y₁ y₂} → x₁ <ᵇ y₁ → measure (bplus x₁ x₂) ≺ measure (bplus y₁ y₂) |
| 57 | + |
| 58 | + -- Deferred same-binder obligations for the extended comparison layer. |
| 59 | + dec-ψα : ∀ {ν α β} → α <ᵇ β → measure (bpsi ν α) ≺ measure (bpsi ν β) |
| 60 | + dec-+2 : ∀ {x y₂ z₂} → y₂ <ᵇ z₂ → measure (bplus x y₂) ≺ measure (bplus x z₂) |
| 61 | + |
| 62 | + core-monotone : _<ᵇ_ ⇒ (_≺_ on measure) |
| 63 | + core-monotone <ᵇ-0-Ω = dec-0-Ω |
| 64 | + core-monotone <ᵇ-0-+ = dec-0-+ |
| 65 | + core-monotone <ᵇ-0-ψ = dec-0-ψ |
| 66 | + core-monotone (<ᵇ-ΩΩ μ<ν) = dec-ΩΩ μ<ν |
| 67 | + core-monotone (<ᵇ-Ωψ μ<ν) = dec-Ωψ μ<ν |
| 68 | + core-monotone (<ᵇ-ψΩ μ<ν) = dec-ψΩ μ<ν |
| 69 | + core-monotone (<ᵇ-ψΩ≤ ν≤μ) = dec-ψΩ≤ ν≤μ |
| 70 | + core-monotone (<ᵇ-+ω x<ω) = dec-+ω x<ω |
| 71 | + core-monotone (<ᵇ-+ψω x<ψω) = dec-+ψω x<ψω |
| 72 | + core-monotone (<ᵇ-+1 x₁<y₁) = dec-+1 x₁<y₁ |
| 73 | + |
| 74 | + -- Generic derivation route: well-founded target + constructor monotonicity |
| 75 | + -- gives well-foundedness of the current `_ <ᵇ _` core via subrelation. |
| 76 | + core-wf : WellFounded _<ᵇ_ |
| 77 | + core-wf = |
| 78 | + let module SR = Subrelation core-monotone |
| 79 | + in SR.wellFounded (wellFounded measure ≺-wf) |
0 commit comments