Zulip Chat Archive

Stream: general

Topic: apply_rules vs solve_by_elim


view this post on Zulip Johan Commelin (May 15 2020 at 19:22):

Do I understand correctly that apply_rules and solve_by_elim are somewhat similar? Is the idea that apply_rules is some sort of solve_by_elim only [...]? And solve_by_elim comes with a default set of rules, but apply_rules doesn't?

view this post on Zulip Scott Morrison (May 16 2020 at 02:28):

apply_rules doesn't do any backtracking.

view this post on Zulip Scott Morrison (May 16 2020 at 02:28):

Once a lemma has been applied on a particular goal, it won't go back to try other lemmas on that goal if it fails to discharge subsequent subgoals.

view this post on Zulip Scott Morrison (May 16 2020 at 02:30):

(And of course this brings an advantage: it can succeed without discharging all the subgoals, whereas solve_by_elim is a finishing tactic.)

view this post on Zulip Scott Morrison (May 16 2020 at 02:30):

We should add some doc-strings to this effect!

view this post on Zulip Johan Commelin (May 16 2020 at 03:42):

@Scott Morrison Aha, thx for explaining

view this post on Zulip Scott Morrison (May 16 2020 at 07:30):

#2696


Last updated: May 14 2021 at 22:15 UTC