Skip to content

Add boolean builtins in Nat #1262

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
felixwellen merged 5 commits into from
Oct 17, 2025
Merged

Add boolean builtins in Nat #1262

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
7e99fdb
Add boolean builtins in `Nat` and update dependencies for compatibility
LorenzoMolena Sep 24, 2025
7990fd3
add reference to an example of how to use `UsingEq` in a with-abstrac…
LorenzoMolena Oct 8, 2025
9d81f5b
remove `UsingEq` where not needed, remove case split on `m` and `n` o…
LorenzoMolena Oct 12, 2025
afb0bfe
remove unnecessary case split on `m` and `n` in the definition of `_≟_`
LorenzoMolena Oct 12, 2025
7a0d824
add comment about `inspect`
LorenzoMolena Oct 17, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Cubical/Algebra/DirectSum/Equiv-DSHIT-DSFun.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -386,7 +386,7 @@ module Equiv-Properties
lemmakk zero a = cong (base 0) (transportRefl a)
lemmakk (suc k) a with (discreteℕ (suc k) (suc k)) | (discreteℕ k k)
... | yes p | yes q = cong₂ _add_
(sym (constSubstCommSlice G (⊕HIT ℕ G Gstr) base (cong suc q) a))
(sym (constSubstCommSlice G (⊕HIT ℕ G Gstr) base p a))
(lemmaSkk (suc k) a k ≤-refl)
∙ +⊕HIT-IdR _
... | yes p | no ¬q = ⊥.rec (¬q refl)
Expand Down
17 changes: 11 additions & 6 deletions Cubical/Algebra/Semilattice/Instances/NatMax.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,17 +35,22 @@ isSemilattice maxSemilatticeStr = makeIsSemilattice isSetℕ maxAssoc maxRId max
maxAssoc : (x y z : ℕ) → max x (max y z) ≡ max (max x y) z
maxAssoc zero y z = refl
maxAssoc (suc x) zero z = refl
maxAssoc (suc x) (suc y) zero = refl
maxAssoc (suc x) (suc y) (suc z) = cong suc (maxAssoc x y z)
maxAssoc (suc x) (suc y) zero = maxSuc ∙ cong (λ p → max p _) (sym (maxSuc {x} {y}))
maxAssoc (suc x) (suc y) (suc z) =
max (suc x) (max (suc y) (suc z)) ≡⟨ cong (max _) (maxSuc {y} {z}) ⟩
max (suc x) (suc (max y z)) ≡⟨ maxSuc ⟩
suc (max x (max y z)) ≡⟨ cong suc (maxAssoc x y z) ⟩
suc (max (max x y) z) ≡⟨ sym maxSuc ⟩
max (suc (max x y)) (suc z) ≡⟨ cong (λ p → max p _) (sym (maxSuc {x} {y})) ⟩
max (max (suc x) (suc y)) (suc z) ∎

maxRId : (x : ℕ) → max x 0 ≡ x
maxRId zero = refl
maxRId (suc x) = refl

maxIdem : (x : ℕ) → max x x ≡ x
maxIdem zero = refl
maxIdem (suc x) = cong suc (maxIdem x)

maxIdem (suc x) = maxSuc ∙ cong suc (maxIdem x)


--characterisation of inequality
Expand All @@ -54,13 +59,13 @@ open JoinSemilattice (ℕ , maxSemilatticeStr) renaming (_≤_ to _≤max_)
≤max→≤ℕ : ∀ x y → x ≤max y → x ≤ℕ y
≤max→≤ℕ zero y _ = zero-≤
≤max→≤ℕ (suc x) zero p = ⊥.rec (snotz p)
≤max→≤ℕ (suc x) (suc y) p = let (k , q) = ≤max→≤ℕ x y (cong predℕ p) in
≤max→≤ℕ (suc x) (suc y) p = let (k , q) = ≤max→≤ℕ x y (cong predℕ (sym maxSuc ∙ p)) in
k , +-suc k x ∙ cong suc q

