Stream: Is there code for X?
Topic: an abel-like tactic for nat?
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?
Adam Topaz (Oct 22 2020 at 00:10):
These aren't so trivial because of the subtraction :oh_no:
Adam Topaz (Oct 22 2020 at 00:11):
For example the second one is false when
i is larger than
Adam Topaz (Oct 22 2020 at 00:12):
nats, of course)
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
Adam Topaz (Oct 22 2020 at 00:17):
(can't seem to find it though...)
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