Zulip Chat Archive

Stream: Is there code for X?

Topic: loogls vs. 0

Joachim Breitner (Oct 17 2023 at 09:10):

Mario Carneiro said:

Joachim Breitner any idea why this doesn't work:

loogle 0 ≤ ?a * ?a

No, not directly. _ ≤ ?a * ?a works (after a long wait, unsurprisingly), so it seems to be related to the 0.
In fact, _ ≤ ?a * ?a, 0 doesn't work, while _ ≤ ?a * ?a, OfNat.ofNat works again.

So the problem is not the index (the lemma is among the “Found 1399 definitions mentioning HMul.hMul, LE.le and OfNat.ofNat”), but somehow the pattern 0 is elaborated into something that doesn't match docs#mul_self_nonneg…

Joachim Breitner (Oct 17 2023 at 09:21):

On the joachim/find branch (has a warm cache, so don’t hesitate :-)) this reproduces the issue:

import Mathlib

open Mathlib.Tactic.Find
open Lean Elab Command

-- #find 0 ≤ ?a * ?a, "mul_self_nonneg"

elab s:"#assert_match " name_s:ident concl:(turnstyle)? query:term : command => liftTermElabM do
    -- let pat ← Lean.Elab.Term.elabTerm query none
    let pat ← Mathlib.Tactic.Find.elabTerm' query none
    let name := Lean.TSyntax.getId name_s
    let matcher ←
      if concl.isSome
      then matchConclusion pat
      else matchAnywhere pat
    let c := (← getEnv).constants.find! name
    logInfoAt query m!"Pattern: {pat}"
    logInfoAt name_s m!"Const type: {c.type}"
    unless ← matcher c do
      logErrorAt s "Pattern does not match when it should!"

#assert_match mul_self_nonneg 0 ≤ ?a * ?a

It works fine if I use Lean.Elab.Term.elabTerm instead of Mathlib.Tactic.Find.elabTerm'. The latter is defined as

/-- A variant of `Lean.Elab.Term.elabTerm` that does not complain for example
when a type class constraint has no instances.  -/
def elabTerm' (t : Term) (expectedType? : Option Expr) : TermElabM Expr := do
  withTheReader Term.Context ({ ·  with ignoreTCFailures := true, errToSorry := false }) do
    let t ← Term.elabTerm t expectedType?
    Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
    return t

With the plain elabTerm I get

@OfNat.ofNat ?m.4722 0 ?m.4678 : ?m.472

for 0 which then matches fine; with elabTerm' I get

@OfNat.ofNat ℕ 0 (instOfNatNat 0) : ℕ

which may explain why it does not match the @OfNat.ofNat α 0 Zero.toOfNat0 : α in the lemma type.

Maybe someone can tell me how to adjust elabTerm' to fix this? Why does it want to specialize to Nat here when I didn’t ask for it?

Mario Carneiro (Oct 17 2023 at 09:25):

Why does it want to specialize to Nat here when I didn’t ask for it?

That's @[default_instance] kicking in

Eric Wieser (Oct 17 2023 at 09:27):

@loogle (0 : ?b) ≤ ?a * ?a

loogle (Oct 17 2023 at 09:27):

:shrug: nothing found

Joachim Breitner (Oct 17 2023 at 09:28):

Can I tell the elaborator that I don’t want any defaulting?

Mario Carneiro (Oct 17 2023 at 09:29):

If you set mayPostpone := true then it won't use default instances

Joachim Breitner (Oct 17 2023 at 09:30):

Let me try that, I wonder if that flag was set for some other reason here.

Joachim Breitner (Oct 17 2023 at 09:35):

At least my rudimentary test suite passes :-)
I’ll try that, and wait for reports about what broke…

Thanks for the help!

Joachim Breitner (Oct 17 2023 at 09:38):

