backup before starting work

This commit is contained in:
wadler 2018-04-20 11:14:12 -03:00
parent 2e69aaf865
commit 76d8d6bcbf
2 changed files with 71 additions and 152 deletions

View file

@ -410,7 +410,7 @@ the argument on which we induct becomes *smaller*.
Generalising on an auxiliary argument, which becomes larger as the argument on 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 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 Having defined shunt be generalisation, it is now easy to respecialise to
give a more efficient definition of reverse. give a more efficient definition of reverse.

View file

@ -14,11 +14,12 @@ module Typed where
import Relation.Binary.PropositionalEquality as Eq import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_) open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim) 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.List.Any using (Any; here; there)
open import Data.Nat using (; zero; suc; _+_; _∸_; _≤_; _⊔_; _≟_) 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.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.Sum using (_⊎_; inj₁; inj₂)
open import Data.Unit using (; tt) open import Data.Unit using (; tt)
open import Function using (_∘_) 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 using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (contraposition; ¬?) open import Relation.Nullary.Negation using (contraposition; ¬?)
open import Relation.Nullary.Product using (_×-dec_) open import Relation.Nullary.Product using (_×-dec_)
open import Collections using (_↔_)
\end{code} \end{code}
@ -216,58 +218,20 @@ erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (er
### Lists as sets ### Lists as sets
\begin{code} \begin{code}
infix 4 _∈_ open Collections.CollectionDec (Id) (_≟_)
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
\end{code} \end{code}
### Properties of sets ### Properties of sets
\begin{code} \begin{code}
⊆∷ : ∀ {y xs ys} → xs ⊆ ys → xs ⊆ y ∷ ys -- ⊆∷ : ∀ {y xs ys} → xs ⊆ ys → xs ⊆ y ∷ ys
⊆∷ xs⊆ ∈xs = there (xs⊆ ∈xs) -- ∷⊆∷ : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys)
-- []⊆ : ∀ {x xs} → [ x ] ⊆ xs → x ∈ xs
∷⊆∷ : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys) -- ⊆[] : ∀ {x xs} → x ∈ xs → [ x ] ⊆ xs
∷⊆∷ xs⊆ (here refl) = here refl -- bind : ∀ {x xs} → xs \\ x ⊆ xs
∷⊆∷ xs⊆ (there ∈xs) = there (xs⊆ ∈xs) -- left : ∀ {xs ys} → xs ⊆ xs ys
-- right : ∀ {xs ys} → ys ⊆ xs ys
[]⊆ : ∀ {x xs} → [ x ] ⊆ xs → x ∈ xs -- prev : ∀ {z y xs} → y ≢ z → z ∈ y ∷ xs → z ∈ 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∈
\end{code} \end{code}
### Free variables ### Free variables
@ -287,7 +251,7 @@ fresh : List Id → Id
fresh = foldr _⊔_ 0 ∘ map suc fresh = foldr _⊔_ 0 ∘ map suc
⊔-lemma : ∀ {x xs} → x ∈ xs → suc x ≤ fresh xs ⊔-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∈) ⊔-lemma {x} {y ∷ xs} (there x∈) = ≤-trans (⊔-lemma {x} {xs} x∈)
(n≤m⊔n (suc y) (fresh xs)) (n≤m⊔n (suc y) (fresh xs))
@ -302,9 +266,9 @@ fresh-lemma x∈ refl = 1+n≰n (⊔-lemma x∈)
∅ x = ⌊ x ⌋ ∅ x = ⌊ x ⌋
_,_↦_ : (Id → Term) → Id → Term → (Id → Term) _,_↦_ : (Id → Term) → Id → Term → (Id → Term)
(ρ , x ↦ M) y with x ≟ y (ρ , x ↦ M) w with w ≟ x
... | yes _ = M ... | yes _ = M
... | no _ = ρ y ... | no _ = ρ w
\end{code} \end{code}
### Substitution ### Substitution
@ -408,85 +372,47 @@ dom ε = []
dom (Γ , x ⦂ A) = x ∷ dom Γ dom (Γ , x ⦂ A) = x ∷ dom Γ
dom-lemma : ∀ {Γ y B} → Γ ∋ y ⦂ B → y ∈ 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) 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 : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ
free-lemma ⌊ ⊢x ⌋ w∈ rewrite f w∈ = dom-lemma ⊢x free-lemma ⌊ ⊢x ⌋ w∈ with w∈
free-lemma {Γ} (ƛ_ {x = x} {N = N} ⊢N) = h ih ... | here = dom-lemma ⊢x
where ... | there ()
ih : free N ⊆ x ∷ dom Γ free-lemma {Γ} (ƛ_ {x = x} {N = N} ⊢N) = proj₂ lemma-\\-∷ (free-lemma ⊢N)
ih = free-lemma ⊢N free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎- w∈
free-lemma (⊢L · ⊢M) w∈ with g w∈ ... | inj₁ ∈L = free-lemma ⊢L ∈L
... | inj₁ ∈L = free-lemma ⊢L ∈L ... | inj₂ ∈M = free-lemma ⊢M ∈M
... | inj₂ ∈M = free-lemma ⊢M ∈M
\end{code} \end{code}
Wow! A lot of work to prove stuff that is obvious. Gulp!
### Renaming ### Renaming
\begin{code} \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) → ⊢rename : ∀ {Γ Δ xs} → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) →
(∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A) (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
⊢rename ⊢σ ⊆xs (⌊ ⊢x ⌋) = ⌊ ⊢σ ∈xs ⊢x ⌋ ⊢rename ⊢σ ⊆xs (⌊ ⊢x ⌋) = ⌊ ⊢σ ∈xs ⊢x ⌋
where where
∈xs = []⊆ ⊆xs ∈xs = proj₂ lemma-[_] ⊆xs
⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N) ⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N)
= ƛ (⊢rename {Γ′} {Δ′} {xs} ⊢σ′ ⊆xs ⊢N) -- ⊆xs : free N \\ x ⊆ xs = ƛ (⊢rename {Γ′} {Δ′} {xs} ⊢σ′ ⊆xs ⊢N)
where where
Γ′ = Γ , x ⦂ A Γ′ = Γ , x ⦂ A
Δ′ = Δ , x ⦂ A Δ′ = Δ , x ⦂ A
xs = x ∷ xs xs = x ∷ xs
⊢σ′ : ∀ {y B} → y ∈ xs → Γ′ ∋ y ⦂ B → Δ′ ∋ y ⦂ B ⊢σ′ : ∀ {y B} → y ∈ xs → Γ′ ∋ y ⦂ B → Δ′ ∋ y ⦂ B
⊢σ′ ∈xs Z = Z ⊢σ′ ∈xs Z = Z
⊢σ′ ∈xs (S x≢y k) with ∈xs ⊢σ′ ∈xs (S x≢y ⊢y) with ∈xs
... | here refl = ⊥-elim (x≢y refl) ... | here = ⊥-elim (x≢y refl)
... | there ∈xs = S x≢y (⊢σ ∈xs k) ... | there ∈xs = S x≢y (⊢σ ∈xs ⊢y)
⊆xs : free N ⊆ xs ⊆xs : free N ⊆ xs
⊆xs = j ⊆xs ⊆xs = proj₁ lemma-\\-∷ ⊆xs
⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M) = ⊢rename ⊢σ (⊆xs ∘ left) ⊢L · ⊢rename ⊢σ (⊆xs ∘ right) ⊢M ⊢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} \end{code}
@ -494,20 +420,20 @@ j {x} {xs} {ys} ⊆ys {w} w∈ with x ≟ w
\begin{code} \begin{code}
lemma₁ : ∀ {y ys} → [ y ] ⊆ y ∷ ys lemma₁ : ∀ {y ys} → [ y ] ⊆ y ∷ ys
lemma₁ (here refl) = here refl lemma₁ = proj₁ lemma-[_] here
lemma₁ (there ())
lemma₂ : ∀ {z x xs} → x ≢ z → z ∈ x ∷ xs → z ∈ xs lemma₂ : ∀ {w x xs} → x ≢ w → w ∈ x ∷ xs → w ∈ xs
lemma₂ x≢z (here refl) = ⊥-elim (x≢z refl) lemma₂ x≢ here = ⊥-elim (x≢ refl)
lemma₂ _ (there z∈xs) = z∈xs lemma₂ _ (there w∈) = w∈
⊢subst : ∀ {Γ Δ xs ys ρ} → ⊢subst : ∀ {Γ Δ xs ys ρ} →
(∀ {x} → x ∈ xs → free (ρ x) ⊆ ys) → (∀ {x} → x ∈ xs → free (ρ x) ⊆ ys) →
(∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A) → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A) →
(∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ subst ys ρ M ⦂ 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) ⊢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 where
y = fresh ys y = fresh ys
Γ′ = Γ , x ⦂ A Γ′ = Γ , x ⦂ A
@ -516,43 +442,35 @@ lemma₂ _ (there z∈xs) = z∈xs
ys = y ∷ ys ys = y ∷ ys
ρ = ρ , x ↦ ⌊ y ⌋ ρ = ρ , x ↦ ⌊ y ⌋
Σ′ : ∀ {z} → z ∈ xs → free (ρ z) ⊆ ys Σ′ : ∀ {w} → w ∈ xs → free (ρ w) ⊆ ys
Σ′ {z} (here refl) with x ≟ z Σ′ {w} here with w ≟ x
... | yes refl = lemma₁ ... | yes refl = lemma₁
... | no x≢z = ⊥-elim (x≢z refl) ... | no w≢ = ⊥-elim (w≢ refl)
Σ′ {z} (there x∈) with x ≟ z Σ′ {w} (there w∈) with w ≟ x
... | yes refl = lemma₁ ... | yes refl = lemma₁
... | no _ = there ∘ (Σ x∈) ... | no _ = there ∘ (Σ w∈)
⊆xs : free N ⊆ xs ⊆xs : free N ⊆ xs
⊆xs = j ⊆xs ⊆xs = proj₁ lemma-\\-∷ ⊆xs
{-
free (ƛ x ⦂ A ⇒ N) ⊆ xs
= def'n
free N \\ x ⊆ xs
= adjoint
free N ⊆ x ∷ xs
-}
⊢σ : ∀ {z C} → z ∈ ys → Δ ∋ z ⦂ C → Δ′ ∋ z ⦂ C ⊢σ : ∀ {w C} → w ∈ ys → Δ ∋ w ⦂ C → Δ′ ∋ w ⦂ C
⊢σ z∈ ⊢z = S (fresh-lemma z∈) ⊢z ⊢σ 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 ⊢ρ′ _ Z with x ≟ x
... | yes _ = ⌊ Z ⌋ ... | yes _ = ⌊ Z ⌋
... | no x≢x = ⊥-elim (x≢x refl) ... | no x≢x = ⊥-elim (x≢x refl)
⊢ρ′ {z} z∈ (S x≢z ⊢z) with x ≟ z ⊢ρ′ {w} w∈ (S x≢w ⊢w) with w ≟ x
... | yes x≡z = ⊥-elim (x≢z x≡z) ... | yes refl = ⊥-elim (x≢w refl)
... | no _ = ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ z∈) (⊢ρ z∈ ⊢z) ... | no _ = ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ w∈) (⊢ρ w∈ ⊢w)
where 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 where
L⊆xs : free L ⊆ xs L⊆ = trans-⊆ lemma-∪₁ ⊆xs
L⊆xs = ⊆xs ∘ left M⊆ = trans-⊆ lemma-∪₂ ⊆xs
M⊆xs : free M ⊆ xs
M⊆xs = ⊆xs ∘ right
⊢substitution : ∀ {Γ x A N B M} → ⊢substitution : ∀ {Γ x A N B M} →
Γ , x ⦂ A ⊢ N ⦂ B → Γ , x ⦂ A ⊢ N ⦂ B →
@ -568,19 +486,20 @@ lemma₂ _ (there z∈xs) = z∈xs
ρ = ∅ , x ↦ M ρ = ∅ , x ↦ M
Σ : ∀ {w} → w ∈ xs → free (ρ w) ⊆ ys Σ : ∀ {w} → w ∈ xs → free (ρ w) ⊆ ys
Σ {w} w∈ y∈ with x ≟ w Σ {w} w∈ y∈ with w ≟ x
... | yes _ = left y∈ ... | yes _ = lemma-∪₁ y∈
... | no x≢w with y∈ ... | no w≢ with y∈
... | here refl = right (i {w} {x} {free N} w∈ x≢w) ... | here = lemma-∪₂
... | there () (proj₂ lemma-\\-∈-≢ ⟨ w∈ , w≢ ⟩)
... | there ()
⊢ρ : ∀ {z C} → z ∈ xs → Γ′ ∋ z ⦂ C → Γ ⊢ ρ z ⦂ C ⊢ρ : ∀ {z C} → z ∈ xs → Γ′ ∋ z ⦂ C → Γ ⊢ ρ z ⦂ C
⊢ρ {.x} z∈ Z with x ≟ x ⊢ρ {.x} z∈ Z with x ≟ x
... | yes _ = ⊢M ... | yes _ = ⊢M
... | no x≢x = ⊥-elim (x≢x refl) ... | no x≢x = ⊥-elim (x≢x refl)
⊢ρ {z} z∈ (S x≢z ⊢z) with x ≟ z ⊢ρ {z} z∈ (S x≢z ⊢z) with z ≟ x
... | yes x≡z = ⊥-elim (x≢z x≡z) ... | yes refl = ⊥-elim (x≢z refl)
... | no _ = ⌊ ⊢z ⌋ ... | no _ = ⌊ ⊢z ⌋
⊆xs : free N ⊆ xs ⊆xs : free N ⊆ xs
⊆xs x∈ = x∈ ⊆xs x∈ = x∈