-- Advanced Functional Programming course 2016 Chalmers/GU
--
-- 2016-02-25 Guest lecture by Andreas Abel
--
-- Introduction to Agda
--
-- File 3: insertion sort preserves length, proved using equality chains

module LengthIsortChain where

open import InsertionSortBool
open import Relation.Binary.PropositionalEquality

-- ≡-Reasoning gives us a defined (!) notation to write equality chains.

open ≡-Reasoning

-- Lemma: insertion increases the length of a list by one.
-- Proof by induction on ys.

length-insert : ∀ x ys → length (insert x ys) ≡ suc (length ys)

-- Case: empty list
length-insert x [] = refl

-- Case: cons list (y ∷ ys)
length-insert x (y ∷ ys) with x <= y

-- Subcase: x <= y is true
... | true  = begin

  length (x ∷ y ∷ ys)   ≡⟨⟩
  suc (length (y ∷ ys))
  ∎

-- Subcase: x <= y is false
... | false = begin

  length (y ∷ insert x ys)     ≡⟨ refl ⟩
  suc (length (insert x ys))   ≡⟨ cong suc (length-insert x ys) ⟩
  suc (suc (length ys))        ≡⟨ refl ⟩
  suc (length (y ∷ ys))
  ∎


-- Theorem: sorting preserves the length
-- By induction on the xs.

length-isort : ∀ xs → length (isort xs) ≡ length xs

-- Case: empty list
length-isort [] = begin
  length (isort [])  ≡⟨⟩
  length {A = ℕ} []  ≡⟨⟩
  zero               ≡⟨⟩
  length {A = ℕ} []
  ∎

-- Case: cons list (y ∷ ys)
length-isort (x ∷ xs) = begin
  length (isort (x ∷ xs))       ≡⟨⟩
  length (insert x (isort xs))  ≡⟨ length-insert _ _ ⟩
  suc (length (isort xs))       ≡⟨ cong suc (length-isort xs) ⟩
  suc (length xs)               ≡⟨⟩
  length (x ∷ xs)
  ∎