CoNaturals.Arithmetic

Martin Escardo, 12th September 2018.

We define arithmetic operations on ℕ∞ by corecursion as defined in the
module CoNaturals. The lack of pattern matching on Zero and Succ and
of some definitional equalities make some proofs lengthier than they
would be if we had used a built-in coinductive definition of ℕ∞.

We use the final coalgebra property of ℕ∞ for the functor 𝟙 + (-) to
both construct the functions and prove their properties (including
idempotency, commutativity and associativity of the minimum
operation).

NB. There are shorter constructions with more direct proofs of the
minimum function, e.g. take the pointwise minimum in 𝟚 (see the
module GenericConvergentSequence), but this module
serves as a good illustration of reasoning with the final coalgebra
property to both construct functions and prove their properties.

This file will grow on demand. The first operation we needed (for
codistances) is minimum.


{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan
open import UF.FunExt

module CoNaturals.Arithmetic (fe : FunExt) where

private
 fe₀ : funext 𝓤₀ 𝓤₀
 fe₀ = fe 𝓤₀ 𝓤₀

open import MLTT.Two-Properties
open import CoNaturals.Type renaming (min to min')
open import CoNaturals.UniversalProperty fe
open import Notation.Order
open import Notation.CanonicalMap


We consider a 𝟙 + (-) coalgebra κ on ℕ∞ × ℕ∞ so that min is the unique
homomorphism to the final coalgebra PRED : ℕ∞ → 𝟙 + ℕ∞ on ℕ∞.


private
 κ-min : ℕ∞ × ℕ∞ → 𝟙 {𝓤₀} + ℕ∞ × ℕ∞
 κ-min (u , v) = 𝟚-Cases (positivity u)
                  (inl ⋆)
                  (𝟚-Cases (positivity v)
                    (inl ⋆)
                    (inr (Pred u , Pred v)))

min : ℕ∞ × ℕ∞ → ℕ∞
min = ℕ∞-corec κ-min


The defining equations of min thus are:


min-eq₀ : ∀ v   → min (Zero , v) ＝ Zero
min-eq₁ : ∀ u   → min (Succ u , Zero) ＝ Zero
min-eq₂ : ∀ u v → min (Succ u , Succ v) ＝ Succ (min (u , v))

min-eq₀ = λ v   → Coalg-morphism-Zero κ-min (Zero , v) ⋆ refl
min-eq₁ = λ u   → Coalg-morphism-Zero κ-min (Succ u , Zero) ⋆ refl
min-eq₂ = λ u v → Coalg-morphism-Succ κ-min (Succ u , Succ v) (u , v) refl


Maximum (another version is defined in GenericConvergentSequence):


private
 κ-max : ℕ∞ × ℕ∞ → 𝟙 {𝓤₀} + ℕ∞ × ℕ∞
 κ-max (u , v) = 𝟚-Cases (positivity u)
                   (𝟚-Cases (positivity v)
                      (inl ⋆)
                      (inr (Zero , Pred v)))
                   (𝟚-Cases (positivity v)
                      (inr (Pred u , Zero))
                      (inr (Pred u , (Pred v))))

max' : ℕ∞ × ℕ∞ → ℕ∞
max' = ℕ∞-corec κ-max

max-eq₀ :         max' (Zero , Zero) ＝ Zero
max-eq₁ : ∀ v   → max' (Zero , Succ v) ＝ Succ (max' (Zero , v))
max-eq₂ : ∀ u   → max' (Succ u , Zero) ＝ Succ (max' (u , Zero))
max-eq₃ : ∀ u v → max' (Succ u , Succ v) ＝ Succ (max' (u , v))

max-eq₀ =         Coalg-morphism-Zero κ-max (Zero , Zero) ⋆ refl
max-eq₁ = λ v   → Coalg-morphism-Succ κ-max (Zero , Succ v) (Zero , v) refl
max-eq₂ = λ u   → Coalg-morphism-Succ κ-max (Succ u , Zero) (u , Zero) refl
max-eq₃ = λ u v → Coalg-morphism-Succ κ-max (Succ u , Succ v) (u , v) refl


Addition:


