## Stream: general

### Topic: Extracting un-named proofs from the goal state

#### Eric Wieser (Jan 12 2021 at 14:23):

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 (Jan 12 2021 at 14:29):

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,
end


#### Reid Barton (Jan 12 2021 at 14:31):

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 (Jan 12 2021 at 14:31):

in this case false

Oh, clever

#### Eric Wieser (Jan 12 2021 at 14:33):

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

#### Kyle Miller (Jan 12 2021 at 17:43):

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 (Jan 12 2021 at 17:45):

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 (Jan 12 2021 at 17:54):

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 (Jan 12 2021 at 17:57):

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

#### Mario Carneiro (Jan 12 2021 at 18:02):

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 (Jan 12 2021 at 18:03):

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

#### Mario Carneiro (Jan 12 2021 at 18:07):

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

#### Kyle Miller (Jan 12 2021 at 18:07):

That didn't seem to work here

#### Kyle Miller (Jan 12 2021 at 18:10):

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


AH I remember

#### Mario Carneiro (Jan 12 2021 at 18:12):

generalize_proofs

#### Bryan Gin-ge Chen (Jan 12 2021 at 18:16):

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 (Jan 12 2021 at 18:16):

docs#tactic.interactive.generalize_proofs exists, hooray!

#### Kyle Miller (Jan 12 2021 at 18:17):

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 (Jan 12 2021 at 18:17):

It was written in 2017, cut it some slack

#### Mario Carneiro (Jan 12 2021 at 18:17):

it actually predates mathlib

#### Bryan Gin-ge Chen (Jan 12 2021 at 18:28):

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

#### Mario Carneiro (Jan 12 2021 at 18:59):

Oops, it appears I made a competing PR #5715

#### Mario Carneiro (Jan 12 2021 at 19:00):

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

#### Bryan Gin-ge Chen (Jan 12 2021 at 19:02):

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

#### Mario Carneiro (Jan 12 2021 at 19:06):

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

Last updated: May 12 2021 at 23:13 UTC