false.elim tactic?

Stream: new members

[Alexandre Rademaker]

What is the false.elim equivalent in tactic mode? I have the following proof state:

lemma anat : AP :=
begin
 apply or.elim h1,
 intro,
 have h, from h13 a,

end

with h15 h I have false. From that I should be able to proof anything.

AA AB AP : Prop,
h1 : AA ∨ AB ∨ AP,
h13 : AA → AB,
h15 : ¬AB,
a : AA,
h : AB
⊢ AP

The complete proof without tactics is:

lemma ana : AP :=
or.elim h1
 (λ h₂ : AA, show AP, from false.elim (absurd h₂ (λ h₁ : AA, show false,
  from (absurd (h13 h₁) h15))))
 (λ h₂ : AB ∨ AP, show AP,
  from or.elim h₂
   (λ h₃ : AB, show AP, from false.elim (absurd h₃ h15))
   (λ h₃ : AP, h₃))

TPiL says nothing about in the chapter 5.

[Jesse Michael Han]

exfalso will change the goal to false

[Marc Huisinga]

the "contradiction" tactic is probably what you're looking for, and it's mentioned briefly in 5.3 ;)

[Bryan Gin-ge Chen]

you could also probably write something like exact (h15 h).elim

[Reid Barton]

or cases h15 h

[Alexandre Rademaker]

What a shame! I missed the. contradiction! ;-) The exact (h15 h).elim didnt' work but cases h15 h works! OK, I have to study cases, very useful.

[Alexandre Rademaker]

It was not clear how to deal with the result of exfalso!

[Marc Huisinga]

exfalso is just apply false.elim

[Alexandre Rademaker]

Maybe I am also missing something, but in TPiL I didn't find how to use previous lemmas during a proof of a new lemma. The include works only for variables?

[Alexandre Rademaker]

I promisse, last question for this week! ;-)

[Patrick Massot]

You can apply them, construct new terms using them.

[Patrick Massot]

Do you have a specific example where I could show you how to do that?

[Patrick Massot]

You could also open a random Lean file found on the internet and see how lemmas are used.

[Patrick Massot]

But it's indeed striking that explanation in TPIL are so local (as opposed to theory building) that this is maybe not explained at all.

[Alexandre Rademaker]

It is a simple puzzle formalized in propositional logic that I am trying to rewrite the proofs with tactics. From the previous lemma ana we can prove the second claudia:

lemma ana : AP :=
or.elim h1
 (λ h₂ : AA, show AP, from false.elim (absurd h₂ (λ h₁ : AA, show false,
  from (absurd (h13 h₁) h15))))
 (λ h₂ : AB ∨ AP, show AP,
  from or.elim h₂
   (λ h₃ : AB, show AP, from false.elim (absurd h₃ h15))
   (λ h₃ : AP, h₃))

lemma claudia : CB :=  (h18 (ana h1 h13 h15))

Above I was able to prove ana with tactics:

include h1 h13 h15

lemma anat : AP :=
begin
 apply or.elim h1,
 intro,
 have h₁, from h13 a,
 cases (h15 h₁),
 intro, apply or.elim a,
 intro h₃, contradiction,
 intro h₄, exact h₄
end

lemma claudiat (a : AP) : CB :=
begin
 exact h18 a,
end

But I don't want to insert the hypothesis a : AP in the claudiat lemma, it could be dependent of the previous lemma. Complete code here.

[Patrick Massot]

You can write exact h18 anat, although there is no point writing that in tactic mode.

[Patrick Massot]

oh wait

[Patrick Massot]

anat depends on a bunch of variable assumptions, right?

[Alexandre Rademaker]

Yes. They are declared as parameters.

[Patrick Massot]

You can write

lemma claudiat : CB :=
begin
  apply h18,
  apply ana ; assumption,
end

[Patrick Massot]

after include h1 h13 h15 h18 of course

[Patrick Massot]

Those includes are not necessary in term mode, because Lean can inspect the proof term and figure out it uses those variables.

[Patrick Massot]

Of course you can also import mathlib's tactic, skip the anat lemma entirely and write:

lemma claudiat : CB :=
by finish

[Alexandre Rademaker]

Oh, thank you. I will study mathlib the the solution above. It seems more succinct than the one I obtained:

lemma claudiat1 : CB :=
begin
 exact h18 (anat h1 h13 h15),
end

[Patrick Massot]

The by finish solution is cheating, it's calling automation to do all the work for you.

[Patrick Massot]

This is clearly a problem you would expect a computer to solve.

[Patrick Massot]

And really there is no point at all in writing

begin
  exact stuff
end

it's exactly the same as writing stuff (hence the name of the exact tactic).

[Alexandre Rademaker]

Yes, but I really prefer to understand better the tactics before relying on the automation...

[Alexandre Rademaker]

but if I remove exact in begin exact h18 (anat h1 h13 h15), end above, I got an error.

[Marc Huisinga]

you need to remove begin/end as well

[Alexandre Rademaker]

Oh, I got your point now. Yes, in that particular case tactic mode does make sense at all. I agree, just forcing myself to learn tactics and comparing with the other approach for construct proofs.

[Kevin Buzzard]

[edit: saw the code link]

[Kevin Buzzard]

lemma ana : AP := or.elim h1 (λ h₂, false.elim $ h15 $ h13 h₂) (λ h₂, or.elim h₂ (λ h₃, false.elim $ h15 h₃) id) would be a term mode way to write it. This would be more the mathlib style I guess.

[Mario Carneiro]

if we're golfing term mode:

theorem ana {AA AB AP : Prop}
  (h1 : AA ∨ AB ∨ AP) (h13 : AA → AB) (h15 : ¬AB) : AP :=
(h1.resolve_left (mt h13 h15)).resolve_left h15