private
 κ-add : ℕ∞ × ℕ∞ → 𝟙 {𝓤₀} + ℕ∞ × ℕ∞
 κ-add (u , v) = 𝟚-Cases (positivity u)
                   (𝟚-Cases (positivity v)
                      (inl ⋆)
                      (inr (Zero , Pred v)))
                   (inr (Pred u , v))

add : ℕ∞ × ℕ∞ → ℕ∞
add = ℕ∞-corec κ-add

add-eq₀ :         add (Zero , Zero) ＝ Zero
add-eq₁ : ∀ v   → add (Zero , Succ v) ＝ Succ (add (Zero , v))
add-eq₂ : ∀ u v → add (Succ u , v) ＝ Succ (add (u , v))

add-eq₀ =         Coalg-morphism-Zero κ-add (Zero , Zero) ⋆ refl
add-eq₁ = λ v   → Coalg-morphism-Succ κ-add (Zero , Succ v) (Zero , v) refl
add-eq₂ = λ u v → Coalg-morphism-Succ κ-add (Succ u , v) (u , v) refl


We now prove properties of the minimum function using the
final-coalgebra property.

We already know that min (Zero , v) ＝ Zero, that is, Zero is
minimal. We next prove that ∞ is maximal, i.e., min (∞ , v) = v.

Using the equations min-eq₀ and min-eq₂, we have that the function
λ v → min (∞ , v) is an algebra homomorphism from PRED to PRED and
hence is equal to the identity function:



min-unit : ∀ v → min (∞ , v) ＝ v
min-unit v = ap (λ - → - v) h-is-corec
 where
  h : ℕ∞ → ℕ∞
  h v = min (∞ , v)
  h-homomorphism : is-homomorphism PRED h
  h-homomorphism = dfunext fe₀ (λ v → φ v (Zero+Succ fe₀ v))
   where
    φ : (v : ℕ∞) → (v ＝ Zero) + (Σ t ꞉ ℕ∞ , v ＝ Succ t) → PRED (h v) ＝ 𝟙+ h (PRED v)
    φ v (inl refl) =
      PRED (min (∞ , Zero))        ＝⟨ ap PRED (min-eq₀ ∞) ⟩
      PRED Zero                    ＝⟨refl⟩
      𝟙+ h (PRED Zero)             ∎
    φ v (inr (t , refl)) =
      PRED (min (∞ , Succ t)) ＝⟨ ap (λ - → PRED (min (- , Succ t))) (Succ-∞-is-∞ fe₀ ⁻¹) ⟩
      PRED (min (Succ ∞ , Succ t)) ＝⟨ ap PRED (min-eq₂ ∞ t) ⟩
      PRED (Succ (min (∞ , t)))    ＝⟨refl⟩
      𝟙+ h (PRED (Succ t))         ∎
  h-is-corec : h ＝ id
  h-is-corec = homomorphism-uniqueness PRED h id h-homomorphism id-homomorphism


Using the equations min-eq₀ and min-eq₂, we have that the function
λ u → min (u , u) is an algebra homomorphism from PRED to PRED and
hence is equal to the identity function:


min-idempotent : ∀ u → min (u , u) ＝ u
min-idempotent u = ap (λ - → - u) h-is-corec
 where
  h : ℕ∞ → ℕ∞
  h u = min (u , u)
  h-homomorphism : is-homomorphism PRED h
  h-homomorphism = dfunext fe₀ (λ u → φ (Zero+Succ fe₀ u))
   where
    φ : {u : ℕ∞} → (u ＝ Zero) + (Σ w ꞉ ℕ∞ , u ＝ Succ w) → PRED (h u) ＝ 𝟙+ h (PRED u)
    φ (inl refl) =
      PRED (min (Zero , Zero))     ＝⟨ ap PRED (min-eq₀ Zero) ⟩
      PRED Zero                    ＝⟨refl⟩
      𝟙+ h (PRED Zero)             ∎
    φ (inr (w , refl)) =
      PRED (min (Succ w , Succ w)) ＝⟨ ap PRED (min-eq₂ w w) ⟩
      PRED (Succ (min (w , w)))    ＝⟨refl⟩
      𝟙+ h (PRED (Succ w))         ∎
  h-is-corec : h ＝ id
  h-is-corec = homomorphism-uniqueness PRED h id h-homomorphism id-homomorphism