≤ℕ→≤max : ∀ x y → x ≤ℕ y → x ≤max y
≤ℕ→≤max zero y _ = refl
≤ℕ→≤max (suc x) zero p = ⊥.rec (¬-<-zero p)
≤ℕ→≤max (suc x) (suc y) (k , p) = cong suc (≤ℕ→≤max x y (k , q))
≤ℕ→≤max (suc x) (suc y) (k , p) = maxSuc ∙ cong suc (≤ℕ→≤max x y (k , q))
where
q : k +ℕ x ≡ y
q = cong predℕ (sym (+-suc k x) ∙ p)
Expand Down
2 changes: 1 addition & 1 deletion Cubical/Data/Nat/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ module Cubical.Data.Nat.Base where

open import Agda.Builtin.Nat public
using (zero; suc; _+_)
renaming (Nat to ℕ; _-_ to _∸_; _*_ to _·_)
renaming (Nat to ℕ; _-_ to _∸_; _*_ to _·_ ; _<_ to _<ᵇ_ ; _==_ to _≡ᵇ_)

open import Cubical.Data.Nat.Literals public
open import Cubical.Data.Bool.Base
Expand Down
73 changes: 67 additions & 6 deletions Cubical/Data/Nat/Order.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,8 @@ open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma
open import Cubical.Data.Sum as ⊎

open import Cubical.Data.Bool.Base hiding (_≟_)

open import Cubical.Data.Nat.Base
open import Cubical.Data.Nat.Properties

Expand Down Expand Up @@ -258,22 +260,59 @@ predℕ-≤-predℕ {suc m} {suc n} ineq = pred-≤-pred ineq
left-≤-max : m ≤ max m n
left-≤-max {zero} {n} = zero-≤
left-≤-max {suc m} {zero} = ≤-refl
left-≤-max {suc m} {suc n} = suc-≤-suc left-≤-max
left-≤-max {suc m} {suc n} = subst (_ ≤_) (sym maxSuc) $ suc-≤-suc $ left-≤-max {m} {n}

right-≤-max : n ≤ max m n
right-≤-max {zero} {m} = zero-≤
right-≤-max {suc n} {zero} = ≤-refl
right-≤-max {suc n} {suc m} = suc-≤-suc right-≤-max
right-≤-max {suc n} {suc m} = subst (_ ≤_) (sym maxSuc) $ suc-≤-suc $ right-≤-max {n} {m}

min-≤-left : min m n ≤ m
min-≤-left {zero} {n} = ≤-refl
min-≤-left {suc m} {zero} = zero-≤
min-≤-left {suc m} {suc n} = suc-≤-suc min-≤-left
min-≤-left {suc m} {suc n} = subst (_≤ _) (sym minSuc) $ suc-≤-suc $ min-≤-left {m} {n}

min-≤-right : min m n ≤ n
min-≤-right {zero} {n} = zero-≤
min-≤-right {suc m} {zero} = ≤-refl
min-≤-right {suc m} {suc n} = suc-≤-suc min-≤-right
min-≤-right {suc m} {suc n} = subst (_≤ _) (sym minSuc) $ suc-≤-suc $ min-≤-right {m} {n}

-- Boolean order relations and their conversions to/from ≤ and <

_≤ᵇ_ : ℕ → ℕ → Bool
m ≤ᵇ n = m <ᵇ suc n

_≥ᵇ_ : ℕ → ℕ → Bool
m ≥ᵇ n = n ≤ᵇ m

_>ᵇ_ : ℕ → ℕ → Bool
m >ᵇ n = n <ᵇ m

private
≤ᵇ-∸-+-cancel : ∀ m n → Bool→Type (m ≤ᵇ n) → (n ∸ m) + m ≡ n
≤ᵇ-∸-+-cancel zero zero t = refl
≤ᵇ-∸-+-cancel zero (suc n) t = +-zero (suc n)
≤ᵇ-∸-+-cancel (suc m) (suc n) t = +-suc (n ∸ m) m ∙ cong suc (≤ᵇ-∸-+-cancel m n t)

