loogle doesn't find dependent function with `?α → ?β`

Stream: mathlib4

[Jireh Loreaux]

@Joachim Breitner Is the following expected behavior for Loogle?

[Jireh Loreaux]

@loogle ⊢ TopologicalSpace.SeparableSpace (?α → ?β)

[loogle]

:shrug: nothing found

[Jireh Loreaux]

@loogle ⊢ TopologicalSpace.SeparableSpace ((i : ?α) → ?β i)

[loogle]

:search: TopologicalSpace.instSeparableSpaceForAllTopologicalSpace

[Joachim Breitner]

Hmm, I don’t claim that there isn’t some amount of accidentialy here, but I would argue that it could be somewhat intentional. The metavariable ?β is introduced outside any local scopes, so it won’t unify with something mentioning local variables. Or put differently, ?α → ?β looks like a non-dependent arrow, so it's not wrong to reject that.

But I admit I am rationalizing :-)

[Joachim Breitner]

It matches what conv => pattern does, for example:

example : ((n : Nat) → Fin n) = ((n : Nat) → Fin n.succ) := by
  -- does not work:
  -- conv => pattern (?a → ?b)
  conv => pattern ((i : ?a) → ?b i)

[Jireh Loreaux]

That feels a bit like a bug, but I'll accept that it possibly needs to be this way. I just tried to think through in my head a way to get the second query out of the first, but it seems infeasible in general (unless you implement explicit support for exactly "is this subexpression of the form metavariable → metavariable? If so, replace it with a dependent one").

[Joachim Breitner]

I agree it’s not perfect yet.

[Joachim Breitner]

⊢ TopologicalSpace.SeparableSpace ((_ : _) → _)

works too.

[Floris van Doorn]

Loogle's behavior seems like the desired behavior to me.