Cannot prove property of function that uses with-in instead of stdlib's inspect

[omelkonian]

The following lemma about membership and mapMaybe has to be defined using the non-internalized inspect,
in order to prove the ∈-mapMaybe⁻-nothing property:

open import Data.Empty
open import Data.Unit
open import Data.Product
open import Data.Maybe
open import Data.List
open import Data.List.Relation.Unary.Any
open import Data.List.Membership.Propositional
open import Relation.Binary.PropositionalEquality as ≡ using (refl; _≡_; inspect)

variable
  A B : Set
  x : A
  y : B
  xs : List A

Is-there : x ∈ xs → Set
Is-there = λ where
  (here _)  → ⊥
  (there _) → ⊤

module _ (f : A → Maybe B) where
  ∈-mapMaybe⁻ : y ∈ mapMaybe f xs
              → ∃ λ x → (x ∈ xs) × (f x ≡ just y)
  ∈-mapMaybe⁻ {y = y} {xs = x ∷ xs} y∈
  --   with f x in fx≡
  -- ... | nothing = map₂ (map₁ there) (∈-mapMaybe⁻ y∈)
  -- ... | just y′
    with f x | inspect f x
  ... | nothing | _ = map₂ (map₁ there) (∈-mapMaybe⁻ y∈)
  ... | just y′ | ≡.[ fx≡ ]
    with y∈
  ... | here refl = x , here refl , fx≡
  ... | there y∈′ = map₂ (map₁ there) (∈-mapMaybe⁻ y∈′)

  ∈-mapMaybe⁻-nothing : (y∈ : y ∈ mapMaybe f (x ∷ xs))
    → f x ≡ nothing
    → Is-there (∈-mapMaybe⁻ y∈ .proj₂ .proj₁)
  ∈-mapMaybe⁻-nothing {x = x} {xs = xs} y∈ fx≡
    with f x | inspect f x | fx≡
  ... | nothing | _ | _ = tt
  ... | just _  | _ | ()

Seems like a bug in the implementation of with...in..., @gallais?

[jamesmckinna]

The first function does now typecheck, as follows:

  ∈-mapMaybe⁻ {y = y} {xs = x ∷ xs} y∈
    with f x in fx≡
  ... | nothing = map₂ (map₁ there) (∈-mapMaybe⁻ y∈)
  ... | just y′ with y∈
  ... | here refl = x , here refl , fx≡
  ... | there y∈′ = map₂ (map₁ there) (∈-mapMaybe⁻ y∈′)

Ah... gotcha. [UPDATED: solved below]

[jamesmckinna]

For which one can prove the following lemma: [UPDATED to streamline the use of with ... in ...]

  ∈-mapMaybe⁻-nothing-∈-mapMaybe⁺ : (y∈ : y ∈ mapMaybe f (x ∷ xs)) →
    f x ≡ nothing → y ∈ mapMaybe f xs
  ∈-mapMaybe⁻-nothing-∈-mapMaybe⁺ {y = y} {x = x} {xs = xs} y∈ fx≡nothing
        with _ ← mapMaybe f (x ∷ xs) in eq rewrite fx≡nothing | eq = y∈

but for which I don't seem able to prove the lemma that you want. [UPDATED: see below]

[jamesmckinna]

A question I cannot yet answer is whether implementing with-application would help, as follows:

  ∈-mapMaybe⁻-nothing : (y∈ : y ∈ mapMaybe f (x ∷ xs)) →
    (eq : f x ≡ nothing) →
    Is-there {xs = x ∷ xs} (∈-mapMaybe⁻ {y = y} (y∈ | f x | eq)  .proj₂ .proj₁)

i.e. to correlate the equation eq with its use in unfolding y∈, which we see in the provable lemma above.

The other thing to say is that the lemma I should have liked to prove may require --with-K?
Something to discuss further at AIM XXXVI this morning...?

[omelkonian]

Here are some more example on the same theme if you want to play around a bit more: https://omelkonian.github.io/formal-prelude/Prelude.Lists.MapMaybe.html

[jamesmckinna]

Actually, I think the following solves it:

  ∈-mapMaybe⁻-nothing : (y∈ : y ∈ mapMaybe f (x ∷ xs)) →
                        (fx≡nothing : f x ≡ nothing) →
                        Is-there ((∈-mapMaybe⁻ y∈) .proj₂ .proj₁)
  ∈-mapMaybe⁻-nothing y∈ fx≡nothing with ∈-mapMaybe⁻ y∈
  ... | x , here refl , fx≡just[y] with () ←  ≡.trans (≡.sym fx≡nothing) fx≡just[y]
  ... | z , there y∈′ , fz≡just[y] = _

The wart in this is of course the RHS treatment of ≡.trans (≡.sym fx≡nothing) fx≡just[y], because the corresponding rewrite steps seem to be forbidden after with ∈-mapMaybe⁻ {xs = x ∷ xs} y∈. Notice that with ... in ... does not seem to be required in this proof?

[jamesmckinna]

