Sign for integers and rationals

[dylanede]

I'm hoping to add functions to get the sign of integers (from HitInt) and rationals (for an eventual PR). So far I have this:

{-# OPTIONS --cubical --exact-split #-}

module hello-world where

open import IO
open import Cubical.HITs.HitInt renaming ( Sign to Sign'; sign to sign' )
open import Cubical.HITs.Rational
open import Cubical.Core.PropositionalTruncation
open import Cubical.Core.Everything
open import Cubical.Data.Bool
open import Cubical.Data.Nat
open import Cubical.Foundations.Function

data Sign : Set where
  pos neg zero : Sign

sign-ℤ : ℤ → Sign
sign-ℤ (pos zero) = zero
sign-ℤ (pos (suc n)) = pos
sign-ℤ (neg zero) = zero
sign-ℤ (neg (suc n)) = neg
sign-ℤ (posneg i) = zero

sign-ℚ : ℚ → Sign
sign-ℚ (con u a x) = case sign-ℤ u , sign-ℤ a of λ
  { (pos , pos) → pos
  ; (pos , neg) → neg
  ; (neg , pos) → neg
  ; (neg , neg) → pos
  ; (_ , zero) → {!!}
  ; (zero , _) → zero
  }
sign-ℚ (path u a v b x i) = {!!}
sign-ℚ (trunc q q₁ x y i i₁) = {!!}

I am however stuck on how to fill in the holes remaining. I'm still new to CTT. Any help would be appreciated.

[dylanede]

I think decidable signedness would be more useful, so I have this right now, still with holes:

data Sign : Set where
  pos neg zero : Sign

data ℤ-has-sign : Sign → ℤ → Set where
  ℤ-pos : ∀ n → ℤ-has-sign pos (pos (suc n))
  ℤ-zero : ℤ-has-sign zero (pos zero)
  ℤ-neg : ∀ n → ℤ-has-sign neg (neg (suc n))

ℤ₊ : Set
ℤ₊ = Σ ℤ (ℤ-has-sign pos)

ℤ₋ : Set
ℤ₋ = Σ ℤ (ℤ-has-sign neg)

sign-ℤ : (z : ℤ) → Σ[ s ∈ Sign ] (ℤ-has-sign s z)
sign-ℤ (pos zero) = zero , ℤ-zero
sign-ℤ (pos (suc n)) = pos , ℤ-pos n
sign-ℤ (neg zero) = zero , subst (ℤ-has-sign zero) posneg ℤ-zero
sign-ℤ (neg (suc n)) = neg , ℤ-neg n
sign-ℤ (posneg i) = zero , {!!} -- no idea

data ℚ-has-sign : Sign → ℚ → Set where
  ℚ-pos₁ : ∀ {u a x} → ℤ-has-sign pos u → ℤ-has-sign pos a → ℚ-has-sign pos (con u a x)
  ℚ-pos₂ : ∀ {u a x} → ℤ-has-sign neg u → ℤ-has-sign neg a → ℚ-has-sign pos (con u a x)
  ℚ-zero : ∀ {u a x} → ℤ-has-sign zero u → ℚ-has-sign zero (con u a x)
  ℚ-neg₁ : ∀ {u a x} → ℤ-has-sign pos u → ℤ-has-sign neg a → ℚ-has-sign neg (con u a x)
  ℚ-neg₂ : ∀ {u a x} → ℤ-has-sign neg u → ℤ-has-sign pos a → ℚ-has-sign neg (con u a x)

ℚ₊ : Set
ℚ₊ = Σ ℚ (ℚ-has-sign pos)

ℚ₋ : Set
ℚ₋ = Σ ℚ (ℚ-has-sign neg)

sign-ℚ : (q : ℚ) → Σ[ s ∈ Sign ] (ℚ-has-sign s q)
sign-ℚ (con u a x) = case sign-ℤ u , sign-ℤ a of λ
  { ((pos , u-pos) , pos , a-pos) → pos , ℚ-pos₁ u-pos a-pos
  ; ((pos , u-pos) , neg , a-neg) → neg , ℚ-neg₁ u-pos a-neg
  ; ((pos , u-pos) , zero , ℤ-zero) → ⊥-elim (x refl)
  ; ((neg , u-neg) , pos , a-pos) → neg , ℚ-neg₂ u-neg a-pos
  ; ((neg , u-neg) , neg , a-neg) → pos , ℚ-pos₂ u-neg a-neg
  ; ((neg , u-neg) , zero , ℤ-zero) → ⊥-elim (x refl)
  ; ((zero , u-zero) , _) → zero , ℚ-zero u-zero
  }
sign-ℚ (path u a v b x i) = {!!} -- no idea
sign-ℚ (trunc q q₁ x y i i₁) = {!!} -- no idea

[WorldSEnder]

It might be easier to work with a different definition for rational instead.

-- z over-suc n == z / (n + 1) , see also HoTT book 11.1
data ℚ : Set where
  _over-suc_ : (z : ℤ) (n : ℕ) → ℚ
  path : ∀ a u b v → (a *ℤ pos (1 + v)) ≡ (u *ℤ pos (1 + b)) → a over-suc b ≡ u over-suc v
  trunc : isSet ℚ

[Saizan]

@WorldSEnder why do you think it might be easier?

@dylanede Do you have a specific reason to include zero as one of the signs? My first thought would be to just send it to pos.

[dylanede]

Well, I was planning on using strictly positive rationals as part of an implementation of the Cauchy reals (as per the HoTT book), though I am now not sure whether a sigma type like ℚ₊ built on ℚ-has-sign pos is the best thing to use for that.

[dylanede]

I think it would still be useful though to know how to fill the holes in the code I've given. It should be possible, right?

[Saizan]

This is how I would make progress on the first attempt

_*S_ : Sign → Sign → Sign
pos *S x = x
x *S pos = x
neg *S neg = pos
_  *S zero = zero
zero *S x = zero

isSetSign : isSet Sign
isSetSign = { }0
-- should have a proof similar to the one for Bool

lemma0 : ∀ u a → sign-ℤ (u *ℤ a) ≡ sign-ℤ u *S sign-ℤ a

-- probably want some other lemmas to finish this proof.
lemma : ∀ u a v b → u *S b ≡ v *S a → u *S a ≡ v *S b
lemma pos a pos b eq = sym eq
lemma pos a neg b eq = { }1
lemma pos a zero b eq = { }2
lemma neg a pos b eq = { }3
lemma neg a neg b eq = sym eq
lemma neg a zero b eq = { }4
lemma zero a pos b eq = { }5
lemma zero a neg b eq = { }6
lemma zero a zero b eq = sym eq

sign-ℚ : ℚ → Sign
sign-ℚ (con u a x) = sign-ℤ u *S sign-ℤ a
sign-ℚ (path u a v b x i) = lemma (sign-ℤ u) (sign-ℤ a) (sign-ℤ v) (sign-ℤ b)
                                  (sym (lemma0 u b) ∙ cong sign-ℤ x ∙ lemma0 v a) i
sign-ℚ (trunc q q₁ x y i i₁) = isSetSign (sign-ℚ q) (sign-ℚ q₁) (cong sign-ℚ x) (cong sign-ℚ y) i i₁

[Alizter]

Well Sign is equivalent to Fin 3, so we can get isSet from there too.

[WorldSEnder]

I thought it might be easier because

• the sign of the definition I gave depends only on z. What is left to prove is basically that the sign is invariant on each path. That should be easy because in the constructor path you only multiply by positive numbers.
• you don't have to carry around a proof that n is not zero.

[Alizter]

Once we show those two definitions of Q are equivalent #116 then Sign should be defined for both anyway right?

[dylanede]

@Saizan, thanks for that, that snippet has really helped me.