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!

Improve this question
$\endgroup$

1 Answer 1

Reset to default
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!
Improve this answer
$\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$
    – Pavel Snopov
    Commented 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$
    – Mario Carneiro
    Commented May 5, 2022 at 1:57

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