Stream: new members

Topic: false.elim tactic?

Alexandre Rademaker (Sep 26 2019 at 19:38):

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 (Sep 26 2019 at 19:40):

exfalso will change the goal to false

Marc Huisinga (Sep 26 2019 at 19:41):

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

Bryan Gin-ge Chen (Sep 26 2019 at 19:42):

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

Reid Barton (Sep 26 2019 at 19:42):

or cases h15 h

Alexandre Rademaker (Sep 26 2019 at 19:46):

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 (Sep 26 2019 at 19:48):

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

Marc Huisinga (Sep 26 2019 at 19:51):

exfalso is just apply false.elim

Alexandre Rademaker (Sep 26 2019 at 19:58):

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 (Sep 26 2019 at 19:59):

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

Patrick Massot (Sep 26 2019 at 20:09):

You can apply them, construct new terms using them.

Patrick Massot (Sep 26 2019 at 20:09):

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

Patrick Massot (Sep 26 2019 at 20:09):

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

Patrick Massot (Sep 26 2019 at 20:10):

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 (Sep 26 2019 at 20:12):

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₄, 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 (Sep 26 2019 at 20:18):

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

oh wait

Patrick Massot (Sep 26 2019 at 20:18):

anat depends on a bunch of variable assumptions, right?

Alexandre Rademaker (Sep 26 2019 at 20:20):

Yes. They are declared as parameters.

Patrick Massot (Sep 26 2019 at 20:20):

You can write

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


Patrick Massot (Sep 26 2019 at 20:21):

after include h1 h13 h15 h18 of course

Patrick Massot (Sep 26 2019 at 20:22):

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

Patrick Massot (Sep 26 2019 at 20:23):

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

lemma claudiat : CB :=
by finish


Alexandre Rademaker (Sep 26 2019 at 20:24):

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 (Sep 26 2019 at 20:25):

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

Patrick Massot (Sep 26 2019 at 20:25):

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

Patrick Massot (Sep 26 2019 at 20:27):

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 (Sep 26 2019 at 20:27):

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

Alexandre Rademaker (Sep 26 2019 at 20:28):

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

Marc Huisinga (Sep 26 2019 at 20:29):

you need to remove begin/end as well

Alexandre Rademaker (Sep 26 2019 at 20:36):

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 (Sep 26 2019 at 21:42):

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 (Sep 26 2019 at 22:44):

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


Last updated: May 06 2021 at 21:09 UTC