Zulip Chat Archive

Stream: general

Topic: Extracting un-named proofs from the goal state


view this post on Zulip 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

view this post on Zulip 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,
  contradiction,
end

view this post on Zulip 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

view this post on Zulip Reid Barton (Jan 12 2021 at 14:31):

in this case false

view this post on Zulip Eric Wieser (Jan 12 2021 at 14:32):

Oh, clever

view this post on Zulip Eric Wieser (Jan 12 2021 at 14:33):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 12 2021 at 17:57):

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

view this post on Zulip 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

view this post on Zulip 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>

view this post on Zulip Mario Carneiro (Jan 12 2021 at 18:07):

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

view this post on Zulip Kyle Miller (Jan 12 2021 at 18:07):

That didn't seem to work here

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 12 2021 at 18:12):

AH I remember

view this post on Zulip Mario Carneiro (Jan 12 2021 at 18:12):

generalize_proofs

view this post on Zulip Eric Wieser (Jan 12 2021 at 18:15):

tactic#generalize_proofs?

view this post on Zulip 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

view this post on Zulip Eric Wieser (Jan 12 2021 at 18:16):

docs#tactic.interactive.generalize_proofs exists, hooray!

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jan 12 2021 at 18:17):

It was written in 2017, cut it some slack

view this post on Zulip Mario Carneiro (Jan 12 2021 at 18:17):

it actually predates mathlib

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jan 12 2021 at 18:59):

Oops, it appears I made a competing PR #5715

view this post on Zulip Mario Carneiro (Jan 12 2021 at 19:00):

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

view this post on Zulip 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!

view this post on Zulip 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