{-# OPTIONS --cubical-compatible #-}
module Padova2025.ProvingBasics.Termination.Ordering where

The standard ordering on the natural numbers#

open import Padova2025.ProgrammingBasics.Naturals.Base
open import Padova2025.ProgrammingBasics.Naturals.Arithmetic
open import Padova2025.ProgrammingBasics.Lists
open import Padova2025.ProvingBasics.Negation
open import Padova2025.ProvingBasics.Connectives.Disjunction
open import Padova2025.ProvingBasics.Connectives.More
open import Padova2025.ProvingBasics.Equality.Base
open import Padova2025.ProvingBasics.Equality.General
open import Padova2025.ProvingBasics.Equality.NaturalNumbers

In this module, we introduce the standard ordering _≤_ on the natural numbers, together with its variants _<_, _≥_ and _>_, and verify their basic properties.

infix 4 _≤_ _<_ _≥_ _>_
data _≤_ : ℕ → ℕ → Set where
  z≤n : {n : ℕ}   → zero ≤ n
  s≤s : {n m : ℕ} → (n≤m : n ≤ m) → succ n ≤ succ m

_<_ : ℕ → ℕ → Set
n < m = succ n ≤ m

_>_ : ℕ → ℕ → Set
n > m = m < n

_≥_ : ℕ → ℕ → Set
n ≥ m = m ≤ n

Exercise: Reflexivity, transitivity and antisymmetry#

Exercise 1≤-refl

≤-refl : {a : ℕ} → a ≤ a
≤-refl = {!!}

The reference solution uses: zero z≤n succ s≤s

Your solution

Reference solution

≤-refl : {a : ℕ} → a ≤ a
≤-refl {zero}   = z≤n
≤-refl {succ a} = s≤s ≤-refl

Exercise 2≤-trans

≤-trans : {a b c : ℕ} → a ≤ b → b ≤ c → a ≤ c
≤-trans = {!!}

The reference solution uses: z≤n s≤s

Your solution

Reference solution

≤-trans : {a b c : ℕ} → a ≤ b → b ≤ c → a ≤ c
≤-trans z≤n     q       = z≤n
≤-trans (s≤s p) (s≤s q) = s≤s (≤-trans p q)

Exercise 3≤-antisymm

≤-antisymm : {a b : ℕ} → a ≤ b → b ≤ a → a ≡ b
≤-antisymm = {!!}

The reference solution uses: z≤n refl s≤s cong succ

Your solution

Reference solution

≤-antisymm : {a b : ℕ} → a ≤ b → b ≤ a → a ≡ b
≤-antisymm z≤n     z≤n     = refl
≤-antisymm (s≤s p) (s≤s q) = cong succ (≤-antisymm p q)

Exercise 4<-irreflexive

<-irreflexive : {a : ℕ} → a < a → ⊥
<-irreflexive = {!!}

The reference solution uses: s≤s

Your solution

Reference solution

<-irreflexive : {a : ℕ} → a < a → ⊥
<-irreflexive (s≤s p) = <-irreflexive p

Exercise 5<-irreflexive'

<-irreflexive' : {a b : ℕ} → a ≤ b → b < a → ⊥
<-irreflexive' = {!!}

The reference solution uses: s≤s

Your solution

Reference solution

<-irreflexive' : {a b : ℕ} → a ≤ b → b < a → ⊥
<-irreflexive' (s≤s p) (s≤s q) = <-irreflexive' p q

Exercise 6<-irreflexive''

<-irreflexive'' : {a b : ℕ} → a < b → b < a → ⊥
<-irreflexive'' = {!!}

The reference solution uses: s≤s

Your solution

Reference solution

<-irreflexive'' : {a b : ℕ} → a < b → b < a → ⊥
<-irreflexive'' (s≤s p) (s≤s q) = <-irreflexive'' p q

Exercise 7≡⇒≤

≡⇒≤ : {a b : ℕ} → a ≡ b → a ≤ b
≡⇒≤ = {!!}

The reference solution uses: refl ≤-refl

Your solution

Reference solution

≡⇒≤ : {a b : ℕ} → a ≡ b → a ≤ b
≡⇒≤ refl = ≤-refl

Exercise: Decision procedures#

Exercise 8≤-<-connex

≤-<-connex : (a b : ℕ) → a ≤ b ⊎ b < a
≤-<-connex = {!!}

The reference solution uses: zero left z≤n succ right s≤s

Your solution

Reference solution

≤-<-connex : (a b : ℕ) → a ≤ b ⊎ b < a
≤-<-connex zero     b        = left z≤n
≤-<-connex (succ a) zero     = right (s≤s z≤n)
≤-<-connex (succ a) (succ b) with ≤-<-connex a b
... | left  a≤b = left  (s≤s a≤b)
... | right b<a = right (s≤s b<a)

Perhaps surprisingly, this exercise and the next exercise can both be solved on autopilot. Judiciously use C-c C-c, C-c C-a and the with keyword to pattern match on the result of a suitable recursive call.

Exercise 9<-cmp

<-cmp : (a b : ℕ) → a ≡ b ⊎ (a < b ⊎ a > b)
<-cmp = {!!}

The reference solution uses: zero left refl succ right s≤s z≤n cong

Your solution

Reference solution

<-cmp : (a b : ℕ) → a ≡ b ⊎ (a < b ⊎ a > b)
<-cmp zero     zero     = left refl
<-cmp zero     (succ b) = right (left (s≤s z≤n))
<-cmp (succ a) zero     = right (right (s≤s z≤n))
<-cmp (succ a) (succ b) with <-cmp a b
... | left  a≡b         = left (cong succ a≡b)
... | right (left a<b)  = right (left (s≤s a<b))
... | right (right a>b) = right (right (s≤s a>b))

Exercise 10dec-≤

dec-≤ : (a b : ℕ) → Dec (a ≤ b)
dec-≤ = {!!}

The reference solution uses: zero yes z≤n succ no s≤s

Your solution

Reference solution

dec-≤ : (a b : ℕ) → Dec (a ≤ b)
dec-≤ zero     b = yes z≤n
dec-≤ (succ a) zero = no λ ()
dec-≤ (succ a) (succ b) with dec-≤ a b
... | yes a≤b  = yes (s≤s a≤b)
... | no  ¬a≤b = no λ { (s≤s a≤b) → ¬a≤b a≤b }

Exercise 11dec-<

dec-< : (a b : ℕ) → Dec (a < b)
dec-< = {!!}

The reference solution uses: dec-≤ succ

Your solution

Reference solution

dec-< : (a b : ℕ) → Dec (a < b)
dec-< a b = dec-≤ (succ a) b

Exercise: Ordering properties of several functions#

succ-monotone : {a b : ℕ} → a ≤ b → succ a ≤ succ b
succ-monotone = s≤s

Exercise 12pred-monotone

pred-monotone : {a b : ℕ} → a ≤ b → pred a ≤ pred b
pred-monotone = {!!}

The reference solution uses: z≤n s≤s

Your solution

Reference solution

pred-monotone : {a b : ℕ} → a ≤ b → pred a ≤ pred b
pred-monotone z≤n     = z≤n
pred-monotone (s≤s p) = p

Exercise 13succ-inflationary

succ-inflationary : (a : ℕ) → a ≤ succ a
succ-inflationary = {!!}

The reference solution uses: zero z≤n s≤s

Your solution

Reference solution

succ-inflationary : (a : ℕ) → a ≤ succ a
succ-inflationary zero     = z≤n
succ-inflationary (succ a) = s≤s (succ-inflationary a)

Exercise 14twice-inflationary

twice-inflationary : (a : ℕ) → a ≤ twice a
twice-inflationary = {!!}

The reference solution uses: zero z≤n succ ≤-trans succ-inflationary succ-monotone

Your solution

Reference solution

twice-inflationary : (a : ℕ) → a ≤ twice a
twice-inflationary zero     = z≤n
twice-inflationary (succ a) = ≤-trans (succ-inflationary (succ a)) (succ-monotone (succ-monotone (twice-inflationary a)))

Exercise 15max-inflationaryₗ

max-inflationaryₗ : (a b : ℕ) → a ≤ max a b
max-inflationaryₗ = {!!}

The reference solution uses: zero z≤n succ ≤-refl s≤s

Your solution

Reference solution

max-inflationaryₗ : (a b : ℕ) → a ≤ max a b
max-inflationaryₗ zero     b        = z≤n
max-inflationaryₗ (succ a) zero     = ≤-refl
max-inflationaryₗ (succ a) (succ b) = s≤s (max-inflationaryₗ a b)

Exercise 16max-inflationaryᵣ

max-inflationaryᵣ : (a b : ℕ) → b ≤ max a b
max-inflationaryᵣ = {!!}

The reference solution uses: zero ≤-refl succ z≤n s≤s

Your solution

Reference solution

max-inflationaryᵣ : (a b : ℕ) → b ≤ max a b
max-inflationaryᵣ zero     b        = ≤-refl
max-inflationaryᵣ (succ a) zero     = z≤n
max-inflationaryᵣ (succ a) (succ b) = s≤s (max-inflationaryᵣ a b)

Exercise 17+-monotone

+-monotone : {a a' b b' : ℕ} → a ≤ b → a' ≤ b' → a + a' ≤ b + b'
+-monotone = {!!}

The reference solution uses: z≤n s≤s ≤-trans succ-monotone ≡⇒≤ sym +-succ

Your solution

Reference solution

+-monotone : {a a' b b' : ℕ} → a ≤ b → a' ≤ b' → a + a' ≤ b + b'
+-monotone z≤n     z≤n     = z≤n
+-monotone z≤n     (s≤s q) = ≤-trans (succ-monotone (+-monotone z≤n q)) (≡⇒≤ (sym (+-succ _ _)))
+-monotone (s≤s p) q       = succ-monotone (+-monotone p q)

Exercise 18+-inflationaryₗ

+-inflationaryₗ : (a b : ℕ) → a ≤ a + b
+-inflationaryₗ = {!!}

The reference solution uses: zero z≤n succ s≤s

Your solution

Reference solution

+-inflationaryₗ : (a b : ℕ) → a ≤ a + b
+-inflationaryₗ zero     b = z≤n
+-inflationaryₗ (succ a) b = s≤s (+-inflationaryₗ a b)

Exercise 19+-inflationaryᵣ

+-inflationaryᵣ : (a b : ℕ) → b ≤ a + b
+-inflationaryᵣ = {!!}

The reference solution uses: +-monotone zero z≤n ≤-refl

Your solution

Reference solution

+-inflationaryᵣ : (a b : ℕ) → b ≤ a + b
+-inflationaryᵣ a b = +-monotone {zero} {b} {a} {b} z≤n ≤-refl

Exercise: Maximum of a list#

maximum : List ℕ → ℕ
maximum []       = zero
maximum (x ∷ xs) = max x (maximum xs)

maximum-≥ : (k : ℕ) (xs : List ℕ) → k ∈ xs → k ≤ maximum xs
maximum-≥ k (x ∷ xs) (here  refl) = max-inflationaryₗ x (maximum xs)
maximum-≥ k (x ∷ xs) (there p)    = ≤-trans (maximum-≥ k xs p) (max-inflationaryᵣ x (maximum xs))

Exercise: Halving#

Exercise 20half-≤

half-≤ : (x : ℕ) → half x ≤ x
half-≤ = {!!}

The reference solution uses: zero z≤n succ succ-monotone ≤-trans succ-inflationary

Your solution

Reference solution

half-≤ : (x : ℕ) → half x ≤ x
half-≤ zero            = z≤n
half-≤ (succ zero)     = z≤n
half-≤ (succ (succ x)) = succ-monotone (≤-trans (half-≤ x) (succ-inflationary x))

Exercise 21half-<

half-< : (x : ℕ) → half (succ x) < succ x
half-< = {!!}

The reference solution uses: zero s≤s z≤n succ-monotone half-≤

Your solution

Reference solution

half-< : (x : ℕ) → half (succ x) < succ x
half-< zero     = s≤s z≤n
half-< (succ x) = succ-monotone (succ-monotone (half-≤ x))

Exercise: Subtraction decreases#

open import Padova2025.ProvingBasics.EvenOdd

Exercise 22monus-≤

monus-≤ : (a b : ℕ) → a ≥ b → a ∸ b ≤ a
monus-≤ = {!!}

The reference solution uses: zero z≤n ≤-refl succ s≤s ≤-trans succ-inflationary

Your solution

Reference solution

monus-≤ : (a b : ℕ) → a ≥ b → a ∸ b ≤ a
monus-≤ a        zero     z≤n       = ≤-refl
monus-≤ (succ a) (succ b) (s≤s a≥b) = ≤-trans (monus-≤ a b a≥b) (succ-inflationary a)

Exercise 23monus-<

monus-< : (a b : ℕ) → IsPositive b → a ≥ b → a ∸ b < a
monus-< = {!!}

The reference solution uses: succ zero s≤s ≤-refl ≤-trans case-succ succ-inflationary

Your solution

Reference solution

monus-< : (a b : ℕ) → IsPositive b → a ≥ b → a ∸ b < a
monus-< (succ a) (succ zero)     b≥0  (s≤s a≥b) = ≤-refl
monus-< (succ a) (succ (succ b)) b≥-1 (s≤s a>b) =
  ≤-trans (monus-< a (succ b) (case-succ b) a>b) (succ-inflationary a)

Infinitude of the even numbers#

open import Padova2025.ProvingBasics.Connectives.Existential
open import Padova2025.ProvingBasics.Connectives.Conjunction
open import Padova2025.ProvingBasics.EvenOdd
open import Padova2025.ProvingBasics.Equality.NaturalNumbers

A particularly positive way of expressing that there are infinitely many even numbers is as follows: Beyond every natural number, there is an even natural number. Let us state and prove this fact in Agda.

Exercise 24Even-infinite

Even-infinite : (x : ℕ) → ∃[ y ] (y ≥ x × Even y)
Even-infinite = {!!}

The reference solution uses: twice _,_ twice-inflationary twice-even

Your solution

Reference solution

Even-infinite : (x : ℕ) → ∃[ y ] (y ≥ x × Even y)
Even-infinite x = twice x , twice-inflationary x , twice-even x
-- Alternatively, more economically, providing `x` or `succ x` instead
-- of `twice x` as witness:
-- Even-infinite x with even-or-odd x
-- ... | left  xeven = x      , ≤-refl              , xeven
-- ... | right xodd  = succ x , succ-inflationary x , succ-odd xodd

Infinitude of the natural numbers#

open import Padova2025.ProvingBasics.Connectives.Existential

One among several ways to express that there are infinitely many natural numbers is as follows: For every finite list of natural numbers, there is a natural number not in that list. We can formalize and prove this assertion as follows.

Exercise 25ℕ-infinite

ℕ-infinite : (xs : List ℕ) → ∃[ x ] x ∉ xs
ℕ-infinite xs = succ (sum xs) , λ p → <-irreflexive (go p)
  where
  go : {xs : List ℕ} {y : ℕ} → y ∈ xs → y < succ (sum xs)
  go (here  refl) = {!!}
  go (there p)    = {!!}

The reference solution uses: succ-monotone ≤-trans ≡⇒≤ sym +-zero +-monotone ≤-refl z≤n

Your solution

Reference solution

ℕ-infinite : (xs : List ℕ) → ∃[ x ] x ∉ xs
ℕ-infinite xs = succ (sum xs) , λ p → <-irreflexive (go p)
  where
  go : {xs : List ℕ} {y : ℕ} → y ∈ xs → y < succ (sum xs)
  go (here  refl) = succ-monotone (≤-trans (≡⇒≤ (sym (+-zero _))) (+-monotone ≤-refl z≤n))
  go (there p)    = ≤-trans (go p) (succ-monotone (+-monotone z≤n ≤-refl))

Exercise: An alternative definition of the strict ordering relation#

Occasionally the following alternative definition of the strict less-than relation is useful.

data _<'_ : ℕ → ℕ → Set where
  base' : {n : ℕ}     → n <' succ n
  step' : {a b : ℕ}   → a <' b → a <' succ b

Exercise 26z<'s

z<'s : {x : ℕ} → zero <' succ x
z<'s = {!!}

The reference solution uses: base' step'

Your solution

Reference solution

z<'s : {x : ℕ} → zero <' succ x
z<'s {zero}   = base'
z<'s {succ x} = step' z<'s

Exercise 27s<'s

s<'s : {x y : ℕ} → x <' y → succ x <' succ y
s<'s = {!!}

The reference solution uses: base' step'

Your solution

Reference solution

s<'s : {x y : ℕ} → x <' y → succ x <' succ y
s<'s base'     = base'
s<'s (step' p) = step' (s<'s p)

