loogle miss

Stream: mathlib4

[Jireh Loreaux]

Why doesn't @loogle (∀ y, inner ?x y = inner ?z y), ?x = ?z

find docs#ext_inner_right here?

[loogle]

:shrug: nothing found

[Floris van Doorn]

@loogle (∀ y, inner ?x y = inner ?z y) -> ?x = ?z

[loogle]

:search: ext_inner_right

[Floris van Doorn]

That doesn't answer your question. I don't your the answer.

[Floris van Doorn]

I expect that Loogle doesn't like this quantifier as head of an expression. This also works:
@loogle inner _ ?y = inner _ ?y

[loogle]

:search: ext_inner_right, ext_inner_map, and 4 more

[Floris van Doorn]

(@Joachim Breitner )

[Joachim Breitner]

(∀ y, inner ?x y = inner ?z y) is equivalent to (y : ?x) → inner ?x y = inner ?z y. I would have assumed that this would be equivalent to searching for inner ?x ?y = inner ?z ?y and then finding a hypothesis matching ?x, but it seems that this somewhere doesn't work.

So I don’t your the answer either.

[Joachim Breitner]

But using the same metavariables on independent filters (the comma-separated things) doesn’t do what you want it to do anyways. Likely loogle should warn about this. If you want the metavariable to scope that way, you have to put them into one expression, like Floris did.

[Eric Wieser]

does P -> R match expressions of the form P -> Q -> R?

[Eric Wieser]

Because if not, then that's often a reason for wanting to use independent filters

[Joachim Breitner]

Eric Wieser said:

does P -> R match expressions of the form P -> Q -> R?

It should

[Joachim Breitner]

If the pattern has parameters, they are matched in any order. Both of these will find List.map:
:search: (?a -> ?b) -> List ?a -> List ?b
:search: List ?a -> (?a -> ?b) -> List ?b

[Joachim Breitner]

@loogle (?a -> ?b) -> List ?b

[loogle]

:search: List.modifyHead, List.map, and 20 more

[Michael Stoll]

@loogle ∀ x < ?a, x < ?b → ?a ≤ ?b

[loogle]

:shrug: nothing found

[Michael Stoll]

But: docs#le_of_forall_lt :

theorem le_of_forall_lt {α : Type u_2} [LinearOrder α] {a b : α} (H : ∀ (c : α), c < a → c < b) :
a ≤ b

Why does Loogle miss this?

[Edward van de Meent]

brackets, i think?

[Edward van de Meent]

@loogle (∀ x < ?a, x < ?b) → ?a ≤ ?b

[loogle]

:search: le_of_forall_lt

[Edward van de Meent]

without, it interprets it as ∀ x < ?a, (x < ?b → ?a ≤ ?b) which seems to say that all elements less than a are minimal?

[Edward van de Meent]

that doesn't quite seem to describe all consequences, but it's a decent start

[Edward van de Meent]

maybe a better description is "a is the successor of all elements strictly smaller than it"