Zulip Chat Archive

Stream: new members

Topic: exists_elim


view this post on Zulip Michael Beeson (Jun 20 2020 at 16:54):

Below I will paste in a correct proof. My question is, please show me a couple of better ways to prove this simple theorem.
Q1: how can I do this without entering tactic mode? Q2: how can I do it entirely in tactic mode, i.e., what do I use in tactic mode that corresponds to exists.elim?

variables (p q r : nat Prop)

lemma test3 :
 ( x:nat ,( p x  q x  r x) ) (x:nat, (r x) ):=
 assume h,
 exists.elim h
  begin
    intros a h2,
    existsi a,
    exact h2.right.right,
  end

view this post on Zulip Bryan Gin-ge Chen (Jun 20 2020 at 16:59):

variables (p q r : nat Prop)
-- Q1
lemma test3_term :
 ( x:nat ,( p x  q x  r x) ) (x:nat, (r x) ):=
 assume h,
 exists.elim h (assume a h2, exists.intro a h2.2.2)
-- Q2
lemma test3_tactic :
 ( x:nat ,( p x  q x  r x) ) (x:nat, (r x) ):=
begin
  intro h,
  cases h with a h2,
  existsi a,
  exact h2.2.2
end

view this post on Zulip Michael Beeson (Jun 20 2020 at 17:01):

Thank you. If there is a way to mark an answer as "the answer" like on stack exchange, I don't know it.

view this post on Zulip Bryan Gin-ge Chen (Jun 20 2020 at 17:03):

The proof using mathlib tactics is much nicer:

import tactic
lemma test3_tactic2 :
 ( x:nat ,( p x  q x  r x) ) (x:nat, (r x) ):=
begin
  rintro a, h1, h2, h3,
  use [a, h3]
end

view this post on Zulip Bryan Gin-ge Chen (Jun 20 2020 at 17:05):

Or even shorter:

import tactic
lemma test3_tactic3 :
 ( x:nat ,( p x  q x  r x) ) (x:nat, (r x) ):=
by tauto

view this post on Zulip Jalex Stark (Jun 20 2020 at 17:37):

Michael Beeson said:

Thank you. If there is a way to mark an answer as "the answer" like on stack exchange, I don't know it.

you can react with emoji

view this post on Zulip Michael Beeson (Jun 20 2020 at 19:19):

'tauto' appears to be misnamed if it deals with quantifiers.
I am trying to work with intuitionistic logic only. Are there analogues for these tactics that are intuitionistic?
I notice that 'ifinish' can't handle this example. In general, once I have a proof, how can I ask Lean to check if
it is really an intuitionistic proof? I'm worried that some tactics may, in the words of Avigad in a comment in finish.lean,
"leak classical logic".

view this post on Zulip Johan Commelin (Jun 20 2020 at 19:19):

#print axioms your_lemma_name

view this post on Zulip Johan Commelin (Jun 20 2020 at 19:20):

If you see classical.choice, something went wrong


Last updated: May 06 2021 at 21:09 UTC