agda: close final Veblen comparison-model lemma

Author: hyperpolymath

proofs/agda/Ordinal/Buchholz/Smoke.agda

@@ -150,6 +150,7 @@ open import Ordinal.Buchholz.VeblenComparisonTarget using
   ; _≺C_
   ; ≈ᶜ-+
   ; ≈ᶜ-ψ
+  ; ≈ᶜ-ψ+
   ; by-first
   ; by-second
   ; ≺C-wf
@@ -159,6 +160,7 @@ open import Ordinal.Buchholz.VeblenComparisonModel using
   ( cmp-payload
   ; cmp-measure
   ; cmp-dec-Ω+
+  ; cmp-dec-ψ+-same-index
   ; cmp-dec-ψ+
   ; comparison-interface
   ; core-wf-from-comparison

proofs/agda/Ordinal/Buchholz/VeblenComparisonModel.agda

@@ -3,9 +3,9 @@
 -- Comparison-model follow-up for the Veblen route.
 --
 -- This packages the new lexicographic comparison target into a
--- near-concrete interface instantiation. The two original deferred
--- same-binder obligations are discharged internally; the remaining
--- assumption is the lifted same-index ψ-to-plus case.
+-- concrete interface instantiation. The original deferred same-binder
+-- obligations and the lifted same-index ψ-to-plus case are all
+-- discharged internally.
 
 module Ordinal.Buchholz.VeblenComparisonModel where
 
@@ -33,21 +33,37 @@ open import Ordinal.Buchholz.Order using
 open import Ordinal.Buchholz.VeblenInterface using (VeblenWFInterface)
 open import Ordinal.Buchholz.VeblenComparisonTarget using
   ( ComparisonMeasure
+  ; Payload
+  ; payload-neutral
+  ; payload-psi
+  ; payload-plus
   ; _≈ᶜ_
   ; ≈ᶜ-+
   ; ≈ᶜ-ψ
-  ; ≈ᶜ-Ω
+  ; ≈ᶜ-ψ+
   ; _≺C_
+  ; _≺P_
+  ; pPsiPsi
+  ; pPsiPlus
   ; by-first
   ; by-second
+  ; by-payload-ψψ
+  ; by-payload-ψ+
+  ; by-payload-++
   ; ≺C-wf
   )
 
-cmp-payload : BT → BT
-cmp-payload bzero       = bzero
-cmp-payload (bOmega _)  = bzero
-cmp-payload (bplus _ y) = y
-cmp-payload (bpsi _ α)  = α
+cmp-anchor : BT → BT
+cmp-anchor bzero        = bzero
+cmp-anchor (bOmega μ)   = bOmega μ
+cmp-anchor (bpsi _ α)   = α
+cmp-anchor (bplus x _)  = cmp-anchor x
+
+cmp-payload : BT → Payload
+cmp-payload bzero       = payload-neutral
+cmp-payload (bOmega _)  = payload-neutral
+cmp-payload (bplus x y) = payload-plus (cmp-anchor x) y
+cmp-payload (bpsi _ α)  = payload-psi α
 
 cmp-measure : BT → ComparisonMeasure
 cmp-measure t = t , cmp-payload t
@@ -56,27 +72,37 @@ cmp-dec-Ω+ :
   ∀ {μ x y} →
   cmp-measure (bOmega μ) ≺C cmp-measure x →
   cmp-measure (bOmega μ) ≺C cmp-measure (bplus x y)
-cmp-dec-Ω+ (inj₁ Ω<x)            = by-first (<ᵇ-Ω+ Ω<x)
-cmp-dec-Ω+ (inj₂ (≈ᶜ-Ω , ()))
+cmp-dec-Ω+ (inj₁ Ω<x) = by-first (<ᵇ-Ω+ Ω<x)
+cmp-dec-Ω+ {x = bzero}      (inj₂ ())
+cmp-dec-Ω+ {x = bOmega _}   (inj₂ (≈ᶜ-Ω , ()))
+cmp-dec-Ω+ {x = bplus _ _}  (inj₂ ())
+cmp-dec-Ω+ {x = bpsi _ _}   (inj₂ ())
+
+cmp-payload-step :
+  ∀ {ν α x y} →
+  bpsi ν α ≈ᶜ x →
+  cmp-payload (bpsi ν α) ≺P cmp-payload x →
+  cmp-payload (bpsi ν α) ≺P cmp-payload (bplus x y)
+cmp-payload-step ≈ᶜ-ψ          (pPsiPsi α<β)  = by-payload-ψ+ α<β
+cmp-payload-step (≈ᶜ-ψ+ _)     (pPsiPlus α<β) = by-payload-ψ+ α<β
+
+cmp-dec-ψ+-same-index :
+  ∀ {ν α β y} →
+  α <ᵇ β →
+  cmp-measure (bpsi ν α) ≺C cmp-measure (bplus (bpsi ν β) y)
+cmp-dec-ψ+-same-index α<β =
+  by-second (≈ᶜ-ψ+ ≈ᶜ-ψ) (by-payload-ψ+ α<β)
 
 cmp-dec-ψ+ :
-  (dec-ψ+-same-index :
-    ∀ {ν α β y} →
-    α <ᵇ β →
-    cmp-measure (bpsi ν α) ≺C cmp-measure (bplus (bpsi ν β) y)) →
   ∀ {ν α x y} →
   cmp-measure (bpsi ν α) ≺C cmp-measure x →
   cmp-measure (bpsi ν α) ≺C cmp-measure (bplus x y)
-cmp-dec-ψ+ dec-ψ+-same-index (inj₁ ψ<x)          = by-first (<ᵇ-ψ+ ψ<x)
-cmp-dec-ψ+ dec-ψ+-same-index (inj₂ (≈ᶜ-ψ , α<β)) = dec-ψ+-same-index α<β
+cmp-dec-ψ+ (inj₁ ψ<x)             = by-first (<ᵇ-ψ+ ψ<x)
+cmp-dec-ψ+ (inj₂ (ψ≈x , ψ<x)) = by-second (≈ᶜ-ψ+ ψ≈x) (cmp-payload-step ψ≈x ψ<x)
 
 comparison-interface :
-  (dec-ψ+-same-index :
-    ∀ {ν α β y} →
-    α <ᵇ β →
-    cmp-measure (bpsi ν α) ≺C cmp-measure (bplus (bpsi ν β) y)) →
   VeblenWFInterface ComparisonMeasure _≺C_
-comparison-interface dec-ψ+-same-index = record
+comparison-interface = record
   { measure = cmp-measure
   ; ≺-wf = ≺C-wf
   ; dec-0-Ω = by-first <ᵇ-0-Ω
@@ -87,19 +113,14 @@ comparison-interface dec-ψ+-same-index = record
   ; dec-ψΩ = λ μ<ν → by-first (<ᵇ-ψΩ μ<ν)
   ; dec-ψΩ≤ = λ ν≤μ → by-first (<ᵇ-ψΩ≤ ν≤μ)
   ; dec-Ω+ = cmp-dec-Ω+
-  ; dec-ψ+ = cmp-dec-ψ+ dec-ψ+-same-index
+  ; dec-ψ+ = cmp-dec-ψ+
   ; dec-+Ω = λ x<Ω → by-first (<ᵇ-+Ω x<Ω)
   ; dec-+ψ = λ x<ψ → by-first (<ᵇ-+ψ x<ψ)
   ; dec-+1 = λ x₁<y₁ → by-first (<ᵇ-+1 x₁<y₁)
-  ; dec-ψα = λ α<β → by-second ≈ᶜ-ψ α<β
-  ; dec-+2 = λ y₂<z₂ → by-second ≈ᶜ-+ y₂<z₂
+  ; dec-ψα = λ α<β → by-second ≈ᶜ-ψ (by-payload-ψψ α<β)
+  ; dec-+2 = λ y₂<z₂ → by-second ≈ᶜ-+ (by-payload-++ y₂<z₂)
   }
 
-core-wf-from-comparison :
-  (dec-ψ+-same-index :
-    ∀ {ν α β y} →
-    α <ᵇ β →
-    cmp-measure (bpsi ν α) ≺C cmp-measure (bplus (bpsi ν β) y)) →
-  WellFounded _<ᵇ_
-core-wf-from-comparison dec-ψ+-same-index =
-  VeblenWFInterface.core-wf (comparison-interface dec-ψ+-same-index)
+core-wf-from-comparison : WellFounded _<ᵇ_
+core-wf-from-comparison =
+  VeblenWFInterface.core-wf comparison-interface

proofs/agda/Ordinal/Buchholz/VeblenComparisonTarget.agda

@@ -1,17 +1,21 @@
 {-# OPTIONS --safe --without-K #-}
 
 -- Lexicographic target that keeps the current Buchholz order on the
--- first coordinate, but relaxes the equality side-condition to
--- "same comparison binder" for the deferred shared-binder shapes.
+-- first coordinate, but relaxes the equality side-condition along
+-- recursive ψ-rooted comparison spines and uses a tagged payload
+-- order for the deferred shared-binder shapes.
 
 module Ordinal.Buchholz.VeblenComparisonTarget where
 
 open import Data.Product.Base using (_×_; _,_)
 open import Data.Product.Relation.Binary.Lex.Strict using (×-Lex; ×-wellFounded')
 open import Data.Sum.Base using (inj₁; inj₂)
-open import Induction.WellFounded using (WellFounded)
-open import Relation.Binary.Core using (Rel)
+open import Function.Base using (_on_)
+open import Induction.WellFounded using (WellFounded; module Subrelation)
+open import Relation.Binary.Core using (Rel; _⇒_)
+open import Relation.Binary.Construct.On as On using (wellFounded)
 open import Relation.Binary.Definitions using (_Respectsʳ_)
+open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 
 open import Ordinal.OmegaMarkers using (OmegaIndex)
 open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
@@ -25,25 +29,77 @@ open import Ordinal.Buchholz.Order using
   ; <ᵇ-ψΩ
   ; <ᵇ-+1
   ; <ᵇ-+ψ
+  ; <ᵇ-inv-+Ω
+  ; <ᵇ-inv-+ψ
   )
 open import Ordinal.Buchholz.WellFounded using (wf-<ᵇ)
 
 ComparisonMeasure : Set
-ComparisonMeasure = BT × BT
+data Payload : Set where
+  payload-neutral : Payload
+  payload-psi     : BT → Payload
+  payload-plus    : BT → BT → Payload
+
+ComparisonMeasure = BT × Payload
 
 infix 4 _≈ᶜ_ _≺C_
+infix 4 _≺P_
 
 data _≈ᶜ_ : BT → BT → Set where
   ≈ᶜ-zero : bzero ≈ᶜ bzero
   ≈ᶜ-Ω    : ∀ {μ : OmegaIndex} → bOmega μ ≈ᶜ bOmega μ
   ≈ᶜ-+    : ∀ {x y z} → bplus x y ≈ᶜ bplus x z
   ≈ᶜ-ψ    : ∀ {ν α β} → bpsi ν α ≈ᶜ bpsi ν β
+  ≈ᶜ-ψ+   : ∀ {ν α x y} → bpsi ν α ≈ᶜ x → bpsi ν α ≈ᶜ bplus x y
+
+data _≺P_ : Payload → Payload → Set where
+  pPsiPsi   : ∀ {α β} → α <ᵇ β → payload-psi α ≺P payload-psi β
+  pPsiPlus  : ∀ {α β y} → α <ᵇ β → payload-psi α ≺P payload-plus β y
+  pPlusPlus : ∀ {a y z} → y <ᵇ z → payload-plus a y ≺P payload-plus a z
 
 ≈ᶜ-trans : ∀ {x y z} → x ≈ᶜ y → y ≈ᶜ z → x ≈ᶜ z
 ≈ᶜ-trans ≈ᶜ-zero ≈ᶜ-zero = ≈ᶜ-zero
 ≈ᶜ-trans ≈ᶜ-Ω    ≈ᶜ-Ω    = ≈ᶜ-Ω
 ≈ᶜ-trans ≈ᶜ-+    ≈ᶜ-+    = ≈ᶜ-+
 ≈ᶜ-trans ≈ᶜ-ψ    ≈ᶜ-ψ    = ≈ᶜ-ψ
+≈ᶜ-trans ≈ᶜ-ψ    (≈ᶜ-ψ+ x≈y) = ≈ᶜ-ψ+ (≈ᶜ-trans ≈ᶜ-ψ x≈y)
+≈ᶜ-trans (≈ᶜ-ψ+ x≈y) ≈ᶜ-+ = ≈ᶜ-ψ+ x≈y
+
+<ᵇ-respʳ-≡ : _<ᵇ_ Respectsʳ _≡_
+<ᵇ-respʳ-≡ refl x<y = x<y
+
+payload-rank : Payload → BT × BT
+payload-rank payload-neutral    = bzero , bzero
+payload-rank (payload-psi α)    = α , bzero
+payload-rank (payload-plus a y) = a , y
+
+_≺PL_ : Rel (BT × BT) _
+_≺PL_ = ×-Lex _≡_ _<ᵇ_ _<ᵇ_
+
+payload-embed : _≺P_ ⇒ (_≺PL_ on payload-rank)
+payload-embed (pPsiPsi α<β)   = inj₁ α<β
+payload-embed (pPsiPlus α<β)  = inj₁ α<β
+payload-embed (pPlusPlus y<z) = inj₂ (refl , y<z)
+
+≺PL-wf : WellFounded _≺PL_
+≺PL-wf = ×-wellFounded' (λ where refl refl → refl) <ᵇ-respʳ-≡ wf-<ᵇ wf-<ᵇ
+
+≺P-wf : WellFounded _≺P_
+≺P-wf =
+  let module SR = Subrelation payload-embed
+  in SR.wellFounded (wellFounded payload-rank ≺PL-wf)
+
+<ᵇ-lift-plus : ∀ {x y z} → x <ᵇ y → x <ᵇ bplus y z
+<ᵇ-lift-plus {x} {y} {z} = lift x y z
+  where
+  lift : ∀ x y z → x <ᵇ y → x <ᵇ bplus y z
+  lift bzero        y              z _            = <ᵇ-0-+
+  lift (bOmega μ)   y              z x<y          = <ᵇ-Ω+ x<y
+  lift (bpsi ν α)   y              z x<y          = <ᵇ-ψ+ x<y
+  lift (bplus x₁ x₂) (bOmega μ)    z x<Ω          = <ᵇ-+1 (<ᵇ-inv-+Ω x<Ω)
+  lift (bplus x₁ x₂) (bpsi ν α)    z x<ψ          = <ᵇ-+1 (<ᵇ-inv-+ψ x<ψ)
+  lift (bplus x₁ x₂) (bplus y₁ y₂) z (<ᵇ-+1 x<y)  =
+    <ᵇ-+1 (lift x₁ y₁ y₂ x<y)
 
 <ᵇ-respʳ-≈ᶜ : _<ᵇ_ Respectsʳ _≈ᶜ_
 <ᵇ-respʳ-≈ᶜ ≈ᶜ-zero ()
@@ -56,15 +112,25 @@ data _≈ᶜ_ : BT → BT → Set where
 <ᵇ-respʳ-≈ᶜ ≈ᶜ-ψ    (<ᵇ-Ωψ μ<ν)    = <ᵇ-Ωψ μ<ν
 <ᵇ-respʳ-≈ᶜ ≈ᶜ-ψ    (<ᵇ-ψΩ μ<ν)    = <ᵇ-ψΩ μ<ν
 <ᵇ-respʳ-≈ᶜ ≈ᶜ-ψ    (<ᵇ-+ψ x<ψ)    = <ᵇ-+ψ (<ᵇ-respʳ-≈ᶜ ≈ᶜ-ψ x<ψ)
+<ᵇ-respʳ-≈ᶜ (≈ᶜ-ψ+ ψ≈x) x<ψ       = <ᵇ-lift-plus (<ᵇ-respʳ-≈ᶜ ψ≈x x<ψ)
 
 _≺C_ : Rel ComparisonMeasure _
-_≺C_ = ×-Lex _≈ᶜ_ _<ᵇ_ _<ᵇ_
+_≺C_ = ×-Lex _≈ᶜ_ _<ᵇ_ _≺P_
 
 by-first : ∀ {x y α β} → x <ᵇ y → (x , α) ≺C (y , β)
 by-first = inj₁
 
-by-second : ∀ {x y α β} → x ≈ᶜ y → α <ᵇ β → (x , α) ≺C (y , β)
+by-second : ∀ {x y α β} → x ≈ᶜ y → α ≺P β → (x , α) ≺C (y , β)
 by-second x≈y α<β = inj₂ (x≈y , α<β)
 
+by-payload-ψψ : ∀ {α β} → α <ᵇ β → payload-psi α ≺P payload-psi β
+by-payload-ψψ = pPsiPsi
+
+by-payload-ψ+ : ∀ {α β y} → α <ᵇ β → payload-psi α ≺P payload-plus β y
+by-payload-ψ+ = pPsiPlus
+
+by-payload-++ : ∀ {a y z} → y <ᵇ z → payload-plus a y ≺P payload-plus a z
+by-payload-++ = pPlusPlus
+
 ≺C-wf : WellFounded _≺C_
-≺C-wf = ×-wellFounded' ≈ᶜ-trans <ᵇ-respʳ-≈ᶜ wf-<ᵇ wf-<ᵇ
+≺C-wf = ×-wellFounded' ≈ᶜ-trans <ᵇ-respʳ-≈ᶜ wf-<ᵇ ≺P-wf