Zulip Chat Archive

Stream: new members

Topic: ifinish


view this post on Zulip Michael Beeson (Sep 12 2020 at 06:56):

ifinish doesn't succeed with this simple proposition:

example:  (A B:Prop), (A  B)  ((A  B)  A)

This is not a question, or even a complaint really, I'm just trying to get familiar enough with ifinish so as to know
whether to expect it to succeed or not. I thought it would do this one.

view this post on Zulip Kenny Lau (Sep 12 2020 at 07:06):

it does for me

view this post on Zulip Michael Beeson (Sep 12 2020 at 07:31):

lemma lemma11helper1:  (A B:Prop), (A  B)  ((A  B)  A) :=
  assume A B,
  begin
    ifinish,
  end

produces

solve1 tactic failed, focused goal has not been solved
state:
A B : Prop,
a : A  B,
f : Prop,
a_1 : (A  B  A)  f
 f

So please post your corresponding input and successful output.

view this post on Zulip Markus Himmel (Sep 12 2020 at 07:32):

It works with current Lean and mathlib:

https://leanprover-community.github.io/lean-web-editor/#code=import%20tactic%0A%0Alemma%20lemma11helper1%3A%20%E2%88%80%20%28A%20B%3AProp%29%2C%20%28A%20%E2%86%92%20B%29%20%E2%86%92%20%28%28A%20%E2%88%A7%20B%29%20%E2%86%94%20A%29%20%3A%3D%0A%20%20assume%20A%20B%2C%0A%20%20begin%0A%20%20%20%20ifinish%2C%0A%20%20end%0A

view this post on Zulip Michael Beeson (Sep 12 2020 at 07:35):

Oh. So I should update lean using leanproject, I guess. I'm worried that some of my nice proofs might break then.


Last updated: May 13 2021 at 19:20 UTC