have¶
The have
goal can be used to put new hypotheses into the local_context. Writing have H : (some proposition)
in Lean is like writing “I now claim that (some proposition) is true” in the middle of a maths proof.
Of course, you now have to prove H
before you can continue, so the number of goals goes up by one.
Example¶
Here is a proof that if P
is true, and if P → Q
and Q → R
, then R
is true. In maths the proof might go like this. “First, I claim that Q
is true, and the proof is that P
is true, and P
implies Q
. Now I claim that R
is true, and that’s because we know that Q
implies R
and we just proved that Q
was true. Here’s what this proof looks like in Lean:
example (P Q R : Prop) (HP : P) (HPQ : P → Q) (HQR : Q → R) : R :=
begin
-- one goal, R.
have HQ : Q, -- now two goals, Q and R.
apply HPQ,
exact HP, -- proof of Q finished, now back to R
apply HQR,
exact HQ -- we can use the proof of Q because we now have it
end
As well as the have HQ : Q,
syntax, there is also the have HQ : Q := ...
syntax, where the proof of Q
follows immediately after the :=
like this:
example (P Q R : Prop) (HP : P) (HPQ : P → Q) (HQR : Q → R) : R :=
begin
have HQ : Q := HPQ HP,
exact (HQR HQ),
end
Example (∀)¶
Here we build terms of type P a and Q a using the have
tactic.
example (X : Type) (P Q : X → Prop) (a : X) (HP : ∀ x : X, P x) (HQ : ∀ x : X, Q x): P a ∧ Q a :=
begin
have HPa : P a := HP a,
have HQa : Q a := HQ a,
split,
-- now two goals P a and Q a
{ exact HPa},
{ exact HQa},
end