Prove alpha equivalence preserves free variables.

1 files changed, 68 insertions, 0 deletions

diff --git a/src/Data/List/Properties/Ext.agda b/src/Data/List/Properties/Ext.agda
new file mode 100644
index 0000000..b27aeb4
--- /dev/null
+++ b/src/Data/List/Properties/Ext.agda
@@ -0,0 +1,68 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.List.Properties.Ext where
+
+open import Data.Bool using (Bool)
+open import Data.Empty using (⊥-elim)
+open import Data.List
+open import Data.List.Membership.Propositional using (_∈_)
+open import Data.List.Relation.Unary.Any using (Any)
+open import Data.Product using (Σ)
+open import Function using (Equivalence; _⇔_; _∘_)
+open import Level using (Level)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≗_; cong; cong₂)
+open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Unary using (Pred; Decidable; _≐_)
+
+private
+  variable
+    a p : Level
+    A B : Set a
+
+open Any
+open Bool
+open Dec
+open Equivalence
+open _≡_
+open Σ
+
+-- Properties of filter -------------------------------------------------------
+
+module _ {P : Pred A p} (P? : Decidable P) where
+  filter-cong :
+    ∀ {Q : Pred A a} (Q? : Decidable Q) → P ≐ Q → filter P? ≗ filter Q?
+  filter-cong Q? P≐Q [] = refl
+  filter-cong Q? P≐Q (x ∷ xs) with P? x | Q? x
+  ... | yes Px | yes Qx = cong (x ∷_) (filter-cong Q? P≐Q xs)
+  ... | yes Px | no ¬Qx = ⊥-elim (¬Qx (P≐Q .proj₁ Px))
+  ... | no ¬Px | yes Qx = ⊥-elim (¬Px (P≐Q .proj₂ Qx))
+  ... | no ¬Px | no ¬Qx = filter-cong Q? P≐Q xs
+
+  filter-map :
+    ∀ (f : B → A) xs →
+    filter P? (map f xs) ≡ map f (filter (P? ∘ f) xs)
+  filter-map f []       = refl
+  filter-map f (x ∷ xs) with does (P? (f x))
+  ... | true  = cong (f x ∷_) (filter-map f xs)
+  ... | false = filter-map f xs
+
+  map-filter-cong :
+    ∀ {f g : A → B} → (f≗g : ∀ {x} → P x → f x ≡ g x) →
+    map f ∘ filter P? ≗ map g ∘ filter P?
+  map-filter-cong f≗g []       = refl
+  map-filter-cong f≗g (x ∷ xs) with P? x
+  ... | yes Px = cong₂ _∷_ (f≗g Px) (map-filter-cong f≗g xs)
+  ... | no ¬Px = map-filter-cong f≗g xs
+
+  filter-map-comm :
+    ∀ {Q : Pred B a} (Q? : Decidable Q) {f g : B → A} xs →
+    (∀ {x} → x ∈ xs → P (f x) ⇔ Q x) →
+    (∀ {x} → Q x → f x ≡ g x) →
+    filter P? (map f xs) ≡ map g (filter Q? xs)
+  filter-map-comm Q?     []       P⇔Q f≗g = refl
+  filter-map-comm Q? {f} (x ∷ xs) P⇔Q f≗g with P? (f x) | Q? x
+  ... | yes Pfx | yes Qx =
+    cong₂ _∷_ (f≗g Qx) (filter-map-comm Q? xs (P⇔Q ∘ there) f≗g)
+  ... | yes Pfx | no ¬Qx = ⊥-elim (¬Qx (P⇔Q (here refl) .to Pfx))
+  ... | no ¬Pfx | yes Qx = ⊥-elim (¬Pfx (P⇔Q (here refl) .from Qx))
+  ... | no ¬Pfx | no ¬Qx = filter-map-comm Q? xs (P⇔Q ∘ there) f≗g