Zulip Chat Archive

Stream: Is there code for X?

Topic: an abel-like tactic for nat?


view this post on Zulip Eric Wieser (Oct 22 2020 at 00:04):

I keep finding myself with trivial goals to prove like k - i = (j - i) + (k - j) and j = i + (j - i), where all my variables are nats. Is there a tactic that will close these goals and introduce any inequalities that it needed to solve them?

view this post on Zulip Adam Topaz (Oct 22 2020 at 00:10):

These aren't so trivial because of the subtraction :oh_no:

view this post on Zulip Adam Topaz (Oct 22 2020 at 00:11):

For example the second one is false when i is larger than j

view this post on Zulip Adam Topaz (Oct 22 2020 at 00:12):

(assuming both i and j are nats, of course)

view this post on Zulip Adam Topaz (Oct 22 2020 at 00:15):

There was some discussion about subtraction in nat at some point on zulip that might be relevant

view this post on Zulip Adam Topaz (Oct 22 2020 at 00:17):

(can't seem to find it though...)

view this post on Zulip Bryan Gin-ge Chen (Oct 22 2020 at 00:19):

Maybe there's a way to modify tactic#zify so that it introduces any necessary hypotheses?


Last updated: May 17 2021 at 16:26 UTC