Zulip Chat Archive

Stream: general

Topic: Definitional reduction


Moses Schönfinkel (Jun 04 2018 at 07:14):

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 (Jun 04 2018 at 11:38):

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

Moses Schönfinkel (Jun 05 2018 at 19:37):

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 (Jun 05 2018 at 19:38):

If #reduce works, then rfl should also

Moses Schönfinkel (Jun 05 2018 at 19:39):

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

Mario Carneiro (Jun 05 2018 at 19:39):

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

Mario Carneiro (Jun 05 2018 at 19:40):

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

Moses Schönfinkel (Jun 05 2018 at 19:44):

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.)


Last updated: Dec 20 2023 at 11:08 UTC