module l19 where
{-
Computer Aided Formal Reasoning (G53CFR, G54CFR)
Peter Morris
Lecture 19: Merge Sort (IV)
As a final trick with our Merge Sort algorithm, we will show that the output
of the sort function is a _sorted_ list. To do this we must first define what
it is to be a sorted list. For clarity we shall lose the size indicies, though
it's straight forward to combine the two proofs and show the output to be
sorted, and of the right size:
-}
open import Data.List
open import Data.Nat hiding (_≤_ ; _<_)
open import Data.Product
{-
The first change is that we will now want proofs of the ordering between the
numbers we are sorting. So let's bring back the inductive definition of _≤_
you've used before, and the proof that it is transitive:
-}
data _≤_ : ℕ → ℕ → Set where
z≤n : ∀ {n} → zero ≤ n
s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n
trans≤ : ∀ {m n o} → m ≤ n → n ≤ o → m ≤ o
trans≤ z≤n q = z≤n
trans≤ (s≤s m≤n) (s≤s n≤o) = s≤s (trans≤ m≤n n≤o)
{-
We will also want _<_ and a proof that if m < n the m ≤ n:
-}
_<_ : ℕ → ℕ → Set
m < n = suc m ≤ n