Rewriting this with an auxiliary function helps clarify things a little, but I kept hitting the error message

Cannot `with` on variable fz≡just[y] bound in a module telescope
(or patterns of a parent clause)
when inferring the type of fx≡just[y]

Accordingly, with a bit more abstraction (can the machine do this?), and noting that here refl forces z = x in the first clause of aux:

  ∈-mapMaybe⁻-nothing : (y∈ : y ∈ mapMaybe f (x ∷ xs)) →
                        (fx≡nothing : f x ≡ nothing) →
                        Is-there ((∈-mapMaybe⁻ y∈) .proj₂ .proj₁)
  ∈-mapMaybe⁻-nothing {y = y} {x = x} {xs = xs} y∈ fx≡nothing
    with z , p , fz≡just[y] ← ∈-mapMaybe⁻ y∈ = aux p fz≡just[y]
    where
      aux : (p : Any (_≡_ z) (x ∷ xs)) → (f z ≡ just y) → Is-there p
      aux (here refl) fx≡just[y] rewrite fx≡nothing with () ← fx≡just[y]
      aux (there p) _ = _

[jamesmckinna]

None of this, of course, vitiates @omelkonian 's original (meta-)point (made eloquently at AIMXXXVI last month) about "don't use with unless you really mean it; ordinary pattern matching suffices, and is easier to prove things about". But then, I agree with that sentiment as well.

But I don't think that this example shows that the use of inspect is necessary, which would be a relief to stdlib maintainers... and the authors of stdlib PR 1930 and stdlib PR 1630... as well as @gallais himself.

But perhaps other fiendish (counter)examples exist out there?

[omelkonian]

@jamesmckinna Nice workaround, although I don't like that it's following an entirely different recursion pattern than the original in ∈-mapMaybe⁻...

So I guess a bug remains with respect to how faithfully with-in internalises the inspect idiom, namely this is accepted:

∈-mapMaybe⁻ : y ∈ mapMaybe f xs
            → ∃ λ x → (x ∈ xs) × (f x ≡ just y)
∈-mapMaybe⁻ {y = y} {xs = x ∷ xs} y∈
  with f x | inspect f x
... | nothing | _ = map₂ (map₁ there) (∈-mapMaybe⁻ y∈)
... | just y′ | ≡.[ fx≡ ]
  with y∈
... | here refl = x , here refl , fx≡
... | there y∈′ = map₂ (map₁ there) (∈-mapMaybe⁻ y∈′)

∈-mapMaybe⁻-nothing : (y∈ : y ∈ mapMaybe f (x ∷ xs))
  → f x ≡ nothing
  → Is-there (∈-mapMaybe⁻ y∈ .proj₂ .proj₁)
∈-mapMaybe⁻-nothing {x = x} {xs = xs} y∈ fx≡
  with f x | inspect f x
... | nothing | _ = tt

...but this is not:

∈-mapMaybe⁻ : y ∈ mapMaybe f xs
            → ∃ λ x → (x ∈ xs) × (f x ≡ just y)
∈-mapMaybe⁻ {y = y} {xs = x ∷ xs} y∈
  with f x in fx≡
... | nothing = map₂ (map₁ there) (∈-mapMaybe⁻ y∈)
... | just y′
  with y∈
... | here refl = x , here refl , fx≡
... | there y∈′ = map₂ (map₁ there) (∈-mapMaybe⁻ y∈′)

∈-mapMaybe⁻-nothing : (y∈ : y ∈ mapMaybe f (x ∷ xs))
  → f x ≡ nothing
  → Is-there (∈-mapMaybe⁻ y∈ .proj₂ .proj₁)
∈-mapMaybe⁻-nothing {x = x} {xs = xs} y∈ fx≡
  with f x in _
... | nothing | _ = tt

[jamesmckinna]

Hmmm. Just to be clear:

• you're happy with the with ... in ... defn of ∈-mapMaybe⁻?
• but NOT happy with the revised defn of ∈-mapMaybe⁻-nothing?

Regarding the former, there does seem to be a clear like-for-like replacement of the use of the inspect idiom by with ... in ..., yes? UPDATED: no, perhaps not, for the same reasons as below: the function may be definable (and typecheck!), but with a lazier analysis of the equation fx≡; that very laziness then bites when trying to prove something about the function definition...

