Extracting un-named proofs from the goal state

Stream: general

[Eric Wieser]

Often I find myself needing a proof that is already part of the goal state, but having to rebuild it because I don't have a name on it. For example:

def foo : fin 2 → ℕ
| ⟨0, _⟩ := 1
| ⟨1, _⟩ := 2
| ⟨n + 2, h⟩ := false.elim $ n.not_lt_zero $ add_lt_iff_neg_right.mp h

example : ∀ x, foo x > 0 := begin
  rintro ⟨(x|x|x), hx⟩; dsimp only [foo],
  norm_num,
  norm_num,
  sorry  -- _.elim > 0; the _ is a proof of false - how do I reuse it?
end

[Reid Barton]

This is a weird way to do it, but works

example : ∀ x, foo x > 0 := begin
  rintro ⟨(x|x|x), hx⟩; dsimp only [foo],
  norm_num,
  norm_num,
  let m : false := _,
  change m.elim > 0,
  contradiction,
end

[Reid Barton]

It requires you to write out the form of the goal though--maybe it would be useful to have a tactic that could search the goal (or really the type of any expression) for a proof of a given p

[Reid Barton]

in this case false

[Eric Wieser]

Oh, clever

[Eric Wieser]

Yeah, such a tactic is something I've found myself wanting multiple times now

[Kyle Miller]

It looks like this actually works:

lemma elim_elim {α : Type*} {p : α → Prop} {h : false} : p (false.elim h) := false.elim h

example : ∀ x, foo x > 0 := begin
  rintro ⟨(x|x|x), hx⟩; dsimp only [foo],
  norm_num,
  norm_num,
  exact elim_elim,
end

[Eric Wieser]

Yeah, that's basically the same trick as Reid's. I think a tactic that extracts proofs from hypotheses and goals would be the most general solution here

[Kyle Miller]

I thought this was interesting because Lean figured out p automatically, but I guess it can't handle this example without being explicit:

example {h : false} : 37^2 + (false.elim h)^7 = 0 := begin
  apply @elim_elim _ (λ x, 37^2 + x^7 = 0),
end

[Eric Wieser]

Your approach is interesting because it suggests there is value to adding lemmas with false hypotheses!

[Mario Carneiro]

Eric Wieser said:

Yeah, that's basically the same trick as Reid's. I think a tactic that extracts proofs from hypotheses and goals would be the most general solution here

I have the vague memory of writing such a tactic back at the dawn of lean 3, no idea what happened to it

[Mario Carneiro]

this is also really useful for proving theorems about classical.some <nasty term you don't want to refer to>

[Mario Carneiro]

@Kyle Miller it will probably work if you mark elim_elim as elab_as_eliminator

[Kyle Miller]

That didn't seem to work here

[Kyle Miller]

With @[elab_as_eliminator]:

example {h : false} : false.elim h > 0 := elim_elim -- works
example {h : false} : false.elim h < 0 := elim_elim -- doesn't work
example {h : false} : false.elim h < 0 := @elim_elim _ (λ x, x < 0) _ -- works

[Mario Carneiro]

AH I remember

[Mario Carneiro]

generalize_proofs

[Eric Wieser]

tactic#generalize_proofs?

[Bryan Gin-ge Chen]

It's missing an invocation of add_tactic_doc: https://github.com/leanprover-community/mathlib/blob/da24addb74fe40009254cadce1e41593e876c82a/src/tactic/generalize_proofs.lean#L67

[Eric Wieser]

docs#tactic.interactive.generalize_proofs exists, hooray!

[Kyle Miller]

That's a nice tactic to have -- I've found myself generalizing proofs a few times by hand.

example : ∀ x, foo x > 0 := begin
  rintro ⟨(x|x|x), hx⟩; dsimp only [foo],
  norm_num,
  norm_num,
  generalize_proofs,
  tauto,
end

[Mario Carneiro]

It was written in 2017, cut it some slack

[Mario Carneiro]

it actually predates mathlib

[Bryan Gin-ge Chen]

Feel free to add / edit #5714 which adds this as an example to the doc string and adds a tactic doc entry.

[Mario Carneiro]

Oops, it appears I made a competing PR #5715

[Mario Carneiro]

I also fixed a bug and added support for at h1 h2 |- to my PR though

[Bryan Gin-ge Chen]

I think you could add an example to the tactic doc string like in mine but otherwise it looks much better, thanks!

[Mario Carneiro]

the examples I use in the tests are a bit simpler than eric's original example