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