Zulip Chat Archive

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

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

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.

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

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

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

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".

Johan Commelin (Jun 20 2020 at 19:19):

#print axioms your_lemma_name

Johan Commelin (Jun 20 2020 at 19:20):

If you see classical.choice, something went wrong

Last updated: Dec 20 2023 at 11:08 UTC

leanprover-community / mathlib