(Notice that the above argument actually shows that any function
f : ℕ∞ × ℕ∞ → ℕ∞ that satisfies f (Zero , Zero) ＝ Zero and
f (Succ w , Succ w) = Succ (f w) is idempotent, as it is the case of
the maximum function)

Similarly, to prove that min is commutative, we show that the function
λ (u , v) → min (v , u) satisfies the same "defining equations" as the
function min.

The following equation is derived from the above equations min-eq₀ and
min-eq₁ by cases on whether u is Zero or a Succ (Pred u).


eq₃-from-eq₀-and-eq₁ : (h : ℕ∞ × ℕ∞ → ℕ∞)
                     → (∀ v → h (Zero , v) ＝ Zero)
                     → (∀ u → h (Succ u , Zero) ＝ Zero)
                     → (∀ u → h (u , Zero) ＝ Zero)
eq₃-from-eq₀-and-eq₁ h eq₀ eq₁ u = γ (Zero+Succ fe₀ u)
 where
  γ : (u ＝ Zero) + (Σ w ꞉ ℕ∞ , u ＝ Succ w) → h (u , Zero) ＝ Zero
  γ (inl refl)       = h (Zero , Zero)   ＝⟨ eq₀ Zero ⟩ Zero ∎
  γ (inr (w , refl)) = h (Succ w , Zero) ＝⟨ eq₁ w ⟩    Zero ∎

min-eq₃ : ∀ u → min (u , Zero) ＝ Zero
min-eq₃ = eq₃-from-eq₀-and-eq₁ min min-eq₀ min-eq₁


Conversely, if a function satisfies the above equations, then it is a
coalgebra homomorphism and hence is equal to ℕ∞-corec κ-min.


min-equations-characterize-homomorphisms :
    (h : ℕ∞ × ℕ∞ → ℕ∞)
  → (∀ v   → h (Zero , v) ＝ Zero)
  → (∀ u   → h (Succ u , Zero) ＝ Zero)
  → (∀ u v → h (Succ u , Succ v) ＝ Succ (h (u , v)))
  → is-homomorphism κ-min h
min-equations-characterize-homomorphisms h eq₀ eq₁ eq₂ = dfunext fe₀ γ
  where
   γ : (w : ℕ∞ × ℕ∞) → PRED (h w) ＝ 𝟙+ h (κ-min w)
   γ (u , v) = φ (Zero+Succ fe₀ u) (Zero+Succ fe₀ v)
    where
     φ : (u ＝ Zero) + (Σ w ꞉ ℕ∞ , u ＝ Succ w)
       → (v ＝ Zero) + (Σ t ꞉ ℕ∞ , v ＝ Succ t)
       → PRED (h (u , v)) ＝ 𝟙+ h (κ-min (u , v))
     φ (inl refl) _  =
       PRED (h (Zero , v))            ＝⟨ ap PRED (eq₀ v) ⟩
       PRED Zero                      ＝⟨refl⟩
       𝟙+ h (κ-min (Zero , v))        ∎
     φ (inr (w , refl)) (inl refl) =
       PRED (h (Succ w , Zero))       ＝⟨ ap PRED (eq₁ w) ⟩
       PRED Zero                      ＝⟨refl⟩
       𝟙+ h (κ-min (Succ w , Zero))   ∎
     φ (inr (w , refl)) (inr (t , refl)) =
       PRED (h (Succ w , Succ t))     ＝⟨ ap PRED (eq₂ w t) ⟩
       PRED (Succ (h (w , t)))        ＝⟨refl⟩
       𝟙+ h (κ-min (Succ w , Succ t)) ∎


We can show that the min defined here is equivalent to that
given in GenericConvergentSequence:


min'-eq₀ : ∀ v → uncurry min' (Zero , v) ＝ Zero
min'-eq₀ v = ℕ∞-to-ℕ→𝟚-lc (fe 𝓤₀ 𝓤₀) refl

min'-eq₁ : ∀ u → uncurry min' (Succ u , Zero) ＝ Zero
min'-eq₁ u = ℕ∞-to-ℕ→𝟚-lc  (fe 𝓤₀ 𝓤₀)
             (dfunext (fe 𝓤₀ 𝓤₀) (λ i → Lemma[min𝟚ab＝₀] (inr refl)))