Exercise 28<⇒<'

<⇒<' : {x y : ℕ} → x < y → x <' y
<⇒<' = {!!}

The reference solution uses: s≤s _≤_ succ z≤n z<'s s<'s

Your solution

Reference solution

<⇒<' : {x y : ℕ} → x < y → x <' y
<⇒<' (s≤s p) = lemma p
  where
  lemma : {x y : ℕ} → x ≤ y → x <' succ y
  lemma z≤n     = z<'s
  lemma (s≤s p) = s<'s (lemma p)

Exercise 29<'⇒<

<'⇒< : {x y : ℕ} → x <' y → x < y
<'⇒< = {!!}

The reference solution uses: base' ≤-refl step' ≤-trans succ-inflationary

Your solution

Reference solution

<'⇒< : {x y : ℕ} → x <' y → x < y
<'⇒< base'     = ≤-refl
<'⇒< (step' p) = ≤-trans (<'⇒< p) (succ-inflationary _)

Exercise: Indexing#

Exercise 30lookup

lookup : {P : ℕ → Set} {n m : ℕ} → All P (downFrom n) → m < n → P m
lookup = {!!}

The reference solution uses: succ _∷_ ≤-<-connex left subst ≤-antisymm pred-monotone right

Your solution

Reference solution

lookup : {P : ℕ → Set} {n m : ℕ} → All P (downFrom n) → m < n → P m
lookup {P} {succ n} {m} (p ∷ ps) m<n with ≤-<-connex n m
... | left  n≤m = subst P (≤-antisymm n≤m (pred-monotone m<n)) p
... | right m<n = lookup ps m<n