From 2cf0f3d2583029bba9c2bb0a97b9185d7b47bdbe Mon Sep 17 00:00:00 2001
From: Heinrich Apfelmus <apfelmus@quantentunnel.de>
Date: Fri, 24 Jan 2025 17:58:16 +0100
Subject: [PATCH] Prove properties about `delete` and `nub`

---
 lib/Haskell/Data/List.agda | 63 ++++++++++++++++++++++++++++++++++++++
 1 file changed, 63 insertions(+)

diff --git a/lib/Haskell/Data/List.agda b/lib/Haskell/Data/List.agda
index 0e2094f1..6ce57adf 100644
--- a/lib/Haskell/Data/List.agda
+++ b/lib/Haskell/Data/List.agda
@@ -38,3 +38,66 @@ 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 recurse ← prop-elem-delete x y zs
+  with y == z in eqyz
+... | True
+    with x == z in eqxz
+...   | True
+      rewrite equality' _ _ (trans (equality x z eqxz) (sym (equality y z eqyz)))
+      = recurse
+...   | False
+      = recurse
+prop-elem-delete x y (z ∷ zs)
+    | False
+    with x == z in eqxz
+...   | True
+      rewrite (lemma-neq-trans x y z eqxz eqyz)
+      = refl
+...   | False
+      = 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