# [Agda] x \in (gfilter _ ys)

Sergei Meshveliani mechvel at botik.ru
Sun Aug 18 14:02:57 CEST 2013

People,
I have the next round in my battle with a filtered list proofs.
I need to proof that
x ∈  gfilter (toMaybe' P?) ys
if                   x ∈  ys
and  P Respects _≈_,  and (P x).

This needs to be by the function  in-gfiltered-id  below:

-----------------------------------------------------------------
open import Level            using (Level) renaming (zero to 0L)
open import Function         using (case_of_)
open import Relation.Nullary using (Dec; yes; no)
open import Relation.Unary   using (Decidable)
open import Relation.Binary  using (Rel; Setoid; module Setoid;
DecSetoid; module DecSetoid)
open import Relation.Binary.Core using (_Respects_; IsEquivalence;
module IsEquivalence)
open import Data.Empty    using (⊥-elim)
open import Data.Maybe    using (Maybe; just; nothing)
open import Data.Product  using (_×_; _,_)
open import Data.List     using (List; []; _∷_; map; gfilter)
open import Data.List.Any using (Any; module Any; module Membership)

toMaybe' : ∀ {p} {C : Set} {P : C → Set p} → Decidable P → C → Maybe C
toMaybe' P? x  with P? x
...                     | yes _ =  just x
...                     | _     =  nothing

postulate anything : ∀ {a} {A : Set a} → A       -- for debug

in-gfiltered-id : ∀ {l p} (A : Setoid 0L l) →    -- case f = id
let
open Setoid A using (_≈_) renaming (Carrier to C)
_∈_ = Membership._∈_ A
in
(P : C → Set p) → (P? : Decidable P) → P Respects _≈_ → (x : C) →
P x → (ys : List C) → x ∈ ys →
x ∈ (gfilter (toMaybe' P?) ys)

open Any

in-gfiltered-id {l} {p} A P P? pCong x Px (y ∷ ys) (here x=y) =

(let triple : Dec (P y) × Maybe C × List C
triple = (P? y , toMb y , filterMb (y ∷ ys))
in
case triple of \
{ (no ¬Py , _ ,      _  ) → let Py = pCong x=y Px in  ⊥-elim (¬Py Py)
; (yes Py , just y , z ∷ zs) →
let
y=z : y ≈ z
y=z = _ -- ? refl
x=z : x ≈ z
x=z = anything -- ? trans x=y y=z

p : Any {0L} {_} (_≈_ x) (z ∷ zs)
p = here x=z                      -- ?
-- here {0L} {_} {C} (_≈_ x) (z ∷ zs) {z} {zs} x=z
-- here {A = C} (_≈_ x) (z ∷ zs) {z} {zs} x=z
in p

; (yes Py , just y ,  []) → _  -- ?
; (yes Py , nothing , _ ) → _  -- ?
}
)
where
open Setoid A using (_≈_) renaming (Carrier to C)
open IsEquivalence (Setoid.isEquivalence A) using (refl; sym; trans)
toMb     = toMaybe' P?
filterMb = gfilter toMb

in-gfiltered-id A P P? pCong x Px (y ∷ ys) (there x∈ys) = _

-- after failing with here', I have not hope with there'

----------------------------------------------------------------------

1. How to prove  in-gfiltered-id ?

2. A note:  instead of  let triple : ...
triple = ( ... )
in
case triple of ...

above it is natural to write

case (P? y , toMb y , filterMb (y ∷ ys)) of ...,

but this latter is not type-checked (in Agda-2.3.2.1).

3. The report is
-------------
Cannot instantiate the metavariable _84 to solution
Any (_≈_ x) (z ∷ zs) since it contains the variable z which is not in
scope of the metavariable or irrelevant in the metavariable but relevant
in the solution when checking that the expression p has type
_B_84 A P P? pCong x Px y ys x=y
-------------

What is wrong with  z  ?

4. I tried to write  here' in full:

p = here {0L} {_} {C} (_≈_ x) (z ∷ zs) {z} {zs} x=z

And it reports
-------------------
Any (_P_100 A P P? pCong x Px y ys x=y Py y z zs)
(_x_101 A P P? pCong x Px y ys x=y Py y z zs ∷
_xs_102 A P P? pCong x Px y ys x=y Py y z zs)
should be a function type, but it isn't
when checking that
(z ∷ zs) {z} {zs} x=z

are valid arguments to a function of type
Any (_P_100 A P P? pCong x Px y ys x=y Py y z zs)
(_x_101 A P P? pCong x Px y ys x=y Py y z zs ∷
_xs_102 A P P? pCong x Px y ys x=y Py y z zs)
---------------------

Thank you in advance for explanation,

------
Sergei

`