module SList where -- natural numbers data Nat : Set where zero : Nat suc : Nat -> Nat infix 2 _+_ infix 3 _*_ _+_ : Nat -> Nat -> Nat n + zero = n n + suc m = suc (n + m) _*_ : Nat -> Nat -> Nat n * zero = zero n * (suc m) = n * m + n one = suc zero two = suc one -- booleans and comparison data Bool : Set where true : Bool false : Bool _≤_ : Nat -> Nat -> Bool zero ≤ n = true (suc m) ≤ zero = false (suc m) ≤ (suc n) = m ≤ n -- logic Proposition = Set data Truth : Proposition where tt : Truth data Absurd : Proposition where True : Bool -> Proposition True true = Truth True false = Absurd -- sorted lists data SList : Nat -> Set where snil : SList zero scons : {n : Nat}(m : Nat) -> True (n ≤ m) -> SList n -> SList m slist1 = scons one tt (scons zero tt snil) {- Exercise 2: insert for SList -} open import Relation.Binary.PropositionalEquality -- inspect -- making use of inequality proofs mkTrue : {b : Bool} -> b ≡ true -> True b mkTrue refl = tt le≡false : {n m : Nat} -> n ≤ m ≡ false -> True (m ≤ n) le≡false {n} {zero} p = tt le≡false {zero} {suc m} () le≡false {suc n} {suc m} p = le≡false {n} {m} p -- maximum max : Nat -> Nat -> Nat max n m with n ≤ m ... | true = m ... | false = n maxLemma : {n m k : Nat} -> True (n ≤ k) -> True (m ≤ k) -> True (max n m ≤ k) maxLemma {n} {m} p q with n ≤ m ... | true = q ... | false = p -- insertion into sorted lists -- to make "inspect" work with "magic with", we use Josh Ko's pattern insert : {n : Nat}(m : Nat) -> SList n -> SList (max n m) insert m snil = scons m tt snil insert m (scons n p l) with inspect (n ≤ m) -- inspect needed to have a (dis)proof of n ≤ m insert m (scons n p l) | b with-≡ b≡n≤m with (n ≤ m) | b≡n≤m insert m (scons n p l) | .(n ≤ m) with-≡ refl | true | n≤m≡true = scons m (mkTrue n≤m≡true) (scons n p l) insert m (scons n p l) | .(n ≤ m) with-≡ refl | false | n≤m≡false = scons n (maxLemma p (le≡false n≤m≡false)) (insert m l)