7
$\begingroup$

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!

$\endgroup$

1 Answer 1

11
$\begingroup$

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!
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ May 4, 2022 at 20:29
  • 1
    $\begingroup$ 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.) $\endgroup$ May 5, 2022 at 1:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.