Prove properties about delete and nub

Author: HeinrichApfelmus

lib/Haskell/Data/List.agda

@@ -1,8 +1,12 @@
 module Haskell.Data.List where
 
 open import Haskell.Prelude
+
 open import Haskell.Data.Ord using (comparing)
 
+open import Haskell.Law.Eq
+open import Haskell.Law.Equality
+
 {-----------------------------------------------------------------------------
     Operations
 ------------------------------------------------------------------------------}
@@ -40,3 +44,67 @@ sortOn f =
     map snd
     ∘ sortBy (comparing fst)
     ∘ map (λ x → let y = f x in seq y (y , x))
+
+{-----------------------------------------------------------------------------
+    Properties
+------------------------------------------------------------------------------}
+--
+lemma-neq-trans
+  : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄
+      (x y z : a)
+  → (x == z) ≡ True
+  → (y == z) ≡ False
+  → (x == y) ≡ False
+--
+lemma-neq-trans x y z eqxz
+  rewrite equality x z eqxz
+  rewrite eqSymmetry y z
+  = λ x → x
+
+-- | A deleted item is no longer an element.
+--
+prop-elem-delete
+  : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄
+      (x y : a) (zs : List a)
+  → elem x (delete y zs)
+    ≡ (if x == y then False else elem x zs)
+--
+prop-elem-delete x y []
+  with x == y
+... | False = refl
+... | True  = refl
+prop-elem-delete x y (z ∷ zs)
+  with y == z in eqyz
+... | True
+    with x == z in eqxz
+    with prop-elem-delete x y zs
+...   | True  | recurse
+      rewrite equality' _ _ (trans (equality x z eqxz) (sym (equality y z eqyz)))
+      = recurse
+...   | False | recurse
+      = recurse
+prop-elem-delete x y (z ∷ zs)
+    | False
+    with x == z in eqxz
+    with prop-elem-delete x y zs
+...   | True  | recurse
+      rewrite (lemma-neq-trans x y z eqxz eqyz)
+      = refl
+...   | False | recurse
+      = recurse
+
+-- | An item is an element of the 'nub' iff it is
+-- an element of the original list.
+--
+prop-elem-nub
+  : ∀ ⦃ _ : Eq a ⦄ ⦃ _ : IsLawfulEq a ⦄
+      (x : a) (ys : List a)
+  → elem x (nub ys)
+    ≡ elem x ys
+--
+prop-elem-nub x [] = refl
+prop-elem-nub x (y ∷ ys)
+  rewrite prop-elem-delete x y (nub ys)
+  with x == y
+... | True = refl
+... | False = prop-elem-nub x ys