```
{-# 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

```
≤-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 = {!!}
```

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

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

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


## Exercise: Decision procedures

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

::: Hint :::
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.
:::

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

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

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


## 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 = {!!}
```

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

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


## 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

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

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

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

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


## Exercise: Indexing

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