(I got the elabTerm' originally from https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/meta.20variable.20confusion/near/387525132, but maybe the mayPostpone := false wasn’t important to fix the issue there.)

Joachim Breitner (Oct 17 2023 at 10:48):

This works now:
@loogle |- 0 ≤ ?a * ?a

loogle (Oct 17 2023 at 10:48):

Failure! Bot is unavailable

Joachim Breitner (Oct 17 2023 at 10:48):

The variant without |- times out with

(deterministic) timeout at 'isDefEq', maximum number of heartbeats (200000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

Joachim Breitner (Oct 17 2023 at 10:48):

@loogle |- 0 ≤ ?a * ?a

loogle (Oct 17 2023 at 10:49):

Failure! Bot is unavailable

Joachim Breitner (Oct 17 2023 at 10:49):

Odd.
@loogle |- 0 ≤ ?a * ?a

loogle (Oct 17 2023 at 10:49):

Failure! Bot is unavailable

Joachim Breitner (Oct 17 2023 at 10:50):

Maybe I was just racing with someone else using the bot. Last try:
@loogle |- 0 ≤ ?a * ?a

loogle (Oct 17 2023 at 10:51):

Failure! Bot is unavailable

Joachim Breitner (Oct 17 2023 at 10:52):

It seems it’s just too slow for zulip’s 5s timeout. But https://loogle.lean-lang.org/?q=%7C-+0+%E2%89%A4+%3Fa+*+%3Fa gives it.

Mario Carneiro (Oct 17 2023 at 10:52):

Is the bot able to differentiate between a missing connection and a timeout?

Mario Carneiro (Oct 17 2023 at 10:53):

maybe you need a less (deterministic) timeout

Joachim Breitner (Oct 17 2023 at 10:53):

It’s not the bot, it’s the zulip server. I think it’s a timeout in all these cases.

Mario Carneiro (Oct 17 2023 at 10:53):

and a more wall-clock based one

Mario Carneiro (Oct 17 2023 at 10:54):

isn't the bot the one that says the bot is unavailable?

Joachim Breitner (Oct 17 2023 at 10:54):

Yes, the python server wrapper could be more zulip-friendly here. Contributions welcome, if someone feels like dealing with concurrent programming and cross-process communication in python :-)

Mario Carneiro (Oct 17 2023 at 10:54):

which I suppose is confusing in itself, there are I guess two bots involved

Joachim Breitner (Oct 17 2023 at 10:55):

No, the zulip server, when the bot (my server) doesn’t respond fast enough. I could also make my server post the response via POST, then there would be no timeout… maybe I’ll do that.

Joachim Breitner (Oct 17 2023 at 13:47):

I wonder whether it has to be so slow, or if isDefEq is doing some unnecessary or unwanted steps, such as trying to solve type class constraints or so.

Looking at

import Mathlib

set_option trace.Meta.isDefEq true in
set_option trace.Meta.isDefEq.assign true in
#find 0 ≤ ?a * ?a, "mul_self_nonneg", LinearOrderedRing

I see

Scratch3.lean:5:6
[Meta.isDefEq] 💥 OfNat ?m.3 0 =?= OfNat ℕ+ (?m.10 + 1) ▶

[Meta.isDefEq] 💥 OfNat ?m.3 0 =?= OfNat ℕ+ (?m.17 + 1) ▶

[Meta.isDefEq] 💥 OfNat ?m.3 0 =?= OfNat ℕ+ (?m.28 + 1) ▶

[Meta.isDefEq] 💥 OfNat ?m.49 0 =?= OfNat ℕ+ (?m.130 + 1) ▶

[Meta.isDefEq] 💥 OfNat ?m.49 0 =?= OfNat ℕ+ (?m.227 + 1) ▶
Scratch3.lean:5:6
[Meta.isDefEq] ✅ ?m.31 =?= ?m.3 ▶

[Meta.isDefEq] ✅ ?m.3 =?= ?m.49 ▶

[Meta.isDefEq] ✅ ?m.49 =?= ?m.49

[Meta.isDefEq] 💥 LE ?m.49 =?= LE (Set ?m.124) ▶

[Meta.isDefEq] 💥 LE ?m.49 =?= LE (Set ?m.222) ▶

[Meta.isDefEq] 💥 LE ?m.49 =?= LE (Set ?m.314) ▶
Scratch3.lean:5:10
[Meta.isDefEq] ✅ ?m.22 =?= ?m.29 ▶

[Meta.isDefEq] ✅ ?m.29 =?= ?m.30 ▶

[Meta.isDefEq] 💥 HMul ?m.30 ?m.30
      ?m.33 =?= HMul (MonoidAlgebra ?m.42 ?m.43)
      (Representation.asModule (Representation.ofMulAction ?m.42 ?m.43 ?m.43)) (MonoidAlgebra ?m.42 ?m.43) ▶

[Meta.isDefEq] 💥 HMul ?m.30 ?m.30
      ?m.133 =?= HMul (MonoidAlgebra ?m.142 ?m.143)
      (Representation.asModule (Representation.ofMulAction ?m.142 ?m.143 ?m.143)) (MonoidAlgebra ?m.142 ?m.143) ▶

[Meta.isDefEq] 💥 HMul ?m.30 ?m.30
      ?m.228 =?= HMul (MonoidAlgebra ?m.237 ?m.238)
      (Representation.asModule (Representation.ofMulAction ?m.237 ?m.238 ?m.238)) (MonoidAlgebra ?m.237 ?m.238) ▶
Scratch3.lean:5:0
Found 17 definitions mentioning HMul.hMul, LinearOrderedRing, LE.le and OfNat.ofNat.
Of these, 1 have a name containing "mul_self_nonneg".
Of these, 1 match your patterns.
• mul_self_nonneg
Scratch3.lean:5:0
[Meta.isDefEq] ✅ 0 ≤ a * a =?= 0 ≤ ?m.335 * ?m.335 ▶

and I am a bit surprised to see mention of MonoidAlgebra, or OfNat ?m.3 0 =?= OfNat ℕ+ (?m.10 + 1), or LE (Set…) here. It seems to be performing some kind of search.

Any ideas what isDefEq is doing here?

Matthew Ballard (Oct 17 2023 at 13:56):

What does trace.Meta.synthInstance say? Also should I be able to copy and paste that code?

Joachim Breitner (Oct 17 2023 at 14:07):

On branch joachim/find you should (has a working cache, so should be quick)

Joachim Breitner (Oct 17 2023 at 14:11):

It does try to synth instances for PNat:

[Meta.synthInstance] 💥 OfNat ?m.3 0 ▼
  [] new goal OfNat ?m.3 0 ▶
  [] 💥 apply instOfNatPNatHAddNatInstHAddInstAddNatOfNat to OfNat ?m.3 0 ▶

[Meta.synthInstance] 💥 OfNat ?m.3 0 ▼
  [] new goal OfNat ?m.3 0 ▶
  [] 💥 apply instOfNatPNatHAddNatInstHAddInstAddNatOfNat to OfNat ?m.3 0 ▶

[Meta.synthInstance] 💥 OfNat ?m.3 0 ▼
  [] new goal OfNat ?m.3 0 ▶
  [] 💥 apply instOfNatPNatHAddNatInstHAddInstAddNatOfNat to OfNat ?m.3 0 ▶

[Meta.synthInstance] 💥 OfNat ?m.49 0 ▼
  [] new goal OfNat ?m.49 0 ▶
  [] 💥 apply instOfNatPNatHAddNatInstHAddInstAddNatOfNat to OfNat ?m.49 0 ▶

[Meta.synthInstance] 💥 OfNat ?m.49 0 ▼
  [] new goal OfNat ?m.49 0 ▶
  [] 💥 apply instOfNatPNatHAddNatInstHAddInstAddNatOfNat to OfNat ?m.49 0 ▶

and

[Meta.synthInstance] 💥 HMul ?m.30 ?m.30 ?m.31 ▼
  [] new goal HMul ?m.30 ?m.30 _tc.0 ▶
  [] 💥 apply @Representation.instHMulMonoidAlgebraToSemiringAsModuleFinsuppToZeroToCommMonoidWithZeroToMonoidToDivInvMonoidAddCommMonoidToAddCommMonoidToNonUnitalNonAssocSemiringToNonAssocSemiringModuleToModuleOfMulActionToMulAction to HMul
        ?m.30 ?m.30 ?m.33 ▶

Nice instance name… is that intentional?

Matthew Ballard (Oct 17 2023 at 14:13):

cache is misbehaving.

That name is tame compared to some. lean4#2343

Joachim Breitner (Oct 17 2023 at 14:16):

Oh, how annoying that the cache doesn't work.

Joachim Breitner (Oct 17 2023 at 14:27):

But you might be on the right track, with it seems that most time is spent in instance inference:

So the question is why isDefEq is even trying to infer instances here, and if really has to, and if not, how it can be told not to.

Last updated: Dec 20 2023 at 11:08 UTC