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  _≤_ _<_ _≥_ _>_
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

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

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

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

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

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

Exercise: Decision procedures

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

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

Exercise: Ordering properties of several functions

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

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

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

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

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

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

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

Exercise: Halving

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

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

Exercise: Subtraction decreases

open import Padova2025.ProvingBasics.EvenOdd

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

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

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.

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

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.

ℕ-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)    = {!!}

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

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

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

<⇒<' : {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)

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

Exercise: Indexing

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