<ᵇ→< : Bool→Type (m <ᵇ n) → m < n
<ᵇ→< {m} {suc n} t .fst = n ∸ m
<ᵇ→< {m} {suc n} t .snd =
n ∸ m + suc m ≡⟨ +-suc (n ∸ m) m ⟩
suc (n ∸ m + m) ≡⟨ cong suc (≤ᵇ-∸-+-cancel m n t) ⟩
suc n ∎

<→<ᵇ : m < n → Bool→Type (m <ᵇ n)
<→<ᵇ {m} {zero} m<0 = ¬-<-zero m<0
<→<ᵇ {zero} {suc n} 0<sn = tt
<→<ᵇ {suc m} {suc n} sm<sn = <→<ᵇ (pred-≤-pred sm<sn)

≤ᵇ→≤ : Bool→Type (m ≤ᵇ n) → m ≤ n
≤ᵇ→≤ {zero} {n} t = zero-≤
≤ᵇ→≤ {suc m} {suc n} t = <ᵇ→< t

≤→≤ᵇ : m ≤ n → Bool→Type (m ≤ᵇ n)
≤→≤ᵇ {zero} {n} 0≤n = tt
≤→≤ᵇ {suc m} {n} sm≤n = <→<ᵇ sm≤n

≤Dec : ∀ m n → Dec (m ≤ n)
≤Dec zero n = yes (n , +-zero _)
Expand All @@ -296,11 +335,30 @@ Trichotomy-suc (lt m<n) = lt (suc-≤-suc m<n)
Trichotomy-suc (eq m=n) = eq (cong suc m=n)
Trichotomy-suc (gt n<m) = gt (suc-≤-suc n<m)

private
∸→>ᵇ : ∀ m n → caseNat ⊥.⊥ Unit (m ∸ n) → Bool→Type (m >ᵇ n)
∸→>ᵇ (suc m) zero t = tt
∸→>ᵇ (suc m) (suc n) t = ∸→>ᵇ m n t

_≟_ : ∀ m n → Trichotomy m n
zero ≟ zero = eq refl
zero ≟ suc n = lt (n , +-comm n 1)
suc m ≟ zero = gt (m , +-comm m 1)
suc m ≟ suc n = Trichotomy-suc (m ≟ n)
suc m ≟ suc n with m ∸ n UsingEq | n ∸ m UsingEq
... | zero , p | zero , q = eq (∸≡0→≡ p q)
... | zero , p | suc _ , q = lt (<ᵇ→< $ ∸→>ᵇ n m $ subst (caseNat ⊥.⊥ Unit) (sym q) tt)
... | suc _ , p | zero , q = gt (<ᵇ→< $ ∸→>ᵇ m n $ subst (caseNat ⊥.⊥ Unit) (sym p) tt)
... | suc _ , p | suc _ , q = ⊥.rec $ ¬m<m {m} $ <-trans
(<ᵇ→< $ ∸→>ᵇ n m $ subst (caseNat ⊥.⊥ Unit) (sym q) tt)
(<ᵇ→< $ ∸→>ᵇ m n $ subst (caseNat ⊥.⊥ Unit) (sym p) tt)

-- Alternative version of ≟, defined without builtin primitives

_≟'_ : ∀ m n → Trichotomy m n
zero ≟' zero = eq refl
zero ≟' suc n = lt (n , +-comm n 1)
suc m ≟' zero = gt (m , +-comm m 1)
suc m ≟' suc n = Trichotomy-suc (m ≟' n)

