how to use `solve_by_elim`

Stream: general

[Chris Hughes]

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]

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

[Simon Hudon]

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

[Scott Morrison]

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]

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

[Simon Hudon]

Cool idea!

[Scott Morrison]

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]

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

[Simon Hudon]

What's the attribute name?

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Simon Hudon]

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]

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]

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

[Simon Hudon]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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