Prove alpha equivalence preserves free variables.

5 files changed, 320 insertions, 5 deletions

diff --git a/Everything.agda b/Everything.agda
index a2b808f..96119c6 100644
--- a/Everything.agda
+++ b/Everything.agda
@@ -2,4 +2,7 @@
 module Everything where
 
 import Data.BinOp
+import Data.List.Properties.Ext
 import Data.Type
+import Data.Type.Properties
+import Data.Util
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
diff --git a/src/Data/Type.agda b/src/Data/Type.agda
index 9773db0..0027b27 100644
--- a/src/Data/Type.agda
+++ b/src/Data/Type.agda
@@ -74,14 +74,14 @@ private
 
 applyRenaming : List Renaming → ℕ → ℕ
 applyRenaming ρs α =
-  foldl (λ α (from , to) → if isYes (α ≟ from) then to else α) α ρs
+  foldl (λ α (from , to) → if isYes (from ≟ α) then to else α) α ρs
 
 rename : List Renaming → Type → Type
 rename ρs (var α)     = var (applyRenaming ρs α)
 rename ρs unit        = unit
 rename ρs (bin ⊗ A B) = bin ⊗ (rename ρs A) (rename ρs B)
 rename ρs (all α A)   =
-  let β = mkFresh (map (applyRenaming ρs) (free A)) in
+  let β = mkFresh (free (all α A) ++ map from ρs ++ map to ρs) in
   all β (rename ((α , β) ∷ ρs) A)
 
 -- Alpha Equivalence ----------------------------------------------------------
@@ -91,8 +91,8 @@ data _≈_ : Type → Type → Set where
   unit : unit ≈ unit
   bin  : A ≈ C → B ≈ D → bin ⊗ A B ≈ bin ⊗ C D
   all  :
-    (∀ γ → γ ∉ free (all α A) → γ ∉ free (all β B) →
-     rename ((γ , α) ∷ []) A ≈ rename ((γ , β) ∷ []) B) →
+    (∀ {γ} → γ ∉ free (all α A) → γ ∉ free (all β B) →
+     rename ((α , γ) ∷ []) A ≈ rename ((β , γ) ∷ []) B) →
     all α A ≈ all β B
 
 -- Basic Manipulations --------------------------------------------------------
@@ -104,5 +104,5 @@ subst ρs α⇒A (var β) =
 subst ρs α⇒A unit = unit
 subst ρs α⇒A (bin ⊗ B C) = bin ⊗ (subst ρs α⇒A B) (subst ρs α⇒A C)
 subst ρs α⇒A (all β B) =
-  let γ = mkFresh (map (applyRenaming ρs) (free (α⇒A .to) ++ free B)) in
+  let γ = 0 in
   all γ (subst ((β , γ) ∷ ρs) α⇒A B)
