Zulip Chat Archive

Stream: general

Topic: how to use `solve_by_elim`


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.

Simon Hudon (Aug 17 2018 at 16:50):

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

Simon Hudon (Aug 17 2018 at 17:14):

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

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.

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.

Simon Hudon (Sep 09 2018 at 00:30):

Cool idea!

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.

Scott Morrison (Sep 25 2018 at 04:32):

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

Simon Hudon (Sep 25 2018 at 04:42):

What's the attribute name?

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!

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.

Scott Morrison (Sep 25 2018 at 06:54):

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

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.

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

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.

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?

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.

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.

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.

Simon Hudon (Oct 06 2018 at 02:50):

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

Scott Morrison (Oct 06 2018 at 04:49):

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


Last updated: Dec 20 2023 at 11:08 UTC