From 1f5fe587d9c55a7cdaba5d77af37676c42aad8b5 Mon Sep 17 00:00:00 2001 From: Pedro Minicz Date: Sat, 26 Oct 2019 15:25:03 -0300 Subject: [PATCH 1/2] Fix: order of parameter in `split` function. The `merge` relation can be illustrated as follow: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit merge xs ys zs ≡ xs + ys = zs This shows a key point: every element of `xs` is contained in `zs`. The original definition of `split` makes no sense under this revelation. split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (xs : List A) → ∃[ ys ] ∃[ zs ] ( merge xs ys zs × All P ys × All (¬_ ∘ P) zs ) `zs` will contain all elements of `xs` (the input!) and we also have that `All (¬_ ∘ P) zs`. This function signature cannot be inhabited, as it would imply that for any `P : A → Set` and any `x : A` we have `¬(P x)`. --- src/plfa/part1/Lists.lagda.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index 0b013423..0f329662 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -1080,8 +1080,8 @@ Define the following variant of the traditional `filter` function on lists, which given a decidable predicate and a list returns all elements of the list satisfying the predicate: - split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (xs : List A) - → ∃[ ys ] ∃[ zs ] ( merge xs ys zs × All P ys × All (¬_ ∘ P) zs ) + split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A) + → ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys ) ``` -- Your code goes here From edd3e835815f809b6acae14577fa31abc6347c77 Mon Sep 17 00:00:00 2001 From: Pedro Minicz Date: Sat, 26 Oct 2019 15:45:15 -0300 Subject: [PATCH 2/2] Improve explanation of `split` exercise. --- src/plfa/part1/Lists.lagda.md | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/plfa/part1/Lists.lagda.md b/src/plfa/part1/Lists.lagda.md index 0f329662..8609ce79 100644 --- a/src/plfa/part1/Lists.lagda.md +++ b/src/plfa/part1/Lists.lagda.md @@ -1076,9 +1076,10 @@ into two lists that merge to give the original list, where all elements of one list satisfy the predicate, and all elements of the other do not satisfy the predicate. -Define the following variant of the traditional `filter` function on lists, -which given a decidable predicate and a list returns all elements of the -list satisfying the predicate: +Define the following variant of the traditional `filter` function on +lists, which given a decidable predicate and a list returns a list of +elements that satisfy the predicate and a list of elements that don't, +with their corresponding proofs. split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A) → ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )