Zulip Chat Archive

Stream: new members

Topic: a way to try a tactic and "no-op"


view this post on Zulip Eric Rodriguez (Feb 25 2021 at 18:45):

So for example, I apply mul_lt_mul and I get four goals; 3 of them are easily provable by assumption;, but one isn't. What I want to do is something like apply mul_lt_mul; assumption, and then deal with the last case. However, assumption errors here; is there a way to just ignore that?

view this post on Zulip Eric Wieser (Feb 25 2021 at 18:46):

tactic#try

view this post on Zulip Eric Rodriguez (Feb 25 2021 at 18:47):

thanks!

view this post on Zulip Eric Rodriguez (Feb 25 2021 at 18:48):

wait, no, that doesn't work; it solves the first goal and then gives up after the goal that errors

view this post on Zulip Eric Rodriguez (Feb 25 2021 at 18:50):

wait no I'm being silly sorry!

view this post on Zulip Eric Wieser (Feb 25 2021 at 18:59):

Of course, another approach would just be to add have : last_goal, {...} before you apply, and then assumption will succeed :)

view this post on Zulip Damiano Testa (Feb 25 2021 at 20:00):

Also, any_goals { [...] }, applies [...] to any unsolved goal, failing only if what you feed it makes progress nowhere.

view this post on Zulip Yakov Pechersky (Feb 25 2021 at 20:06):

For others, an example:

import data.nat.basic

example {a b c d : } (h : a < c) (h' : b  d) (hb : 0 < b) : a * b < c * d :=
begin
  apply mul_lt_mul;
  try { assumption },
  exact (show 0  c, from sorry)
end

Last updated: May 12 2021 at 22:15 UTC