diff --git a/src/Data/Type/Properties.agda b/src/Data/Type/Properties.agda
new file mode 100644
index 0000000..80e104a
--- /dev/null
+++ b/src/Data/Type/Properties.agda
@@ -0,0 +1,231 @@
+{-# OPTIONS --without-K --safe #-}
+
+open import Data.Util
+
+module Data.Type.Properties
+  {mkFresh}
+  (isFresh : IsFresh mkFresh)
+  where
+
+open import Data.Bool using (Bool)
+open import Data.Empty using (⊥-elim)
+open import Data.List using (List; _++_; map; filter)
+open import Data.List.Membership.Propositional using (_∈_; _∉_)
+open import Data.List.Membership.Propositional.Properties
+open import Data.List.Properties
+open import Data.List.Properties.Ext
+open import Data.List.Relation.Unary.Any using (Any)
+open import Data.Nat using (ℕ; _≟_; _+_)
+open import Data.Product using () renaming (_,_ to _,′_)
+open import Data.Sum as ⊎ using (_⊎_; fromInj₁; fromInj₂; [_,_])
+open import Data.Type mkFresh
+open import Function using (_⇔_; _∘_; _∘₂_; mk⇔; id; flip)
+open import Relation.Binary hiding (_⇔_)
+open import Relation.Binary.PropositionalEquality as P
+  using (_≡_; _≢_; _≗_; sym; cong; cong₂; module ≡-Reasoning)
+open import Relation.Nullary using (Dec; Reflects; ¬_; _because_; yes; no)
+open import Relation.Nullary.Negation using (¬?; decidable-stable)
+
+open Any
+open Bool
+open Dec
+open List
+open Reflects
+open _≡_
+open _⊎_
+open ℕ
+
+private
+  variable
+    α β γ : ℕ
+    A B : Type
+
+-- Properties of applyRenaming ------------------------------------------------
+
+applyRenaming-skip :
+  ∀ β ρs → α ≢ γ → applyRenaming ((α , β) ∷ ρs) γ ≡ applyRenaming ρs γ
+applyRenaming-skip {α} {γ} β ρs α≢γ with α ≟ γ
+... | false because _      = refl
+... | true because ofʸ α≡γ = ⊥-elim (α≢γ α≡γ)
+
+applyRenaming-step :
+  ∀ α β ρs → applyRenaming ((α , β) ∷ ρs) α ≡ applyRenaming ρs β
+applyRenaming-step α β ρs with α ≟ α
+... | true because _        = refl
+... | false because ofⁿ α≢α = ⊥-elim (α≢α refl)
+
+applyRenaming-++ :
+  ∀ ρs ρs₁ → applyRenaming ρs₁ ∘ applyRenaming ρs ≗ applyRenaming (ρs ++ ρs₁)
+applyRenaming-++ []       ρs₁ α = refl
+applyRenaming-++ (ρ ∷ ρs) ρs₁ α = applyRenaming-++ ρs ρs₁ _
+
+applyRenaming⁻¹ :
+  ∀ ρs → applyRenaming ρs α ≡ β → α ≡ β ⊎ α ∈ map Subst.from ρs
+applyRenaming⁻¹         []             [ρs]α≡β = inj₁ [ρs]α≡β
+applyRenaming⁻¹ {α} {β} ((γ , δ) ∷ ρs) [ρs]α≡β with γ ≟ α
+... | true  because ofʸ γ≡α = inj₂ (here (sym γ≡α))
+... | false because ofⁿ _   = ⊎.map₂ there (applyRenaming⁻¹ ρs [ρs]α≡β)
+
+applyRenaming-lookup :
+  ∀ ρs → α ∈ map Subst.from ρs → applyRenaming ρs α ∈ map Subst.to ρs
+applyRenaming-lookup {α} ((β , γ) ∷ ρs) (here α≡β) with β ≟ α
+... | true because _ =
+  [ here ∘ sym , there ∘ applyRenaming-lookup ρs ] (applyRenaming⁻¹ ρs refl)
+... | no β≢α         = ⊥-elim (β≢α (sym α≡β))
+applyRenaming-lookup {α} ((β , γ) ∷ ρs) (there α∈ρs) with β ≟ α
+... | true because _ =
+  [ here ∘ sym , there ∘ applyRenaming-lookup ρs ] (applyRenaming⁻¹ ρs refl)
+... | no β≢α         = there (applyRenaming-lookup ρs α∈ρs)
+
+-- Properties of rename -------------------------------------------------------
+
+free-rename : ∀ ρs A → free (rename ρs A) ≡ map (applyRenaming ρs) (free A)
+free-rename ρs (var α)     = refl
+free-rename ρs unit        = refl
+free-rename ρs (bin ⊗ A B) = begin
+  free (rename ρs A) ++ free (rename ρs B)
+    ≡⟨  cong₂ _++_ (free-rename ρs A) (free-rename ρs B) ⟩
+  map (applyRenaming ρs) (free A) ++ map (applyRenaming ρs) (free B)
+    ≡˘⟨ map-++-commute _ (free A) (free B) ⟩
+  map (applyRenaming ρs) (free A ++ free B)
+    ∎
+  where open ≡-Reasoning
+free-rename ρs (all α A)   =
+  begin
+    filter (¬? ∘ (β′ ≟_)) (free (rename ((α , β′) ∷ ρs) A))
+      ≡⟨ cong (filter (¬? ∘ (β′ ≟_))) (free-rename ((α , β′) ∷ ρs) A) ⟩
+    filter (¬? ∘ (β′ ≟_)) (map (applyRenaming ((α , β′) ∷ ρs)) (free A))
+      ≡⟨ filter-map-comm
+           (¬? ∘ (β′ ≟_))
+           (¬? ∘ (α ≟_))
+           (free A)
+           x∈A⇒β≢[β/α,ρs]x⇔α≢x
+           (applyRenaming-skip β′ ρs) ⟩
+    map (applyRenaming ρs) (filter (¬? ∘ (α ≟_)) (free A))
+      ∎
+  where
+  open ≡-Reasoning
+  αs = free (all α A) ++ map Subst.from ρs ++ map Subst.to ρs
+  β′ = mkFresh αs
+
+  β∉ρs = isFresh .distinct αs ∘ ∈-++⁺ʳ (free (all α A))
+
+  β≡[β/α,ρs]α : β′ ≡ applyRenaming ((α , β′) ∷ ρs) α
+  β≡[β/α,ρs]α = begin
+    β′
+      ≡⟨  fromInj₁ (⊥-elim ∘ β∉ρs ∘ ∈-++⁺ˡ) (applyRenaming⁻¹ ρs refl) ⟩
+    applyRenaming ρs β′
+      ≡˘⟨ applyRenaming-step α β′ ρs ⟩
+    applyRenaming ((α , β′) ∷ ρs) α
+      ∎
+
+  x∈A⇒β≡[β/α,ρs]x⇒α≡x :
+    ∀ {x} → x ∈ free A → β′ ≡ applyRenaming ((α , β′) ∷ ρs) x → ¬ α ≢ x
+  x∈A⇒β≡[β/α,ρs]x⇒α≡x {x} x∈A β≡[β/α,ρs]x α≢x =
+    β∉ρs (∈-++⁺ʳ (map Subst.from ρs) β∈ρs₂)
+    where
+    x∈A/α : x ∈ free (all α A)
+    x∈A/α = ∈-filter⁺ (¬? ∘ (α ≟_)) x∈A α≢x
+
+    β≢x : β′ ≢ x
+    β≢x refl = isFresh .distinct αs (∈-++⁺ˡ x∈A/α)
+
+    β≡[ρs]x : β′ ≡ applyRenaming ρs x
+    β≡[ρs]x = P.trans β≡[β/α,ρs]x (applyRenaming-skip β′ ρs α≢x)
+
+    x≡β⊎x∈ρs : x ≡ β′ ⊎ x ∈ map Subst.from ρs
+    x≡β⊎x∈ρs = applyRenaming⁻¹ ρs (sym β≡[ρs]x)
+
+    x∈ρs₁ : x ∈ map Subst.from ρs
+    x∈ρs₁ = fromInj₂ (⊥-elim ∘ β≢x ∘ sym) x≡β⊎x∈ρs
+
+    β∈ρs₂ : β′ ∈ map Subst.to ρs
+    β∈ρs₂ =
+      P.subst (_∈ map Subst.to ρs) (sym β≡[ρs]x)
+        (applyRenaming-lookup ρs x∈ρs₁)
+
+  x∈A⇒β≢[β/α,ρs]x⇔α≢x :
+    ∀ {x} → x ∈ free A → β′ ≢ applyRenaming ((α , β′) ∷ ρs) x ⇔ α ≢ x
+  x∈A⇒β≢[β/α,ρs]x⇔α≢x x∈A =
+    mk⇔ (λ { β≢[β/α,ρs]α refl → β≢[β/α,ρs]α β≡[β/α,ρs]α })
+        (λ α≢x β≡[β/α,ρs]x → x∈A⇒β≡[β/α,ρs]x⇒α≡x x∈A β≡[β/α,ρs]x α≢x)
+
+  lemma′ : β ∉ free (all α A) → β ≡ α ⊎ β ∉ free A
+  lemma′ {β} β∉A/α with β ≟ α
+  ... | true  because ofʸ β≡α = inj₁ β≡α
+  ... | false because ofⁿ β≢α =
+    inj₂ (β∉A/α ∘ flip (∈-filter⁺ (¬? ∘ (α ≟_))) (β≢α ∘ sym))
+
+#∀-rename : ∀ ρs A → #∀ (rename ρs A) ≡ #∀ A
+#∀-rename ρs (var α)     = refl
+#∀-rename ρs unit        = refl
+#∀-rename ρs (bin ⊗ A B) = cong₂ _+_ (#∀-rename ρs A) (#∀-rename ρs B)
+#∀-rename ρs (all α A)   = cong suc (#∀-rename (_ ∷ ρs) A)
+
+size-rename : ∀ ρs A → size (rename ρs A) ≡ size A
+size-rename ρs (var α)     = refl
+size-rename ρs unit        = refl
+size-rename ρs (bin ⊗ A B) =
+  cong₂ (suc ∘₂ _+_) (size-rename ρs A) (size-rename ρs B)
+size-rename ρs (all α A)   = cong suc (size-rename (_ ∷ ρs) A)
+
+-- Properties of _≈_ ----------------------------------------------------------
+
+free-≈ : A ≈ B → free A ≡ free B
+free-≈ (var α)                   = refl
+free-≈ unit                      = refl
+free-≈ (bin A≈C B≈D)             = cong₂ _++_ (free-≈ A≈C) (free-≈ B≈D)
+free-≈ (all {α} {A} {β} {B} A≈B) = begin
+  free (all α A)
+    ≡˘⟨ lemma α γ′ (free A) γ∉∀α∙A ⟩
+  filter (¬? ∘ (γ′ ≟_)) (map (applyRenaming ((α , γ′) ∷ [])) (free A))
+    ≡⟨  cong (filter (¬? ∘ (γ′ ≟_))) (begin
+      map (applyRenaming ((α , γ′) ∷ [])) (free A)
+        ≡˘⟨ free-rename ((α , γ′) ∷ []) A ⟩
+      free (rename ((α , γ′) ∷ []) A)
+        ≡⟨  free-≈ (A≈B γ∉∀α∙A γ∉∀β∙B) ⟩
+      free (rename ((β , γ′) ∷ []) B)
+        ≡⟨  free-rename ((β , γ′) ∷ []) B ⟩
+      map (applyRenaming ((β , γ′) ∷ [])) (free B)
+        ∎) ⟩
+  filter (¬? ∘ (γ′ ≟_)) (map (applyRenaming ((β , γ′) ∷ [])) (free B))
+    ≡⟨  lemma β γ′ (free B) γ∉∀β∙B ⟩
+  free (all β B)
+    ∎
+  where
+  open ≡-Reasoning
+  γ′ = mkFresh (free (all α A) ++ free (all β B))
+  γ∉∀α∙A∪∀β∙B = isFresh .distinct (free (all α A) ++ free (all β B))
+  γ∉∀α∙A = γ∉∀α∙A∪∀β∙B ∘ ∈-++⁺ˡ
+  γ∉∀β∙B = γ∉∀α∙A∪∀β∙B ∘ ∈-++⁺ʳ _
+
+  lemma :
+    ∀ α β xs → β ∉ filter (¬? ∘ (α ≟_)) xs →
+    filter (¬? ∘ (β ≟_)) (map (applyRenaming ((α , β) ∷ [])) xs) ≡
+    filter (¬? ∘ (α ≟_)) xs
+  lemma α β xs β∉xs = begin
+    filter (¬? ∘ (β ≟_)) (map (applyRenaming ((α , β) ∷ [])) xs)
+      ≡⟨ filter-map-comm
+           (¬? ∘ (β ≟_))
+           (¬? ∘ (α ≟_))
+           xs
+           (λ x∈xs → mk⇔ (⇒ x∈xs) (⇐ x∈xs))
+           (applyRenaming-skip β []) ⟩
+    map id (filter (¬? ∘ (α ≟_)) xs)
+      ≡⟨ map-id _ ⟩
+    filter (¬? ∘ (α ≟_)) xs
+      ∎
+    where
+    ⇒ : ∀ {x} → x ∈ xs → β ≢ applyRenaming ((α , β) ∷ []) x → α ≢ x
+    ⇒ {x} x∈xs β≢[β/α]x α≡x with α ≟ x
+    ... | yes α≡x = β≢[β/α]x refl
+    ... | no α≢x  = α≢x α≡x
+
+    ⇐ : ∀ {x} → x ∈ xs → α ≢ x → β ≢ applyRenaming ((α , β) ∷ []) x
+    ⇐ {x} x∈xs α≢x β≡[β/α]x with α ≟ x
+    ... | no α≢x  =
+      β∉xs
+        (∈-filter⁺ (¬? ∘ (α ≟_))
+          (P.subst (_∈ _) (sym β≡[β/α]x) x∈xs)
+          (α≢x ∘ flip P.trans β≡[β/α]x))
+    ... | yes α≡x = α≢x α≡x
diff --git a/src/Data/Util.agda b/src/Data/Util.agda
new file mode 100644
index 0000000..4d9ec33
--- /dev/null
+++ b/src/Data/Util.agda
@@ -0,0 +1,13 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.Util where
+
+open import Data.List using (List)
+open import Data.List.Membership.Propositional using (_∉_)
+open import Data.Nat using (ℕ)
+
+record IsFresh (mkFresh : List ℕ → ℕ) : Set where
+  field
+    distinct : ∀ αs → mkFresh αs ∉ αs
+
+open IsFresh public