Dichotomyℕ : ∀ (n m : ℕ) → (n ≤ m) ⊎ (n > m)
Dichotomyℕ n m with (n ≟ m)
Expand Down Expand Up @@ -331,7 +389,10 @@ splitℕ-< m n with m ≟ n
<-split : m < suc n → (m < n) ⊎ (m ≡ n)
<-split {n = zero} = inr ∘ snd ∘ m+n≡0→m≡0×n≡0 ∘ snd ∘ pred-≤-pred
<-split {zero} {suc n} = λ _ → inl (suc-≤-suc zero-≤)
<-split {suc m} {suc n} = ⊎.map suc-≤-suc (cong suc) ∘ <-split ∘ pred-≤-pred
<-split {suc m} {suc n} sm<ssn with m ≟ n
... | lt m<n = inl (suc-≤-suc m<n)
... | eq m≡n = inr (cong suc m≡n)
... | gt n<m = ⊥.rec $ ¬m<m {suc (suc n)} $ ≤-trans (suc-≤-suc (suc-≤-suc n<m)) sm<ssn

≤-split : m ≤ n → (m < n) ⊎ (m ≡ n)
≤-split p = <-split (suc-≤-suc p)
Expand Down
53 changes: 46 additions & 7 deletions Cubical/Data/Nat/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,8 @@ open import Cubical.Data.Empty as ⊥
open import Cubical.Data.Sigma
open import Cubical.Data.Sum.Base

open import Cubical.Data.Bool.Base

open import Cubical.Relation.Nullary

private
Expand All @@ -21,24 +23,44 @@ private
min : ℕ → ℕ → ℕ
min zero m = zero
min (suc n) zero = zero
min (suc n) (suc m) = suc (min n m)
min (suc n) (suc m) with n <ᵇ m UsingEq
... | false , _ = suc m
... | true , _ = suc n

minSuc : min (suc n) (suc m) ≡ suc (min n m)
minSuc {zero} {zero} = refl
minSuc {zero} {suc m} = refl
minSuc {suc n} {zero} = refl
minSuc {suc n} {suc m} with suc n <ᵇ suc m
... | false = refl
... | true = refl

minComm : (n m : ℕ) → min n m ≡ min m n
minComm zero zero = refl
minComm zero (suc m) = refl
minComm (suc n) zero = refl
minComm (suc n) (suc m) = cong suc (minComm n m)
minComm (suc n) (suc m) = minSuc ∙∙ cong suc (minComm n m) ∙∙ sym minSuc

max : ℕ → ℕ → ℕ
max zero m = m
max (suc n) zero = suc n
max (suc n) (suc m) = suc (max n m)
max (suc n) (suc m) with n <ᵇ m UsingEq
... | false , _ = suc n
... | true , _ = suc m

maxSuc : max (suc n) (suc m) ≡ suc (max n m)
maxSuc {zero} {zero} = refl
maxSuc {zero} {suc m} = refl
maxSuc {suc n} {zero} = refl
maxSuc {suc n} {suc m} with suc n <ᵇ suc m
... | false = refl
... | true = refl

maxComm : (n m : ℕ) → max n m ≡ max m n
maxComm zero zero = refl
maxComm zero (suc m) = refl
maxComm (suc n) zero = refl
maxComm (suc n) (suc m) = cong suc (maxComm n m)
maxComm (suc n) (suc m) = maxSuc ∙∙ cong suc (maxComm n m) ∙∙ sym maxSuc

znots : ¬ (0 ≡ suc n)
znots eq = subst (caseNat ℕ ⊥) eq 0
Expand Down Expand Up @@ -122,14 +144,25 @@ decodeℕ (suc n) (suc m) = λ r → cong suc (decodeℕ n m r)
retr : (n m : ℕ) → (p : n ≡ m) → decodeℕ n m (compute-eqℕ n m p) ≡ p
retr n m p = J (λ m p → decodeℕ n m (compute-eqℕ n m p) ≡ p) (reflRetr n) p

-- Conversions between boolean equality (≡ᵇ) and path equality (≡)

≡ᵇ→≡ : Bool→Type (m ≡ᵇ n) → m ≡ n
≡ᵇ→≡ {zero} {zero} t = refl
≡ᵇ→≡ {suc m} {suc n} t = cong suc (≡ᵇ→≡ t)

≡→≡ᵇ : m ≡ n → Bool→Type (m ≡ᵇ n)
≡→≡ᵇ {zero} {zero} _ = tt
≡→≡ᵇ {zero} {suc n} p = ⊥.rec (znots p)
≡→≡ᵇ {suc m} {zero} p = ⊥.rec (snotz p)
≡→≡ᵇ {suc m} {suc n} p = ≡→≡ᵇ {m} {n} (cong predℕ p)

discreteℕ : Discrete ℕ
discreteℕ zero zero = yes refl
discreteℕ zero (suc n) = no znots
discreteℕ (suc m) zero = no snotz
discreteℕ (suc m) (suc n) with discreteℕ m n
... | yes p = yes (cong suc p)
... | no p = no (λ x → p (injSuc x))
discreteℕ (suc m) (suc n) with m ≡ᵇ n UsingEq
... | false , p = no (subst Bool→Type p ∘ ≡→≡ᵇ)
... | true , p = yes (≡ᵇ→≡ (subst Bool→Type (sym p) tt))

separatedℕ : Separated ℕ
separatedℕ = Discrete→Separated discreteℕ
Expand Down Expand Up @@ -270,6 +303,12 @@ n∸n (suc n) = n∸n n
∸-distribʳ zero (suc n) k = sym (zero∸ (k + n · k))
∸-distribʳ (suc m) (suc n) k = ∸-distribʳ m n k ∙ sym (∸-cancelˡ k (m · k) (n · k))

∸≡0→≡ : m ∸ n ≡ 0 → n ∸ m ≡ 0 → m ≡ n
∸≡0→≡ {zero} {zero} _ _ = refl
∸≡0→≡ {zero} {suc n} _ q = ⊥.rec (snotz q)
∸≡0→≡ {suc m} {zero} p _ = ⊥.rec (snotz p)
∸≡0→≡ {suc m} {suc n} p q = cong suc (∸≡0→≡ {m} {n} p q)

infix 6 _!
infix 7 _choose_

Expand Down
12 changes: 12 additions & 0 deletions Cubical/Foundations/Prelude.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -498,6 +498,18 @@ isContrSinglP A a .fst = _ , transport-filler (λ i → A i) a
isContrSinglP A a .snd (x , p) i =
_ , λ j → fill A (λ j → λ {(i = i0) → transport-filler (λ i → A i) a j; (i = i1) → p j}) (inS a) j

-- Helpers for carrying equalities into with-abstractions
-- see `discreteℕ` in Data.Nat.Properties for an example of usage

infixl 0 _UsingEq
infixl 0 _i0:>_UsingEqP

_UsingEq : (a : A) → singl a
Copy link
Collaborator

@felixwellen felixwellen Oct 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Add a comment showing how this can be used

Copy link
Contributor Author

@LorenzoMolena LorenzoMolena Oct 8, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is the comment I just added enough?

Copy link
Contributor

@anshwad10 anshwad10 Oct 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It looke like this has exactly the same use case as inspect. Is this not redundant?

Copy link
Contributor Author

@LorenzoMolena LorenzoMolena Oct 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you, I completely missed it. Do you know exactly how should I use it?
Right now I'm trying to case-split on inspect (_≡ᵇ n) m in the proof of discreteness of ℕ, but this doesn't seem to work, since it only gives me the path, but not each boolean case.

Copy link
Contributor Author

@LorenzoMolena LorenzoMolena Oct 11, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nevermind, I got it.

Is this what you meant?

