A question about Lean: maxHeartbeats

Stream: Equational

[Zoltan A. Kocsis (Z.A.K.)]

I'm struggling to formalize 1701_not_implies_4587. I have to go into deeply nested match ... with statements, and then the Lean tactics just seem to give up (I think it's a less artificial version of this issue).

I did hit the same issue in 1661 but I could work around it by proving strategic lemmata and using them in preemptive rewrites. But that doesn't work here: I hit "(deterministic) timeout at elaborator, maximum number of heartbeats (200000) has been reached" even when trying to use the exact tactic to prove a term with no free variables.

Is it acceptable to use set_option maxHeartbeats <num> to increase the limit? (And if I do it, will it affect the whole project, or just the current file, or just the next proof, or what? The docs proved surprisingly useless for answering this question.)

[Daniel Weber]

You can use set_option maxHeartbearts 400000 in theorem ..., and then it's only that theorem

[Zoltan A. Kocsis (Z.A.K.)]

Thanks! Can this come back to bite me later in some way (I assume it was set at the current number for a reason)?

[Daniel Weber]

I think it mostly has its value to prevent proofs getting stuck in really long loops, and to encourage people to split slow theorems to multiple ones. If you can't/it will be a lot of effort to split the theorem to lemmas I think it's best to just increase maxHeartbearts

[Shreyas Srinivas]

It will increase the elaboration time of the proof, but if you can't avoid it then do please use the local option Daniel has suggested

[Shreyas Srinivas]

Is this an auto-generated proof?

[Shreyas Srinivas]

Also, if you use set_option trace.profiler true you might be able to find out which parts are time consuming.

[Zoltan A. Kocsis (Z.A.K.)]

Is this an auto-generated proof?

No, it just naturally falls into a lot of case distinctions. If you look in InfModel_1661 you'll see a similar argument. There, I could get around the issue by creating a couple of the lemmas that I used in my initial pen-and-paper sketch of the argument (op_right_even and the ilk), and use them in strategic rewrites, which cuts down the work enough that I don't get the elaborator heartbeat error.

Unfortunately, this approach does not work in the more complicated case distinctions required for this case of 1701. I introduced a lot of small lemmas to speed things up. But it didn't work: I gave up when even trying to do an rw with

private lemma op_left_cache :
  op_1701_4587 (op_1701_4587 3 4) 4 = 5 := by simp [op_1701_4587]

which, as you see, does not have free variables, triggered the error.

It will increase the elaboration time of the proof, but if you can't avoid it then do please use the local option Daniel has suggested

I think what I want to do is "tell Lean to check the cases" here, really. The insight was in the construction, not in the particular verification, and spending too much time writing the proofs would take time away from finding new ones, which is more productive at this stage. The long-term solution is probably a custom macro or a custom tactic, but I can do proof engineering work later, when the implications are resolved. So unless there are other objections, I'll go with "shorter proofs, more heartbeats" for now, and maybe create an issue to find better ways to do this proof./

Thanks for your help both!

[Notification Bot]

Zoltan A. Kocsis (Z.A.K.) has marked this topic as resolved.

[Shreyas Srinivas]

Let me check this lemma and see if I can reduce the proof length time.

[Shreyas Srinivas]

*proof elaborating time

[Shreyas Srinivas]

Which PR is this?

[Zoltan A. Kocsis (Z.A.K.)]

Much appreciated, but it's not a PR yet (only 2 of the 3 proofs are finished). It'll be a PR in about 10 hours, as I have something else to do this morning.

[Zoltan A. Kocsis (Z.A.K.)]

I'll ping you when it's up!

[Zoltan A. Kocsis (Z.A.K.)]

@Shreyas Srinivas I put up the currently completed proofs here so that you can take a look in the meantime if you're feeling up for it.

They're in equational_theories/InfModel_1701.lean, it is private theorem op_1701_4587_satisfies_1701 which is causing me trouble.

[Zoltan A. Kocsis (Z.A.K.)]

I didn't have time to rebase over current main, but I expect no issues.

[Shreyas Srinivas]

thanks. let's see if I have any luck with it

[Notification Bot]

ChunHao Peng has marked this topic as unresolved.

[Mario Carneiro]

have these proofs landed yet, or are they on a branch? I can take a look if you have a messy proof you are having performance problems with

[Shreyas Srinivas]

Yeah they have landed

[Shreyas Srinivas]

See : https://github.com/teorth/equational_theories/blob/main/equational_theories/InfModel_1701.lean

[Shreyas Srinivas]

Specifically here : https://github.com/teorth/equational_theories/blob/a7ada1c2a4979134357893fef2239abde6d2eba1/equational_theories/InfModel_1701.lean#L352

[Shreyas Srinivas]

Meanwhile I will shorten the counterexample proofs in equational#573

[Shreyas Srinivas]

Also @Zoltan A. Kocsis (Z.A.K.) : I would like to move the files you have created inside the ManuallyProved folder

[Mario Carneiro]

is there a high level explanation of the proof? The comments seem to refer to one

[Zoltan A. Kocsis (Z.A.K.)]

(Again, this should probably move to a different thread, I propose this one:
#Equational > A question about Lean: maxHeartbeats

[Mario Carneiro]

(you can move messages)

[Zoltan A. Kocsis (Z.A.K.)]

@Mario Carneiro : Thanks for looking into this. In an ideal world, there would not be much to any of the proofs in InfModel_XXXX.lean (including the one in PR#573). All of these results can be proven by

1. Do a case analysis on both arguments. There are some special cases (those constants which appear in the definition of the op). Do a case analysis on the parities of both arguments.
2. Compute using the parities and the op.

[Notification Bot]

9 messages were moved here from #Equational > 1648 !=> 206 by Zoltan A. Kocsis (Z.A.K.).

[Notification Bot]

3 messages were moved here from #Equational > A question about Lean: maxHeartbeats by Zoltan A. Kocsis (Z.A.K.).

[Notification Bot]

3 messages were moved here from #Equational > 1648 !=> 206 by Zoltan A. Kocsis (Z.A.K.).

[Zoltan A. Kocsis (Z.A.K.)]

@Mario Carneiro : Advance warning just in case you decided to work on these, PR #579 will move the InfModel_*.lean files to the ManuallyProved/ directory.