min'-eq₂ : ∀ u v → uncurry min' (Succ u , Succ v) ＝ Succ (uncurry min' (u , v))
min'-eq₂ u v = ℕ∞-to-ℕ→𝟚-lc (fe 𝓤₀ 𝓤₀) (dfunext (fe 𝓤₀ 𝓤₀) γ)
 where γ : pr₁ (uncurry min' (Succ u , Succ v)) ∼ pr₁ (Succ (uncurry min' (u , v)))
       γ zero = refl
       γ (succ i) = refl

min＝ : min ＝ uncurry min'
min＝ = homomorphism-uniqueness κ-min min (uncurry min')
       (ℕ∞-corec-homomorphism κ-min)
       (min-equations-characterize-homomorphisms
        (uncurry min') min'-eq₀ min'-eq₁ min'-eq₂)


To prove that min is commutative, we show that the following function
h is also a coalgebra homomorphism and hence equal to ℕ∞-corec p:


min-commutative : ∀ u v → min (u , v) ＝ min (v , u)
min-commutative u v = h (v , u)               ＝⟨ ap (λ - → - (v , u)) h-is-min ⟩
                      ℕ∞-corec κ-min (v , u) ∎
 where
  h : ℕ∞ × ℕ∞ → ℕ∞
  h (u , v) = min (v , u)
  h-homomorphism : is-homomorphism κ-min h
  h-homomorphism = min-equations-characterize-homomorphisms h h-eq₀ h-eq₁ h-eq₂
   where
    h-eq₀ : (v : ℕ∞) → min (v , Zero) ＝ Zero
    h-eq₀ v = min-eq₃ v
    h-eq₁ : (u : ℕ∞) → min (Zero , Succ u) ＝ Zero
    h-eq₁ u = min-eq₀ (Succ u)
    h-eq₂ : (u v : ℕ∞) → min (Succ v , Succ u) ＝ Succ (min (v , u))
    h-eq₂ u v = min-eq₂ v u
  h-is-min : h ＝ min
  h-is-min = homomorphism-uniqueness κ-min h (ℕ∞-corec κ-min)
              h-homomorphism (ℕ∞-corec-homomorphism κ-min)


Similarly, to prove that min is associative, we show that the two functions

   λ (u , v , w) → min (u , min (v , w))
   λ (u , v , w) → min (min (u , v) , w)

are homormorphisms from the same coalgebra on ℕ∞ × ℕ∞ × ℕ∞ to the
final coalgebra PRED.


min-associative : (u v w : ℕ∞) → min (u , min (v , w)) ＝ min (min (u , v) , w)
min-associative u v w = ap (λ - → - (u , v , w)) p
 where
  f g : ℕ∞ × ℕ∞ × ℕ∞ → ℕ∞
  f (u , v , w) = min (u , min (v , w))
  g (u , v , w) = min (min (u , v) , w)
  κ : ℕ∞ × ℕ∞ × ℕ∞ → 𝟙 + ℕ∞ × ℕ∞ × ℕ∞
  κ (u , v , w) = 𝟚-Cases (positivity u)
                   (inl ⋆)
                   (𝟚-Cases (positivity v)
                     (inl ⋆)
                     (𝟚-Cases (positivity w)
                       (inl ⋆)
                       (inr (Pred u , Pred v , Pred w))))
  f-homomorphism : is-homomorphism κ f
  f-homomorphism = dfunext fe₀ γ
   where
    γ : (z : ℕ∞ × ℕ∞ × ℕ∞) → PRED (f z) ＝ 𝟙+ f (κ z)
    γ (u , v , w) = φ (Zero+Succ fe₀ u) (Zero+Succ fe₀ v) (Zero+Succ fe₀ w)
     where
      φ : (u ＝ Zero) + (Σ x ꞉ ℕ∞ , u ＝ Succ x)
       → (v ＝ Zero) + (Σ y ꞉ ℕ∞ , v ＝ Succ y)
       → (w ＝ Zero) + (Σ z ꞉ ℕ∞ , w ＝ Succ z)
       → PRED (f (u , v , w)) ＝ 𝟙+ f (κ (u , v , w))
      φ (inl refl) _ _ = ap PRED (min-eq₀ (min (v , w)))
      φ (inr (x , refl)) (inl refl) _ =
        PRED (min (Succ x , min (Zero , w)))        ＝⟨ ap (λ - → PRED (min (Succ x , -))) (min-eq₀ w) ⟩
        PRED (min (Succ x , Zero))                  ＝⟨ ap PRED (min-eq₃ u) ⟩
        PRED Zero                                   ＝⟨ ap PRED (min-eq₃ u) ⟩
        𝟙+ f (κ (Succ x , Zero , w))                ∎
      φ (inr (x , refl)) (inr (y , refl)) (inl refl) =
        PRED (min (Succ x , min (Succ y , Zero)))   ＝⟨ ap (λ - → PRED (min (Succ x , -))) (min-eq₃ (Succ y)) ⟩
        PRED (min (Succ x , Zero))                  ＝⟨ ap PRED (min-eq₃ (Succ x)) ⟩
        𝟙+ f (κ (Succ x , Succ y , Zero))           ∎
      φ (inr (x , refl)) (inr (y , refl)) (inr (z , refl)) =
        PRED (min (Succ x , min (Succ y , Succ z))) ＝⟨ ap (λ - → PRED (min (Succ x , -))) (min-eq₂ y z) ⟩
        PRED (min (Succ x , Succ (min (y , z))))    ＝⟨ ap PRED (min-eq₂ x (min (y , z))) ⟩
        𝟙+ f (κ (Succ x , Succ y , Succ z))         ∎
  g-homomorphism : is-homomorphism κ g
  g-homomorphism = dfunext fe₀ γ
   where
    γ : (z : ℕ∞ × ℕ∞ × ℕ∞) → PRED (g z) ＝ 𝟙+ g (κ z)
    γ (u , v , w) = φ (Zero+Succ fe₀ u) (Zero+Succ fe₀ v) (Zero+Succ fe₀ w)
     where
      φ : (u ＝ Zero) + (Σ x ꞉ ℕ∞ , u ＝ Succ x)
       → (v ＝ Zero) + (Σ y ꞉ ℕ∞ , v ＝ Succ y)
       → (w ＝ Zero) + (Σ z ꞉ ℕ∞ , w ＝ Succ z)
       → PRED (g (u , v , w)) ＝ 𝟙+ g (κ (u , v , w))
      φ (inl refl) _ _ = ap PRED (min-eq₀ (min (v , w)))
      φ (inr (x , refl)) (inl refl) _ =
        PRED (min (min (Succ x , Zero) , w))        ＝⟨ ap (λ - → PRED (min (- , w))) (min-eq₃ (Succ x)) ⟩
        PRED (min (Zero , w))                       ＝⟨ ap PRED (min-eq₀ w) ⟩
        PRED Zero                                   ＝⟨refl⟩
        𝟙+ g (κ (Succ x , Zero , w))                ∎
      φ (inr (x , refl)) (inr (y , refl)) (inl refl) =
        PRED (min (min (Succ x , Succ y) , Zero))   ＝⟨ ap PRED (min-eq₃ (min (Succ x , Succ y))) ⟩
        PRED Zero                                   ＝⟨refl⟩
        𝟙+ g (κ (Succ x , Succ y , Zero))           ∎
      φ (inr (x , refl)) (inr (y , refl)) (inr (z , refl)) =
        PRED (min (min (Succ x , Succ y) , Succ z)) ＝⟨ ap (λ - → PRED (min (- , Succ z))) (min-eq₂ x y) ⟩
        PRED (min (Succ (min (x , y)) , Succ z))    ＝⟨ ap PRED (min-eq₂ (min (x , y)) z) ⟩
        PRED (Succ (min (min (x , y) , z)))         ＝⟨refl⟩
        𝟙+ g (κ (Succ x , Succ y , Succ z))         ∎
  p : f ＝ g
  p = homomorphism-uniqueness κ f g f-homomorphism g-homomorphism


Thus, ℕ∞ equipped with (min , Zero, ∞) is a bounded semilattice with
bottom Zero and top ∞.


min-is-bounded-semilattice :
   (∀ v     → min (Zero , v) ＝ Zero)
 × (∀ v     → min (∞ , v) ＝ v)
 × (∀ u     → min (u , u) ＝ u)
 × (∀ u v   → min (u , v) ＝ min (v , u))
 × (∀ u v w → min (u , min (v , w)) ＝ min (min (u , v) , w))
min-is-bounded-semilattice = min-eq₀ ,
                             min-unit ,
                             min-idempotent ,
                             min-commutative ,
                             min-associative


The following two facts invert the equations that characterize min:


min-Zero : ∀ u v   → min (u , v) ＝ Zero → (u ＝ Zero) + (v ＝ Zero)
min-Succ : ∀ u v x → min (u , v) ＝ Succ x → (u ＝ Succ (Pred u))
                                          × (v ＝ Succ (Pred v))
                                          × (x ＝ min (Pred u , Pred v))


And here are their constructions:


min-Zero u v r = h (Zero+Succ fe₀ u) (Zero+Succ fe₀ v)
 where
  h : (u ＝ Zero) + (Σ w ꞉ ℕ∞ , u ＝ Succ w) → (v ＝ Zero) + (Σ t ꞉ ℕ∞ , v ＝ Succ t)
    → (u ＝ Zero) + (v ＝ Zero)
  h (inl refl) _ = inl refl
  h (inr (w , refl)) (inl refl) = inr refl
  h (inr (w , refl)) (inr (t , refl)) = 𝟘-elim (Zero-not-Succ (r ⁻¹ ∙ min-eq₂ w t))

min-Succ u v x r = h (Zero+Succ fe₀ u) (Zero+Succ fe₀ v)
 where
  h : (u ＝ Zero) + (Σ w ꞉ ℕ∞ , u ＝ Succ w) → (v ＝ Zero) + (Σ t ꞉ ℕ∞ , v ＝ Succ t)
    → (u ＝ Succ (Pred u)) × (v ＝ Succ (Pred v)) × (x ＝ min (Pred u , Pred v))
  h (inl refl) _ =
    𝟘-elim (Zero-not-Succ (Zero           ＝⟨ (min-eq₀ v)⁻¹ ⟩
                           min (Zero , v) ＝⟨ r ⟩
                           Succ x         ∎))
  h (inr (w , refl)) (inl refl) =
    𝟘-elim (Zero-not-Succ (Zero           ＝⟨ (min-eq₃ u)⁻¹ ⟩
                           min (u , v)    ＝⟨ r ⟩
                           Succ x         ∎))
  h (inr (w , refl)) (inr (t , refl)) = refl , refl ,
    Succ-lc (Succ x                       ＝⟨ r ⁻¹ ⟩
             min (Succ w , Succ t)        ＝⟨ min-eq₂ w t ⟩
             Succ (min (w , t))           ∎)


Relation of min with ≼ defined in the module GenericConvergentSequence.


≼-min-l : (u v : ℕ∞) → min (u , v) ≼ u
≼-min-l u v zero p = γ
 where
  a : min (u , v) ＝ Succ (Pred (min (u , v)))
  a = positive-equal-Succ fe₀ (p ∶ zero ⊏ min (u , v))
  b : u ＝ Succ (Pred u)
  b = pr₁ (min-Succ u v (Pred (min (u , v))) a)
  γ : zero ⊏ u
  γ = ap (λ - → ι - zero) b
≼-min-l u v (succ n) p = γ
 where
  a : min (u , v) ＝ Succ (Pred (min (u , v)))
  a = positive-equal-Succ fe₀ (⊏-positive (succ n) (min (u , v)) p)
  b : (u ＝ Succ (Pred u))
    × (v ＝ Succ (Pred v))
    × (Pred (min (u , v)) ＝ min (Pred u , Pred v))
  b = min-Succ u v (Pred (min (u , v))) a
  q : n ⊏ Pred (min (u , v))
  q = p ∶ succ n ⊏ min (u , v)
  r : n ⊏ min (Pred u , Pred v)
  r = transport (λ - → n ⊏ -) (pr₂ (pr₂ b)) q
  IH : n ⊏ Pred u
  IH = ≼-min-l (Pred u) (Pred v) n r
  γ : succ n ⊏ u
  γ = IH

≼-min-r : (u v : ℕ∞) → min (u , v) ≼ v
≼-min-r u v n p = ≼-min-l v u n q
 where
  q : n ⊏ min (v , u)
  q = transport (λ - → n ⊏ -) (min-commutative u v) p

≼-from-min→ : (u v : ℕ∞) → min (u , v) ＝ u → u ≼ v
≼-from-min→ u v p = transport (λ - → - ≼ v) p (≼-min-r u v)