Unsolved metas in `Data.List.Properties` cf. discussion on #2415, #2359, #2365

[jamesmckinna]

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)
  -}

[JacquesCarette]

Thanks for posting this. For reporting upstream, we'll have to golf a bit to get a MWE that eliminates as much stdlib as possible by inlining.

[jamesmckinna]

I think that unless we can figure this out for v2.1-rc2, this should be punted to v2.2?

[JacquesCarette]

I agree that we shouldn't hold up v2.1 for this.