Zulip Chat Archive

Stream: new members

Topic: false.elim tactic?


view this post on Zulip 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.

view this post on Zulip Jesse Michael Han (Sep 26 2019 at 19:40):

exfalso will change the goal to false

view this post on Zulip 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 ;)

view this post on Zulip Bryan Gin-ge Chen (Sep 26 2019 at 19:42):

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

view this post on Zulip Reid Barton (Sep 26 2019 at 19:42):

or cases h15 h

view this post on Zulip 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.

view this post on Zulip Alexandre Rademaker (Sep 26 2019 at 19:48):

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

view this post on Zulip Marc Huisinga (Sep 26 2019 at 19:51):

exfalso is just apply false.elim

view this post on Zulip 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?

view this post on Zulip Alexandre Rademaker (Sep 26 2019 at 19:59):

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

view this post on Zulip Patrick Massot (Sep 26 2019 at 20:09):

You can apply them, construct new terms using them.

view this post on Zulip Patrick Massot (Sep 26 2019 at 20:09):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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₃, 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.

view this post on Zulip Patrick Massot (Sep 26 2019 at 20:18):

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

view this post on Zulip Patrick Massot (Sep 26 2019 at 20:18):

oh wait

view this post on Zulip Patrick Massot (Sep 26 2019 at 20:18):

anat depends on a bunch of variable assumptions, right?

view this post on Zulip Alexandre Rademaker (Sep 26 2019 at 20:20):

Yes. They are declared as parameters.

view this post on Zulip Patrick Massot (Sep 26 2019 at 20:20):

You can write

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

view this post on Zulip Patrick Massot (Sep 26 2019 at 20:21):

after include h1 h13 h15 h18 of course

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 26 2019 at 20:25):

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

view this post on Zulip 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).

view this post on Zulip Alexandre Rademaker (Sep 26 2019 at 20:27):

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

view this post on Zulip 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.

view this post on Zulip Marc Huisinga (Sep 26 2019 at 20:29):

you need to remove begin/end as well

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Sep 26 2019 at 21:32):

[edit: saw the code link]

view this post on Zulip 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.

view this post on Zulip 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