In Lean, contradiction tactic failed but actually goal accomplished

Question

I've been playing with Lean, trying to prove the next lemma:

lemma l1_cl (A B C : Prop) : ((A →  B) → C) → ((A ∧ ¬ B) ∨ C) :=

Here is the proof I've currently written:

begin
  intro h,
  cases classical.em C; cases classical.em A; cases classical.em B; try {right, assumption};
  {right, apply h, intro hA, contradiction},
  {sorry},{sorry},{sorry}
end

First {} seems okay; here is the Tactic state right before the contradiction:

1 goal
ABC: Prop
h: (A → B) → C
h_1: ¬C
h_2: ¬A
h_3: ¬B
hA: A
⊢ B

So, I have that h_2: ¬A and hA: A, which should lead to the contradiction. Applying contradiction in Coq thus leads to completing the goal.

But here in Lean something strange occurs: in Tactic state window I get the notification goals accomplished 🎉, whileas in Messages I get contradiction tactic failed with the next state:

state:
A B C : Prop,
h : (A → B) → C,
h_1 : ¬C,
h_2 : A,
h_3 : ¬B,
hA : A
⊢ B

So it seems like h_2 somehow has been changed, and this might lead to that message, although the goal is completed. Probably I've used contradiction tactic in the wrong way, but I don't see that for now. Can anyone help me to figure things out and to get rid of the message?

Thanks in advance!

Answer 1

The issue is the ; at the end of the long line. This is causing the {right, ...} block to be applied to all goals, meaning that the {sorry} blocks never have a chance to run, and the error you are getting at contradiction is in the second invocation on the block on the second goal. Change the ; to , to fix the issue:

lemma l1_cl (A B C : Prop) : ((A →  B) → C) → ((A ∧ ¬ B) ∨ C) :=
begin
  intro h,
  cases classical.em C;
    cases classical.em A;
    cases classical.em B;
    try {right, assumption}, -- <- note the comma
  {sorry},
  {sorry},
  {right, apply h, intro hA, contradiction},
  {right, apply h, intro hA, contradiction},
end

(Actually, as you can see the provided proof only works on goals 3 and 4; it is the first two that fail.)

Alternatively, you can keep the ; but use try to apply the block anywhere it works:

lemma l1_cl (A B C : Prop) : ((A →  B) → C) → ((A ∧ ¬ B) ∨ C) :=
begin
  intro h,
  cases classical.em C;
    cases classical.em A;
    cases classical.em B;
    try {right, assumption}; -- <- note the semicolon
    try {right, apply h, intro hA, contradiction},
  {sorry},{sorry},
end

---

Or if you are feeling lazy (and are using mathlib)

import tactic.tauto
lemma l1_cl (A B C : Prop) : ((A → B) → C) → ((A ∧ ¬ B) ∨ C) :=
by tauto!