michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Fix: order of parameter in split function.

Browse source 
The `merge` relation can be illustrated as follow:

    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)`.
This commit is contained in:
Pedro Minicz 2019-10-26 15:25:03 -03:00
parent 0e1c5d34ea
commit 1f5fe587d9
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/plfa/part1/Lists.lagda.md
View file

@ -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 which given a decidable predicate and a list returns all elements of the
list satisfying the predicate: list satisfying the predicate:
split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (xs : List A) split : ∀ {A : Set} {P : A → Set} (P? : Decidable P) (zs : List A)
→ ∃[ ys ] ∃[ zs ] ( merge xs ys zs × All P ys × All (¬_ ∘ P) zs ) → ∃[ xs ] ∃[ ys ] ( merge xs ys zs × All P xs × All (¬_ ∘ P) ys )
``` ```
-- Your code goes here -- Your code goes here