Zulip Chat Archive

Stream: general

Topic: how to use `solve_by_elim`


view this post on Zulip Chris Hughes (Aug 17 2018 at 16:48):

What is the syntax for giving solve_by_elim a discharger. I tried solve_by_elim `[cc] like the docs suggest, but I couldn't get it to work.

view this post on Zulip Simon Hudon (Aug 17 2018 at 16:50):

That would be a case of outdated documentation. Try solve_by_elim { discharger := `[cc] }

view this post on Zulip Simon Hudon (Aug 17 2018 at 17:14):

I just updated it. https://github.com/leanprover/mathlib/pull/266

view this post on Zulip Scott Morrison (Sep 09 2018 at 00:24):

Hi @Simon Hudon, I proposed a further modification to solve_by_elim at https://github.com/leanprover/mathlib/pull/324. I'd be interested in your opinion sometime.

view this post on Zulip Scott Morrison (Sep 09 2018 at 00:24):

It's essentially just an extra option to make it convenient to add congr_fun and congr_arg to the assumptions.

view this post on Zulip Simon Hudon (Sep 09 2018 at 00:30):

Cool idea!

view this post on Zulip Scott Morrison (Sep 25 2018 at 04:31):

Thanks, @Simon Hudon and @Reid Barton for looking at my proposed changes to solve_by_elim. I've just pushed another change that make it quite a bit more usable --- it's now quite like the syntax for adding and removing lemmas from simp.

view this post on Zulip Scott Morrison (Sep 25 2018 at 04:32):

https://github.com/leanprover/mathlib/pull/324

view this post on Zulip Simon Hudon (Sep 25 2018 at 04:42):

What's the attribute name?

view this post on Zulip Scott Morrison (Sep 25 2018 at 06:53):

Oh -- there's no attribute that is automatically hooked into solve_by_elim, although we could do that!

view this post on Zulip Scott Morrison (Sep 25 2018 at 06:54):

You can write solve_by_elim [f, a], where f is a lemma, and a is an attribute, it will will look up all lemmas tagged with a, and then use the local context, f, and those a-lemmas.

view this post on Zulip Scott Morrison (Sep 25 2018 at 06:54):

You can also write solve_by_elim only [f, a] to not include the local context.

view this post on Zulip Simon Hudon (Sep 25 2018 at 06:56):

Actually, now I see what you did and it might be better to refrain from having a default solve_by_elim attribute, at least for now. We're battling the huge size of the simp list at the moment, maybe we can avoid or at least postpone the same situation for solve_by_elim and other attribute-based tactics.

view this post on Zulip Scott Morrison (Oct 06 2018 at 01:15):

Hi @Simon Hudon, I noticed what I think is a bug, or at least suboptimal behaviour in solve_by_elim, preventing successful backtracking when an apply generates multiple subgoals:

example {α : Type} (r : α → α → Prop) (f : α → α → α)
  (l : ∀ a b c : α, r a b → r a (f b c) → r a c)
  (a b c : α) (h₁ : r a b) (h₂ : r a (f b c)) : r a c :=
begin
  -- solve_by_elim ought to work here:
  have w : r a c,
  { apply l,
    apply h₁,
    apply h₂ },
  clear w,
  -- sadly, it doesn't, because of the way we recurse to subgoals.
  solve_by_elim,
  -- (Once solve_by_elim successfully uses h₂ on the first goal, it can't
  -- backtrack after realising that was a bad idea.)
end

view this post on Zulip Scott Morrison (Oct 06 2018 at 01:15):

There's an easy fix, but I thought I'd check if you agreed it warrants fixing before I PR it.

view this post on Zulip Simon Hudon (Oct 06 2018 at 01:33):

It looks like your proof of w is the only path that solve_by_elim can take. Can you show me the mistaken approach it tries?

view this post on Zulip Scott Morrison (Oct 06 2018 at 02:44):

It can trying applying h2 first. That succeeds, but then it has no where to go, and it fails to backtrack.

view this post on Zulip Scott Morrison (Oct 06 2018 at 02:44):

(Because with multiple sub goals solve_by_elim currently uses ; to recurse into them, it can’t backtrack across multiple sub goals.

view this post on Zulip Scott Morrison (Oct 06 2018 at 02:46):

That is, it tries:

apply l,
apply h2

And then is faced with the goal r a (f (f b c) ?m) and can’t proceed.

view this post on Zulip Simon Hudon (Oct 06 2018 at 02:50):

Ah! I see! How do you suggest to solve this?

view this post on Zulip Scott Morrison (Oct 06 2018 at 04:49):

It's pretty easy: see https://github.com/leanprover/mathlib/pull/393/commits/3fab845ccdfb081febf09821c4c1e43dbb82f75b


Last updated: May 09 2021 at 19:11 UTC