From 76d8d6bcbf42d12d58768cda85912f13ee5be714 Mon Sep 17 00:00:00 2001 From: wadler Date: Fri, 20 Apr 2018 11:14:12 -0300 Subject: [PATCH] backup before starting work --- src/Lists.lagda | 2 +- src/extra/Typed-backup.lagda | 221 +++++++++++------------------------ 2 files changed, 71 insertions(+), 152 deletions(-) diff --git a/src/Lists.lagda b/src/Lists.lagda index 1a5dfd1d..0962bae1 100644 --- a/src/Lists.lagda +++ b/src/Lists.lagda @@ -410,7 +410,7 @@ the argument on which we induct becomes *smaller*. Generalising on an auxiliary argument, which becomes larger as the argument on which we recurse or induct becomes smaller, is a common trick. It belongs in -you sling of arrows, ready to slay the right problem. +your quiver of arrows, ready to slay the right problem. Having defined shunt be generalisation, it is now easy to respecialise to give a more efficient definition of reverse. diff --git a/src/extra/Typed-backup.lagda b/src/extra/Typed-backup.lagda index fe0a5b87..fc16d88f 100644 --- a/src/extra/Typed-backup.lagda +++ b/src/extra/Typed-backup.lagda @@ -14,11 +14,12 @@ module Typed where import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_) open import Data.Empty using (⊥; ⊥-elim) -open import Data.List using (List; []; _∷_; [_]; _++_; map; foldr; filter) +open import Data.List using (List; []; _∷_; _++_; map; foldr; filter) open import Data.List.Any using (Any; here; there) open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_; _≟_) open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n) -open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) renaming (_,_ to ⟨_,_⟩) +open import Data.Product using (_×_; proj₁; proj₂; ∃; ∃-syntax) + renaming (_,_ to ⟨_,_⟩) open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.Unit using (⊤; tt) open import Function using (_∘_) @@ -27,6 +28,7 @@ open import Function.Equivalence using (_⇔_; equivalence) open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary.Negation using (contraposition; ¬?) open import Relation.Nullary.Product using (_×-dec_) +open import Collections using (_↔_) \end{code} @@ -216,58 +218,20 @@ erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (er ### Lists as sets \begin{code} -infix 4 _∈_ -infix 4 _⊆_ -infixl 5 _∪_ -infixl 5 _\\_ - -_∈_ : Id → List Id → Set -x ∈ xs = Any (x ≡_) xs - -_⊆_ : List Id → List Id → Set -xs ⊆ ys = ∀ {w} → w ∈ xs → w ∈ ys - -_∪_ : List Id → List Id → List Id -xs ∪ ys = xs ++ ys - -_\\_ : List Id → Id → List Id -xs \\ x = filter (¬? ∘ (x ≟_)) xs +open Collections.CollectionDec (Id) (_≟_) \end{code} ### Properties of sets \begin{code} -⊆∷ : ∀ {y xs ys} → xs ⊆ ys → xs ⊆ y ∷ ys -⊆∷ xs⊆ ∈xs = there (xs⊆ ∈xs) - -∷⊆∷ : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys) -∷⊆∷ xs⊆ (here refl) = here refl -∷⊆∷ xs⊆ (there ∈xs) = there (xs⊆ ∈xs) - -[]⊆ : ∀ {x xs} → [ x ] ⊆ xs → x ∈ xs -[]⊆ ⊆xs = ⊆xs (here refl) - -⊆[] : ∀ {x xs} → x ∈ xs → [ x ] ⊆ xs -⊆[] x∈ (here refl) = x∈ -⊆[] x∈ (there ()) - -bind : ∀ {x xs} → xs \\ x ⊆ xs -bind {x} {[]} () -bind {x} {y ∷ ys} with x ≟ y -... | yes refl = ⊆∷ (bind {x} {ys}) -... | no _ = ∷⊆∷ (bind {x} {ys}) - -left : ∀ {xs ys} → xs ⊆ xs ∪ ys -left (here refl) = here refl -left (there x∈) = there (left x∈) - -right : ∀ {xs ys} → ys ⊆ xs ∪ ys -right {[]} y∈ = y∈ -right {x ∷ xs} y∈ = there (right {xs} y∈) - -prev : ∀ {z y xs} → y ≢ z → z ∈ y ∷ xs → z ∈ xs -prev y≢z (here z≡y) = ⊥-elim (y≢z (sym z≡y)) -prev _ (there z∈) = z∈ +-- ⊆∷ : ∀ {y xs ys} → xs ⊆ ys → xs ⊆ y ∷ ys +-- ∷⊆∷ : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys) +-- []⊆ : ∀ {x xs} → [ x ] ⊆ xs → x ∈ xs +-- ⊆[] : ∀ {x xs} → x ∈ xs → [ x ] ⊆ xs +-- bind : ∀ {x xs} → xs \\ x ⊆ xs +-- left : ∀ {xs ys} → xs ⊆ xs ∪ ys +-- right : ∀ {xs ys} → ys ⊆ xs ∪ ys +-- prev : ∀ {z y xs} → y ≢ z → z ∈ y ∷ xs → z ∈ xs \end{code} ### Free variables @@ -287,7 +251,7 @@ fresh : List Id → Id fresh = foldr _⊔_ 0 ∘ map suc ⊔-lemma : ∀ {x xs} → x ∈ xs → suc x ≤ fresh xs -⊔-lemma {x} {.x ∷ xs} (here refl) = m≤m⊔n (suc x) (fresh xs) +⊔-lemma {x} {.x ∷ xs} here = m≤m⊔n (suc x) (fresh xs) ⊔-lemma {x} {y ∷ xs} (there x∈) = ≤-trans (⊔-lemma {x} {xs} x∈) (n≤m⊔n (suc y) (fresh xs)) @@ -302,9 +266,9 @@ fresh-lemma x∈ refl = 1+n≰n (⊔-lemma x∈) ∅ x = ⌊ x ⌋ _,_↦_ : (Id → Term) → Id → Term → (Id → Term) -(ρ , x ↦ M) y with x ≟ y +(ρ , x ↦ M) w with w ≟ x ... | yes _ = M -... | no _ = ρ y +... | no _ = ρ w \end{code} ### Substitution @@ -408,85 +372,47 @@ dom ε = [] dom (Γ , x ⦂ A) = x ∷ dom Γ dom-lemma : ∀ {Γ y B} → Γ ∋ y ⦂ B → y ∈ dom Γ -dom-lemma Z = here refl +dom-lemma Z = here dom-lemma (S x≢y ⊢y) = there (dom-lemma ⊢y) -f : ∀ {x y} → y ∈ [ x ] → y ≡ x -f (here y≡x) = y≡x -f (there ()) - -g : ∀ {w xs ys} → w ∈ xs ∪ ys → w ∈ xs ⊎ w ∈ ys -g {_} {[]} {ys} w∈ = inj₂ w∈ -g {_} {x ∷ xs} {ys} (here px) = inj₁ (here px) -g {_} {x ∷ xs} {ys} (there w∈) with g w∈ -... | inj₁ ∈xs = inj₁ (there ∈xs) -... | inj₂ ∈ys = inj₂ ∈ys - -k : ∀ {w x xs} → w ∈ xs \\ x → x ≢ w -k {w} {x} {[]} () -k {w} {x} {x′ ∷ xs′} w∈ with x ≟ x′ -k {w} {x} {x′ ∷ xs′} w∈ | yes refl = k {w} {x} {xs′} w∈ -k {w} {x} {x′ ∷ xs′} (here w≡x′) | no x≢x′ = λ x≡w → x≢x′ (trans x≡w w≡x′) -k {w} {x} {x′ ∷ xs′} (there w∈) | no x≢x′ = k {w} {x} {xs′} w∈ - -h : ∀ {x xs ys} → xs ⊆ x ∷ ys → xs \\ x ⊆ ys -h {x} {xs} {ys} xs⊆ {w} w∈ with xs⊆ (bind w∈) -... | here w≡x = ⊥-elim (k {w} {x} {xs} w∈ (sym w≡x)) -... | there w∈′ = w∈′ - free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ -free-lemma ⌊ ⊢x ⌋ w∈ rewrite f w∈ = dom-lemma ⊢x -free-lemma {Γ} (ƛ_ {x = x} {N = N} ⊢N) = h ih - where - ih : free N ⊆ x ∷ dom Γ - ih = free-lemma ⊢N -free-lemma (⊢L · ⊢M) w∈ with g w∈ -... | inj₁ ∈L = free-lemma ⊢L ∈L -... | inj₂ ∈M = free-lemma ⊢M ∈M +free-lemma ⌊ ⊢x ⌋ w∈ with w∈ +... | here = dom-lemma ⊢x +... | there () +free-lemma {Γ} (ƛ_ {x = x} {N = N} ⊢N) = proj₂ lemma-\\-∷ (free-lemma ⊢N) +free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈ +... | inj₁ ∈L = free-lemma ⊢L ∈L +... | inj₂ ∈M = free-lemma ⊢M ∈M \end{code} -Wow! A lot of work to prove stuff that is obvious. Gulp! - ### Renaming \begin{code} -∷drop : ∀ {v vs ys} → v ∷ vs ⊆ ys → vs ⊆ ys -∷drop ⊆ys ∈vs = ⊆ys (there ∈vs) - -i : ∀ {w x xs} → w ∈ xs → x ≢ w → w ∈ xs \\ x -i {w} {x} {.w ∷ xs} (here refl) x≢w with x ≟ w -... | yes refl = ⊥-elim (x≢w refl) -... | no _ = here refl -i {w} {x} {y ∷ xs} (there w∈) x≢w with x ≟ y -... | yes refl = (i {w} {x} {xs} w∈ x≢w) -... | no _ = there (i {w} {x} {xs} w∈ x≢w) - -j : ∀ {x xs ys} → xs \\ x ⊆ ys → xs ⊆ x ∷ ys -j {x} {xs} {ys} ⊆ys {w} w∈ with x ≟ w -... | yes refl = here refl -... | no x≢w = there (⊆ys (i w∈ x≢w)) - ⊢rename : ∀ {Γ Δ xs} → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) → (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) -⊢rename ⊢σ ⊆xs (⌊ ⊢x ⌋) = ⌊ ⊢σ ∈xs ⊢x ⌋ +⊢rename ⊢σ ⊆xs (⌊ ⊢x ⌋) = ⌊ ⊢σ ∈xs ⊢x ⌋ where - ∈xs = []⊆ ⊆xs + ∈xs = proj₂ lemma-[_] ⊆xs ⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N) - = ƛ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N) -- ⊆xs : free N \\ x ⊆ xs + = ƛ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N) where Γ′ = Γ , x ⦂ A Δ′ = Δ , x ⦂ A xs′ = x ∷ xs ⊢σ′ : ∀ {y B} → y ∈ xs′ → Γ′ ∋ y ⦂ B → Δ′ ∋ y ⦂ B - ⊢σ′ ∈xs′ Z = Z - ⊢σ′ ∈xs′ (S x≢y k) with ∈xs′ - ... | here refl = ⊥-elim (x≢y refl) - ... | there ∈xs = S x≢y (⊢σ ∈xs k) + ⊢σ′ ∈xs′ Z = Z + ⊢σ′ ∈xs′ (S x≢y ⊢y) with ∈xs′ + ... | here = ⊥-elim (x≢y refl) + ... | there ∈xs = S x≢y (⊢σ ∈xs ⊢y) ⊆xs′ : free N ⊆ xs′ - ⊆xs′ = j ⊆xs -⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M) = ⊢rename ⊢σ (⊆xs ∘ left) ⊢L · ⊢rename ⊢σ (⊆xs ∘ right) ⊢M + ⊆xs′ = proj₁ lemma-\\-∷ ⊆xs +⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M) + = ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M + where + L⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₁) ⊆xs + M⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₂) ⊆xs \end{code} @@ -494,20 +420,20 @@ j {x} {xs} {ys} ⊆ys {w} w∈ with x ≟ w \begin{code} lemma₁ : ∀ {y ys} → [ y ] ⊆ y ∷ ys -lemma₁ (here refl) = here refl -lemma₁ (there ()) +lemma₁ = proj₁ lemma-[_] here -lemma₂ : ∀ {z x xs} → x ≢ z → z ∈ x ∷ xs → z ∈ xs -lemma₂ x≢z (here refl) = ⊥-elim (x≢z refl) -lemma₂ _ (there z∈xs) = z∈xs +lemma₂ : ∀ {w x xs} → x ≢ w → w ∈ x ∷ xs → w ∈ xs +lemma₂ x≢ here = ⊥-elim (x≢ refl) +lemma₂ _ (there w∈) = w∈ ⊢subst : ∀ {Γ Δ xs ys ρ} → (∀ {x} → x ∈ xs → free (ρ x) ⊆ ys) → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A) → (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ subst ys ρ M ⦂ A) -⊢subst Σ ⊢ρ ⊆xs ⌊ ⊢x ⌋ = ⊢ρ (⊆xs (here refl)) ⊢x +⊢subst Σ ⊢ρ ⊆xs ⌊ ⊢x ⌋ + = ⊢ρ (⊆xs here) ⊢x ⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N) - = ƛ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N) + = ƛ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N) where y = fresh ys Γ′ = Γ , x ⦂ A @@ -516,43 +442,35 @@ lemma₂ _ (there z∈xs) = z∈xs ys′ = y ∷ ys ρ′ = ρ , x ↦ ⌊ y ⌋ - Σ′ : ∀ {z} → z ∈ xs′ → free (ρ′ z) ⊆ ys′ - Σ′ {z} (here refl) with x ≟ z + Σ′ : ∀ {w} → w ∈ xs′ → free (ρ′ w) ⊆ ys′ + Σ′ {w} here with w ≟ x ... | yes refl = lemma₁ - ... | no x≢z = ⊥-elim (x≢z refl) - Σ′ {z} (there x∈) with x ≟ z + ... | no w≢ = ⊥-elim (w≢ refl) + Σ′ {w} (there w∈) with w ≟ x ... | yes refl = lemma₁ - ... | no _ = there ∘ (Σ x∈) + ... | no _ = there ∘ (Σ w∈) ⊆xs′ : free N ⊆ xs′ - ⊆xs′ = j ⊆xs -{- - free (ƛ x ⦂ A ⇒ N) ⊆ xs - = def'n - free N \\ x ⊆ xs - = adjoint - free N ⊆ x ∷ xs --} + ⊆xs′ = proj₁ lemma-\\-∷ ⊆xs - ⊢σ : ∀ {z C} → z ∈ ys → Δ ∋ z ⦂ C → Δ′ ∋ z ⦂ C - ⊢σ z∈ ⊢z = S (fresh-lemma z∈) ⊢z + ⊢σ : ∀ {w C} → w ∈ ys → Δ ∋ w ⦂ C → Δ′ ∋ w ⦂ C + ⊢σ w∈ ⊢w = S (fresh-lemma w∈) ⊢w - ⊢ρ′ : ∀ {z C} → z ∈ xs′ → Γ′ ∋ z ⦂ C → Δ′ ⊢ ρ′ z ⦂ C + ⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C ⊢ρ′ _ Z with x ≟ x ... | yes _ = ⌊ Z ⌋ ... | no x≢x = ⊥-elim (x≢x refl) - ⊢ρ′ {z} z∈′ (S x≢z ⊢z) with x ≟ z - ... | yes x≡z = ⊥-elim (x≢z x≡z) - ... | no _ = ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ z∈) (⊢ρ z∈ ⊢z) + ⊢ρ′ {w} w∈′ (S x≢w ⊢w) with w ≟ x + ... | yes refl = ⊥-elim (x≢w refl) + ... | no _ = ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ w∈) (⊢ρ w∈ ⊢w) where - z∈ = lemma₂ x≢z z∈′ + w∈ = lemma₂ x≢w w∈′ -⊢subst {xs = xs} Σ ⊢ρ {L · M} ⊆xs (⊢L · ⊢M) = ⊢subst Σ ⊢ρ L⊆xs ⊢L · ⊢subst Σ ⊢ρ M⊆xs ⊢M +⊢subst {xs = xs} Σ ⊢ρ {L · M} ⊆xs (⊢L · ⊢M) + = ⊢subst Σ ⊢ρ L⊆ ⊢L · ⊢subst Σ ⊢ρ M⊆ ⊢M where - L⊆xs : free L ⊆ xs - L⊆xs = ⊆xs ∘ left - M⊆xs : free M ⊆ xs - M⊆xs = ⊆xs ∘ right + L⊆ = trans-⊆ lemma-∪₁ ⊆xs + M⊆ = trans-⊆ lemma-∪₂ ⊆xs ⊢substitution : ∀ {Γ x A N B M} → Γ , x ⦂ A ⊢ N ⦂ B → @@ -568,19 +486,20 @@ lemma₂ _ (there z∈xs) = z∈xs ρ = ∅ , x ↦ M Σ : ∀ {w} → w ∈ xs → free (ρ w) ⊆ ys - Σ {w} w∈ y∈ with x ≟ w - ... | yes _ = left y∈ - ... | no x≢w with y∈ - ... | here refl = right (i {w} {x} {free N} w∈ x≢w) - ... | there () + Σ {w} w∈ y∈ with w ≟ x + ... | yes _ = lemma-∪₁ y∈ + ... | no w≢ with y∈ + ... | here = lemma-∪₂ + (proj₂ lemma-\\-∈-≢ ⟨ w∈ , w≢ ⟩) + ... | there () ⊢ρ : ∀ {z C} → z ∈ xs → Γ′ ∋ z ⦂ C → Γ ⊢ ρ z ⦂ C ⊢ρ {.x} z∈ Z with x ≟ x ... | yes _ = ⊢M ... | no x≢x = ⊥-elim (x≢x refl) - ⊢ρ {z} z∈ (S x≢z ⊢z) with x ≟ z - ... | yes x≡z = ⊥-elim (x≢z x≡z) - ... | no _ = ⌊ ⊢z ⌋ + ⊢ρ {z} z∈ (S x≢z ⊢z) with z ≟ x + ... | yes refl = ⊥-elim (x≢z refl) + ... | no _ = ⌊ ⊢z ⌋ ⊆xs : free N ⊆ xs ⊆xs x∈ = x∈