From 1f5fe587d9c55a7cdaba5d77af37676c42aad8b5 Mon Sep 17 00:00:00 2001 From: Pedro Minicz Date: Sat, 26 Oct 2019 15:25:03 -0300 Subject: [PATCH] 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