Skip to content

Commit 76cd412

Browse files
hyperpolymathhyperpolymath
committed
agda: add reduced-assumption Veblen comparison model
1 parent 4af27fe commit 76cd412

4 files changed

Lines changed: 197 additions & 0 deletions

File tree

‎proofs/agda/All.agda‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,8 @@ open import Ordinal.Buchholz.VeblenInterface
4343
open import Ordinal.Buchholz.VeblenIdentityModel
4444
open import Ordinal.Buchholz.VeblenMeasureTarget
4545
open import Ordinal.Buchholz.VeblenProjectionMeasure
46+
open import Ordinal.Buchholz.VeblenComparisonTarget
47+
open import Ordinal.Buchholz.VeblenComparisonModel
4648
open import Ordinal.Buchholz.VeblenObligations
4749
open import Ordinal.Buchholz.Smoke
4850

‎proofs/agda/Ordinal/Buchholz/Smoke.agda‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -144,6 +144,26 @@ open import Ordinal.Buchholz.VeblenProjectionMeasure using
144144
; proj-dec-ψΩ<
145145
)
146146

147+
open import Ordinal.Buchholz.VeblenComparisonTarget using
148+
( ComparisonMeasure
149+
; _≈ᶜ_
150+
; _≺C_
151+
; ≈ᶜ-+
152+
; ≈ᶜ-ψ
153+
; by-first
154+
; by-second
155+
; ≺C-wf
156+
)
157+
158+
open import Ordinal.Buchholz.VeblenComparisonModel using
159+
( cmp-payload
160+
; cmp-measure
161+
; cmp-dec-Ω+
162+
; cmp-dec-ψ+
163+
; comparison-interface
164+
; core-wf-from-comparison
165+
)
166+
147167
open import Ordinal.Buchholz.VeblenObligations using
148168
( plus-right
149169
; psi-arg

‎proofs/agda/Ordinal/Buchholz/VeblenComparisonModel.agda‎

Lines changed: 105 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,105 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
-- Comparison-model follow-up for the Veblen route.
4+
--
5+
-- This packages the new lexicographic comparison target into a
6+
-- near-concrete interface instantiation. The two original deferred
7+
-- same-binder obligations are discharged internally; the remaining
8+
-- assumption is the lifted same-index ψ-to-plus case.
9+
10+
module Ordinal.Buchholz.VeblenComparisonModel where
11+
12+
open import Induction.WellFounded using (WellFounded)
13+
open import Data.Product.Base using (_,_)
14+
open import Data.Sum.Base using (inj₁; inj₂)
15+
16+
open import Ordinal.OmegaMarkers using (_<Ω_; _≤Ω_)
17+
open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
18+
open import Ordinal.Buchholz.Order using
19+
( _<ᵇ_
20+
; <ᵇ-0-Ω
21+
; <ᵇ-0-+
22+
; <ᵇ-0-ψ
23+
; <ᵇ-ΩΩ
24+
; <ᵇ-Ωψ
25+
; <ᵇ-ψΩ
26+
; <ᵇ-ψΩ≤
27+
; <ᵇ-Ω+
28+
; <ᵇ-ψ+
29+
; <ᵇ-+Ω
30+
; <ᵇ-+ψ
31+
; <ᵇ-+1
32+
)
33+
open import Ordinal.Buchholz.VeblenInterface using (VeblenWFInterface)
34+
open import Ordinal.Buchholz.VeblenComparisonTarget using
35+
( ComparisonMeasure
36+
; _≈ᶜ_
37+
; ≈ᶜ-+
38+
; ≈ᶜ-ψ
39+
; ≈ᶜ-Ω
40+
; _≺C_
41+
; by-first
42+
; by-second
43+
; ≺C-wf
44+
)
45+
46+
cmp-payload : BT → BT
47+
cmp-payload bzero = bzero
48+
cmp-payload (bOmega _) = bzero
49+
cmp-payload (bplus _ y) = y
50+
cmp-payload (bpsi _ α) = α
51+
52+
cmp-measure : BT → ComparisonMeasure
53+
cmp-measure t = t , cmp-payload t
54+
55+
cmp-dec-Ω+ :
56+
∀ {μ x y} →
57+
cmp-measure (bOmega μ) ≺C cmp-measure x →
58+
cmp-measure (bOmega μ) ≺C cmp-measure (bplus x y)
59+
cmp-dec-Ω+ (inj₁ Ω<x) = by-first (<ᵇ-Ω+ Ω<x)
60+
cmp-dec-Ω+ (inj₂ (≈ᶜ-Ω , ()))
61+
62+
cmp-dec-ψ+ :
63+
(dec-ψ+-same-index :
64+
∀ {ν α β y} →
65+
α <ᵇ β →
66+
cmp-measure (bpsi ν α) ≺C cmp-measure (bplus (bpsi ν β) y)) →
67+
∀ {ν α x y} →
68+
cmp-measure (bpsi ν α) ≺C cmp-measure x →
69+
cmp-measure (bpsi ν α) ≺C cmp-measure (bplus x y)
70+
cmp-dec-ψ+ dec-ψ+-same-index (inj₁ ψ<x) = by-first (<ᵇ-ψ+ ψ<x)
71+
cmp-dec-ψ+ dec-ψ+-same-index (inj₂ (≈ᶜ-ψ , α<β)) = dec-ψ+-same-index α<β
72+
73+
comparison-interface :
74+
(dec-ψ+-same-index :
75+
∀ {ν α β y} →
76+
α <ᵇ β →
77+
cmp-measure (bpsi ν α) ≺C cmp-measure (bplus (bpsi ν β) y)) →
78+
VeblenWFInterface ComparisonMeasure _≺C_
79+
comparison-interface dec-ψ+-same-index = record
80+
{ measure = cmp-measure
81+
; ≺-wf = ≺C-wf
82+
; dec-0-Ω = by-first <ᵇ-0-Ω
83+
; dec-0-+ = by-first <ᵇ-0-+
84+
; dec-0-ψ = by-first <ᵇ-0-ψ
85+
; dec-ΩΩ = λ μ<ν → by-first (<ᵇ-ΩΩ μ<ν)
86+
; dec-Ωψ = λ μ<ν → by-first (<ᵇ-Ωψ μ<ν)
87+
; dec-ψΩ = λ μ<ν → by-first (<ᵇ-ψΩ μ<ν)
88+
; dec-ψΩ≤ = λ ν≤μ → by-first (<ᵇ-ψΩ≤ ν≤μ)
89+
; dec-Ω+ = cmp-dec-Ω+
90+
; dec-ψ+ = cmp-dec-ψ+ dec-ψ+-same-index
91+
; dec-+Ω = λ x<Ω → by-first (<ᵇ-+Ω x<Ω)
92+
; dec-+ψ = λ x<ψ → by-first (<ᵇ-+ψ x<ψ)
93+
; dec-+1 = λ x₁<y₁ → by-first (<ᵇ-+1 x₁<y₁)
94+
; dec-ψα = λ α<β → by-second ≈ᶜ-ψ α<β
95+
; dec-+2 = λ y₂<z₂ → by-second ≈ᶜ-+ y₂<z₂
96+
}
97+
98+
core-wf-from-comparison :
99+
(dec-ψ+-same-index :
100+
∀ {ν α β y} →
101+
α <ᵇ β →
102+
cmp-measure (bpsi ν α) ≺C cmp-measure (bplus (bpsi ν β) y)) →
103+
WellFounded _<ᵇ_
104+
core-wf-from-comparison dec-ψ+-same-index =
105+
VeblenWFInterface.core-wf (comparison-interface dec-ψ+-same-index)

‎proofs/agda/Ordinal/Buchholz/VeblenComparisonTarget.agda‎

Lines changed: 70 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,70 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
-- Lexicographic target that keeps the current Buchholz order on the
4+
-- first coordinate, but relaxes the equality side-condition to
5+
-- "same comparison binder" for the deferred shared-binder shapes.
6+
7+
module Ordinal.Buchholz.VeblenComparisonTarget where
8+
9+
open import Data.Product.Base using (_×_; _,_)
10+
open import Data.Product.Relation.Binary.Lex.Strict using (×-Lex; ×-wellFounded')
11+
open import Data.Sum.Base using (inj₁; inj₂)
12+
open import Induction.WellFounded using (WellFounded)
13+
open import Relation.Binary.Core using (Rel)
14+
open import Relation.Binary.Definitions using (_Respectsʳ_)
15+
16+
open import Ordinal.OmegaMarkers using (OmegaIndex)
17+
open import Ordinal.Buchholz.Syntax using (BT; bzero; bOmega; bplus; bpsi)
18+
open import Ordinal.Buchholz.Order using
19+
( _<ᵇ_
20+
; <ᵇ-0-+
21+
; <ᵇ-0-ψ
22+
; <ᵇ-Ω+
23+
; <ᵇ-Ωψ
24+
; <ᵇ-ψ+
25+
; <ᵇ-ψΩ
26+
; <ᵇ-+1
27+
; <ᵇ-+ψ
28+
)
29+
open import Ordinal.Buchholz.WellFounded using (wf-<ᵇ)
30+
31+
ComparisonMeasure : Set
32+
ComparisonMeasure = BT × BT
33+
34+
infix 4 _≈ᶜ_ _≺C_
35+
36+
data _≈ᶜ_ : BT → BT → Set where
37+
≈ᶜ-zero : bzero ≈ᶜ bzero
38+
≈ᶜ-Ω : ∀ {μ : OmegaIndex} → bOmega μ ≈ᶜ bOmega μ
39+
≈ᶜ-+ : ∀ {x y z} → bplus x y ≈ᶜ bplus x z
40+
≈ᶜ-ψ : ∀ {ν α β} → bpsi ν α ≈ᶜ bpsi ν β
41+
42+
≈ᶜ-trans : ∀ {x y z} → x ≈ᶜ y → y ≈ᶜ z → x ≈ᶜ z
43+
≈ᶜ-trans ≈ᶜ-zero ≈ᶜ-zero = ≈ᶜ-zero
44+
≈ᶜ-trans ≈ᶜ-Ω ≈ᶜ-Ω = ≈ᶜ-Ω
45+
≈ᶜ-trans ≈ᶜ-+ ≈ᶜ-+ = ≈ᶜ-+
46+
≈ᶜ-trans ≈ᶜ-ψ ≈ᶜ-ψ = ≈ᶜ-ψ
47+
48+
<ᵇ-respʳ-≈ᶜ : _<ᵇ_ Respectsʳ _≈ᶜ_
49+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-zero ()
50+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-Ω x<Ω = x<Ω
51+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-+ <ᵇ-0-+ = <ᵇ-0-+
52+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-+ (<ᵇ-Ω+ Ω<x) = <ᵇ-Ω+ Ω<x
53+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-+ (<ᵇ-ψ+ ψ<x) = <ᵇ-ψ+ ψ<x
54+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-+ (<ᵇ-+1 x<y) = <ᵇ-+1 x<y
55+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-ψ <ᵇ-0-ψ = <ᵇ-0-ψ
56+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-ψ (<ᵇ-Ωψ μ<ν) = <ᵇ-Ωψ μ<ν
57+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-ψ (<ᵇ-ψΩ μ<ν) = <ᵇ-ψΩ μ<ν
58+
<ᵇ-respʳ-≈ᶜ ≈ᶜ-ψ (<ᵇ-+ψ x<ψ) = <ᵇ-+ψ (<ᵇ-respʳ-≈ᶜ ≈ᶜ-ψ x<ψ)
59+
60+
_≺C_ : Rel ComparisonMeasure _
61+
_≺C_ = ×-Lex _≈ᶜ_ _<ᵇ_ _<ᵇ_
62+
63+
by-first : ∀ {x y α β} → x <ᵇ y → (x , α) ≺C (y , β)
64+
by-first = inj₁
65+
66+
by-second : ∀ {x y α β} → x ≈ᶜ y → α <ᵇ β → (x , α) ≺C (y , β)
67+
by-second x≈y α<β = inj₂ (x≈y , α<β)
68+
69+
≺C-wf : WellFounded _≺C_
70+
≺C-wf = ×-wellFounded' ≈ᶜ-trans <ᵇ-respʳ-≈ᶜ wf-<ᵇ wf-<ᵇ

0 commit comments

Comments
 (0)