introduce implication

Stream: general

[Chris Laux]

Beginner question: is there an intro command for simple implication, like iff.intro for equivalence? I somehow can't find it in the manual

[Simon Hudon]

A lambda expression does that. λ x : t, (s : u) has type t -> u

[Chris Laux]

Ok, I see. I'm trying to solve the simple exercise example : (∃ x : α, r) → r := sorry, but I just can't find the right notation. Would anyone mind telling me the answer?

[Johan Commelin]

Do you want to use term mode or tactic mode? With or without mathlib?

[Floris van Doorn]

Assuming r is a proposition (of type Prop) then the following is a short way to prove it:

example {α : Type} {r : Prop} : (∃ x : α, r) → r :=
λ⟨x, h⟩, h

The λ⟨x, h⟩ introduces a variable x : α and h : r (so that together, ⟨x, h⟩ : ∃ x : α, r), and then the proof of r is h.

[Floris van Doorn]

This doesn't work if r is not a proposition.

[Floris van Doorn]

Slightly longer, but without the ⟨x, h⟩ brackets:

example {α : Type} {r : Prop} : (∃ x : α, r) → r :=
λ prf, exists.elim prf (λ x h, h)

Here we call exists.elim prf to eliminate the existential quantifier.

[Chris Laux]

@Floris van Doorn : thanks. @Johan Commelin : I'm just getting started, so I'm not sure about those distinctions

[Kevin Buzzard]

If your background is in CS then you might want to start with term mode like Floris was doing. If you background is in maths then you might want to learn tactic mode first

[Floris van Doorn]

Yes, I also wanted to give you an example of the proof in tactic mode, but I had to run:

example {α : Type} {r : Prop} : (∃ x : α, r) → r :=
begin
  intro prf,
  cases prf with x h,
  exact h
end

Probably the best way to learn more is to look at relevant parts of theorem proving in Lean

[Chris Laux]

That is an exercise from "Theorem proving in Lean", in that chapter they are showing answers in term mode.

[Chris Laux]

Btw, is there a reference handbook/file of sorts that lists all possible "commands" for Lean?

[Anne Baanen]

The command #help commands lists them, with a short description.

[Anne Baanen]

But those are just the top-level commands, like def and import and so on

[Rob Lewis]

There's also the reference manual, which may not be 100% up to date, but tries to document things like this. https://leanprover.github.io/reference/

[Chris Laux]

Thanks, guys