Zulip Chat Archive

Stream: new members

Topic: using #reduce and #eval in proofs?


view this post on Zulip Jason Gross (Jul 21 2020 at 19:43):

Is there a way to use the output of #reduce and/or #eval in defining a constant without copy/paste? def foo : ℕ := #reduce (0 + 1) gives error: invalid expression, unexpected token and warning: declaration 'foo' uses sorry

view this post on Zulip Kenny Lau (Jul 21 2020 at 19:48):

#eval is unsafe and/so it is faster and/so you basically can't use it (usually norm_num works in this situation)

view this post on Zulip Kenny Lau (Jul 21 2020 at 19:48):

#reduce is as fast/slow as rfl

view this post on Zulip Kenny Lau (Jul 21 2020 at 19:49):

note that 0 + 1 already defines a natural number, so you don't need to reduce it

view this post on Zulip Kenny Lau (Jul 21 2020 at 19:49):

how you could use it would be theorem foo : 0 + 1 = [copy result of #reduce] := rfl

view this post on Zulip Kenny Lau (Jul 21 2020 at 19:49):

and theorem foo : 0 + 1 = [copy result of #eval] := by norm_num

view this post on Zulip Jason Gross (Jul 21 2020 at 19:52):

norm_num has asymptotically quadratic performance in the size of the term I'm building (even though my algorithm is obviously linear) and so seems to be unsuitable (maybe I'm using it wrong). I want a replacement for something like theorem foo : Σ v, v = 0 + 1 := by { eapply sigma.mk, norm_num } which is faster


Last updated: May 11 2021 at 14:11 UTC