# In Lean, contradiction tactic failed but actually goal accomplished

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?

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!

• Thank you! The 2nd scenario works fine! But via the 1st one, the message persists: it seems that the provided proof works on goals 1 and 2, at least this is what I get in the Tactic state. Nevertheless, applying the proof to first 2 cases, the problem is gone. May 4, 2022 at 20:29
• Because the three cases appear in the order C, A, B and classical.em has the type p ∨ ¬p which puts the positive case first, the first four goals have h_1 : C and are killed by the try block, and the latter four have h_1: ¬C, and h_2, h_3 have types [A,B; A,¬B; ¬A,B; ¬A,¬B] in that order. Since the proof is assuming A and trying to get a contradiction, the latter two goals (3 and 4) are provable by this method, while goals 1 and 2 need a different approach. (In other words, the code should be correct as written unless em or the cases were done in another order.) May 5, 2022 at 1:57