Loogle and iff_of_eq

Stream: general

[Henrik Böving]

I have a query that takes quite a long time and has an interesting result:

[Henrik Böving]

@loogle ?a = ?b -> (?a <-> ?b)

[loogle]

Failure! Bot is unavailable

[Henrik Böving]

Ah well it even times the bot out :D in the web UI we get:

    Iff.of_eq Init.Core
    ∀ {a b : Prop}, a = b → (a ↔ b)
    iff_of_eq Std.Logic
    ∀ {a b : Prop}, a = b → (a ↔ b)
    Eq.to_iff Std.Logic
    ∀ {a b : Prop}, a = b → (a ↔ b)

do we have plans to deduplicate this type of stuff eventually ?

[Henrik Böving]

Uh and this one: https://loogle.lean-lang.org/?q=%28%3Fa+-%3E+%3Fb%29+%3D+%28%3Fc+-%3E+%3Fd%29 throws a 502.

[Kevin Buzzard]

I think iff_of_eq and Eq.to_iff are both allowed (naming convention, dot notation)?

[Joachim Breitner]

It's not surprising it takes a long time: there are many theorems with iff and eq around. I don't see immediate low hanging fruit to improve that. Writing a query with |- can help a bit with speed.

[Mario Carneiro]

Iff.of_eq is also a legal dot-notation lemma (since in lean 4 you can make use of dot-notation for either an argument or the conclusion)

[Mario Carneiro]

it might be a good idea to use alias though to make it clear that the duplication is deliberate

[Joachim Breitner]

Henrik Böving said:

Uh and this one: https://loogle.lean-lang.org/?q=%28%3Fa+-%3E+%3Fb%29+%3D+%28%3Fc+-%3E+%3Fd%29 throws a 502.

That’s (?a -> ?b) = (?c -> ?d). Had to paste that into an URL decoder :-)

That query only has Eq to index by, so it sequentially goes through every lemma that has an equality. Locally I get the heartbeat timeout. I guess you’d see this as an error message if the nginx proxy was just a bit more patient, or the loogle host faster.

~/projekte/programming/loogle $ time lake exe loogle --read-index  ./lake-packages/mathlib/build/lib/MathlibExtras/Find.extra '(?a -> ?b) = (?c -> ?d)'
(deterministic) timeout at 'whnf', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

real    0m9,904s
user    0m9,411s
sys 0m0,515s

[Joachim Breitner]

A quick look at the flame graph of running loogle doesn't reveal any low-hanging fruit or unexpected time spent there, but I don't have much experience with these flame graphs. And continuation-passing style (e.g. with docs#Lean.Meta.withNewLocalInstances) obscures things a bit.

[Joachim Breitner]

You’ll now get a proper error message for the (?a -> ?b) = (?c -> ?d) query – after about 80s. (I bumped the proxy timeout.)