Definitional reduction

Stream: general

[Moses Schönfinkel]

If I can #eval f a b to tt, should I make sure that example : f a b = ttis rfl? In my case, b = g a and g seems to be naughty enough for Lean being to unwilling to expand everything. (f a a = tt is indeed rfl)

[Simon Hudon]

This may be a case where you suffer from the fact that definitional equality is not transitive.

[Moses Schönfinkel]

Let's suppose #reduce f x evaluates to tt. Is there a general easy way to prove example : f x = tt if rfl doesn't get the job done (probably due to non-transitive defeq)?

[Mario Carneiro]

If #reduce works, then rfl should also

[Moses Schönfinkel]

Would there by any difference between #eval and #reduce?

[Mario Carneiro]

yes, the same statement doesn't hold if you use #eval

[Mario Carneiro]

there are some terms that #eval can evaluate which #reduce gets stuck on due to axioms like propext

[Moses Schönfinkel]

I would love to at least try #reduce but deterministic timeout is making it somewhat impossible. I am pretty sure everything I use is fairly computable tho. Should I just write a tactic that unfolds everything explicitly until refl or should I try to find a way to make the whole thing rfl? (In the case where #eval f x yields tt but f x = tt is not rfl.)