discreteℕ : Discrete ℕ
discreteℕ zero zero = yes refl
discreteℕ zero (suc n) = no znots
discreteℕ (suc m) zero = no snotz
discreteℕ (suc m) (suc n) with m ≡ᵇ n | inspect (m ≡ᵇ_) n
... | false | [ p ]ᵢ = no  (subst Bool→Type p ∘ ≡→≡ᵇ)
... | true  | [ p ]ᵢ = yes (≡ᵇ→≡ (subst Bool→Type (sym p) tt))

a UsingEq = isContrSingl a .fst

_i0:>_UsingEqP : (A : I → Type ℓ) (a : A i0) → singlP A a
A i0:> a UsingEqP = isContrSinglP A a .fst

-- Higher cube types

SquareP :
Expand Down
19 changes: 14 additions & 5 deletions Cubical/HITs/Truncation/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -213,24 +213,33 @@ isOfHLevelMin→isOfHLevel {n = suc n} {m = zero} h = (isContr→isOfHLevel (suc
isOfHLevelMin→isOfHLevel {A = A} {n = suc n} {m = suc m} h =
subst (λ x → isOfHLevel x A) (helper n m)
(isOfHLevelPlus (suc n ∸ (suc (min n m))) h)
, subst (λ x → isOfHLevel x A) ((λ i → m ∸ (minComm n m i) + suc (minComm n m i)) ∙ helper m n)
, subst (λ x → isOfHLevel x A) ((λ i → m ∸ (minComm n m i) + (minComm (suc n) (suc m) i)) ∙ helper m n)
(isOfHLevelPlus (suc m ∸ (suc (min n m))) h)
where
helper : (n m : ℕ) → n ∸ min n m + suc (min n m) ≡ suc n
helper : (n m : ℕ) → n ∸ min n m + min (suc n) (suc m) ≡ suc n
helper zero zero = refl
helper zero (suc m) = refl
helper (suc n) zero = cong suc (+-comm n 1)
helper (suc n) (suc m) = +-suc _ _ ∙ cong suc (helper n m)
helper (suc n) (suc m) =
suc n ∸ min (suc n) (suc m) + min (suc (suc n)) (suc (suc m)) ≡⟨ step0 ⟩
suc n ∸ suc (min n m) + suc (min (suc n) (suc m)) ≡⟨⟩
n ∸ min n m + suc (min (suc n) (suc m)) ≡⟨ step1 ⟩
suc (n ∸ min n m + min (suc n) (suc m)) ≡⟨ step2 ⟩
suc (suc n) ∎
where
step0 = cong₂ (λ p → suc n ∸ p +_) (minSuc {n}) minSuc
step1 = +-suc _ _
step2 = cong suc (helper n m)

ΣTruncElim : ∀ {ℓ ℓ' ℓ''} {A : Type ℓ} {n m : ℕ}
{B : (x : ∥ A ∥ n) → Type ℓ'}
{C : (Σ[ a ∈ (∥ A ∥ n) ] (∥ B a ∥ m)) → Type ℓ''}
→ ((x : (Σ[ a ∈ (∥ A ∥ n) ] (∥ B a ∥ m))) → isOfHLevel (min n m) (C x))
→ ((a : A) (b : B (∣ a ∣ₕ)) → C (∣ a ∣ₕ , ∣ b ∣ₕ))
→ (x : (Σ[ a ∈ (∥ A ∥ n) ] (∥ B a ∥ m))) → C x
ΣTruncElim hB g (a , b) =
ΣTruncElim {n = n} hB g (a , b) =
elim (λ x → isOfHLevelΠ _ λ b → isOfHLevelMin→isOfHLevel (hB (x , b)) .fst )
(λ a → elim (λ _ → isOfHLevelMin→isOfHLevel (hB (∣ a ∣ₕ , _)) .snd) λ b → g a b)
(λ a → elim (λ _ → isOfHLevelMin→isOfHLevel {n = n} (hB (∣ a ∣ₕ , _)) .snd) λ b → g a b)
a b

truncIdempotentIso : (n : ℕ) → isOfHLevel n A → Iso (∥ A ∥ n) A
Expand Down