boolean eval and equality

Stream: lean4

[Siddhartha Gadgil]

I have a situation where a Boolean expression quickly evaluates to false but proving this is false by rfl has a timeout because of trying to compute the whnf of the expression.

#eval eg1Soln.isSat                                                              -- false

theorem eg1false : eg1Soln.isSat = false := by rfl   -- timeout

I know that whnf of eg1Soln is huge and does timeout for good reason. My question is can I use the information used in eval to prove stuff, i.e., avoid computing the whnf fully to use rfl.

The type of egSoln is an inductive type with two constructors, with eg1Soln.isSat depending only on which constructor was used. This is picked up by eval but unfortunately rfl` tries to fully simplify the expression and times out.

I also tried using by decide, which again did not use the evaluation.

Thanks for any help and clarifications.

[Kevin Buzzard]

Can you prove a theorem and rewrite it instead of relying on rfl?

[Siddhartha Gadgil]

Not in an obvious way (though I can try this idea).

[Siddhartha Gadgil]

Unless I work around this issue, or there is a way to use eval (I see from the source that the implementation is unsafe), it seems that something will have to be simplified by using rfl and eg1falseabove seems as simple as it gets.

[Sebastian Ullrich]

There is https://github.com/leanprover/lean4/blob/f45bfaffdf938dd7411398c0bb774ad2e39bc236/src/Init/Core.lean#L1039-L1071, which you can use via the nativeDecide tactic. But from your description, it is not clear to me why rfl has to do exorbitantly more work; it should not need to reduce irrelevant constructor arguments.