Regarding the latter, I think I do see a (the?) problem: inspect f x = [ refl {x = f x} ] is actually more strict than with f x in eq, which delays the analysis of the equality eq and hence whether or not the typechecker can match it against refl/rewrite with it... whereas this has already happened in any inspect-based definition and proof. (There's a separate bug/anomaly about not being able to do rewrite or pattern-matching with after a with ... in ... which I keep tripping over; apparently trying to use a nested with fails also in this instance, which is very annoying). That might account for the slight gymnastics required in my 'workaround' proofs.

In that respect, it's actually a bit weird that the original pragmatics (of each idiom) was to give a name (pattern variable binding) to the equation, when in the case of inspect, that pattern variable is always definitionally bound to refl!

So the issue seems to be that the lazier with ... in eq might miss opportunities for goals to be well-typed, which would otherwise be OK after subsequent matching of eq against refl. To restore such strictness, we would need to be able to inline the match of eq against refl, eg via an eq@refl pattern, but that doesn't seem to be possible... yet? (Does this generate the same error as rewrite-after-a-with?)

@gallais, do you think the idiom could be extended to incorporate such behaviour? eg by positing the auxiliary function generated by with to actually be a pattern-matching lambda, with the match on refl built into its definition?

[omelkonian]

Hmmm. Just to be clear:

* you're happy with the `with ... in ...` defn of `∈-mapMaybe⁻`?

* but NOT happy with the revised defn of `∈-mapMaybe⁻-nothing`?

Exactly, I find it odd that ∈-mapMaybe⁻-nothing now does a case analysis of the membership proof returned by ∈-mapMaybe⁻ (via aux); it's not just "gymnastics" performing the same proof, it is a different proof in spirit.

[jamesmckinna]

I agree they are different proofs! But I think my analysis above of the real problem lies in the strictness of inspect; the gymnastics are required in order to offer an analysis in harmony with the 'lazier' definition using with ... in ...... I think?

[jamesmckinna]

A weird anomaly (is it a 'bug'? not sure, but it's weird):

inspect : {A : Set a} {B : A → Set b} →
                 (f : (x : A) → B x) (x : A) →
                 Reveal f · x is f x
inspect f a = let eq = refl {x = f a} in [ eq ]

is fine... whereas

strict-inspect : {A : Set a} {B : A → Set b} →
                 (f : (x : A) → B x) (x : A) →
                 Reveal f · x is f x
strict-inspect f a = let eq@refl = refl {x = f a} in [ eq ]

is not, because the attempt to match/constrain eq against refl fails in the absence of the K axiom...

Related:

pattern explicit-refl f a = refl {x = .(f a)}

fails because dotted patterns aren't allowed in pattern synonyms, while

pattern inspect-refl f a = refl

fails because the variables f and a are not used.

So it seems that the old library definition of inspect occupies a very peculiar sweet spot, being definitionally equal to refl, yet neither a priori matchable against refl, nor replaceable by a pattern synonym based on refl. Am I alone in finding this weird?

[jamesmckinna]

Hmmm... I've been playing a bit more, and you still won't like it, I'm sure, but here goes as the 'simplest' version I can offer:

-- warm-up exercise, exhibiting reduction behaviour in `y∈`

  ∈-mapMaybe⁻-nothing-∈-mapMaybe⁺ : (y∈ : y ∈ mapMaybe f (x ∷ xs)) →
    f x ≡ nothing → y ∈ mapMaybe f xs
  ∈-mapMaybe⁻-nothing-∈-mapMaybe⁺ y∈ fx≡nothing
    rewrite fx≡nothing = y∈

-- tidier version of 'impossible' lemma

  ∈-mapMaybe⁻-nothing : (y∈ : y ∈ mapMaybe f (x ∷ xs)) →
                        (fx≡nothing : f x ≡ nothing) →
                        Is-there ((∈-mapMaybe⁻ y∈) .proj₂ .proj₁)
  ∈-mapMaybe⁻-nothing y∈ fx≡nothing
    with ∈-mapMaybe⁻ y∈
  ... | x , here refl , fx≡just[y] with nothing ← f x | () ← fx≡just[y]
  ... | z , there y∈′ , fz≡just[y] = _

This seems to be the best I can do, and corresponds, as you say, not to your original 'computational' proof, which uses the equation fx≡nothing to make progress in evaluating mapMaybe and hence also ∈-mapMaybe⁻ y∈, but instead to a McCarthy-style 'induction on the computation of ∈-mapMaybe⁻ y∈'... which still leaves us with two clauses.

The first, failing case, is when z = x (by refl, and here, for some reason, it is OK to cut in the irrefutable pattern nothing ← f x (proxying for a forbidden rewrite fx≡nothing, but NB the scope of x has moved inwards: so the match on f x is, in some sense, fresh wrt fx≡nothing), leaving the now impossible equation fx≡just[y] (but I can't seem to sequence any of these steps in any more 'natural' order, possibly because of the just-observed scoping)

The second is the customary success case that 'just works', and so we're done.

So... still puzzling... I'm certainly still puzzled!!!

UPDATED: the mistake, perhaps, is to introduce fx≡nothing too soon (!?)... delaying it produces instead

  ∈-mapMaybe⁻-nothing : (y∈ : y ∈ mapMaybe f (x ∷ xs)) →
                        (fx≡nothing : f x ≡ nothing) →
                        Is-there ((∈-mapMaybe⁻ y∈) .proj₂ .proj₁)
  ∈-mapMaybe⁻-nothing y∈ with z , z∈ , fz≡just[y] ← ∈-mapMaybe⁻ y∈ | z∈
  ... | here refl rewrite fz≡just[y] = λ ()
  ... | there _ = λ _ → _

... FWIW

[jamesmckinna]

Aaargh: #6841 the saga continues...