ifinish

Stream: new members

[Michael Beeson]

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.

[Kenny Lau]

it does for me

[Michael Beeson]

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.

[Markus Himmel]

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

[Michael Beeson]

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