Open
Description
WIP!
TODO: fix up the description of this issue
Meanwhile, this is an enhancement of @Taneb 's original, contrasting behaviour of filter with that of partition:
(tested under v2.6.3; does this also yield yellow under v2.6.4.*?)
module V21-BUG where
open import Data.Bool.Base using (true; false; if_then_else_)
open import Data.List.Base using (List; []; _∷_)
open import Data.Product.Base using (_,_; _×_)
open import Level using (Level)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Unary using (Pred; Decidable)
open import Relation.Nullary using (does; _because_; invert; contradiction)
private
variable
a p : Level
A : Set a
x : A
xs : List A
module _ {P : Pred A p} (P? : Decidable P) where
filter : List A → List A
filter [] = []
-- ORIGINAL: Working
filter (x ∷ xs) with does (P? x)
... | false = filter xs
... | true = x ∷ filter xs
partition : List A → (List A × List A)
partition [] = [] , []
{-
-- NOT Working
-- refactor original
partition (x ∷ xs) with ys , zs ← partition xs | does (P? x)
... | true = x ∷ ys , zs
... | false = ys , x ∷ zs
-- direct-style
partition (x ∷ xs) = let ys , zs = partition xs in if does (P? x)
then (x ∷ ys , zs)
else (ys , x ∷ zs)
-}
-- ORIGINAL: ALSO NOT Working
partition (x ∷ xs) with does (P? x) | partition xs
... | true | (ys , zs) = (x ∷ ys , zs)
... | false | (ys , zs) = (ys , x ∷ zs)
filter-accept : P x → filter (x ∷ xs) ≡ x ∷ filter xs
filter-accept {x = x} Px with P? x
... | true because _ = refl
... | false because [¬Px] = contradiction Px (invert [¬Px])
filter-eq : ∀ x xs → P x → filter (x ∷ xs) ≡ x ∷ filter xs
filter-eq x xs Px = filter-accept Px
partition-accept : P x → let ys , zs = partition xs in partition (x ∷ xs) ≡ (x ∷ ys , zs)
partition-accept {x = x} {xs = xs} Px with P? x
... | true because _ = refl
... | false because [¬Px] = contradiction Px (invert [¬Px])
partition-eq : ∀ x xs → P x → let ys , zs = partition xs in partition (x ∷ xs) ≡ (x ∷ ys , zs)
partition-eq x xs Px = partition-accept Px {- YELLOW!? -}
{-
Failed to solve the following constraints:
Data.Product.Base.proj₂ (partition _xs_95)
= Data.Product.Base.proj₂ (partition xs)
: List A
(blocked on _xs_95)
Data.Product.Base.proj₁ (partition _xs_95)
= Data.Product.Base.proj₁ (partition xs)
: List A
(blocked on _xs_95)
partition _xs_95 = partition xs
: Data.Product.Base.Σ (List A) (λ x₁ → List A)
(blocked on _xs_95)
-}