intro¶
In general, the intro tactic changes a goal of type P → Q
into a hypothesis of type P
and a goal of type Q
. Here is a simple example.
example (P Q : Prop) (HQ : Q) : P → Q :=
begin
intro HP,
exact HQ
end
When this proof begins, the state is
P Q : Prop,
HQ : Q
⊢ P → Q
After intro HP
the state is
P Q : Prop,
HQ : Q,
HP : P
⊢ Q
and the goal is then solved with the exact tactic.
∀ is a function¶
Terms of type ∀ x, P x can be regarded as functions which eat a variable x and spit out a proof of P x; here is an example of what this looks like.
example (X : Type) (a : X) (P : X → Prop) (H : ∀ x, P x) : P a :=
begin
/-
X : Type,
a : X,
P : X → Prop,
H : ∀ (x : X), P x
⊢ P a
-/
exact (H a), -- H is a function; evaluate it at a
end
¬ is a function¶
In Lean, ¬ P
is notation for not P
, which is defined to mean P → false
. So one can work with ¬ P
as if it were a function.
example (P Q : Prop) : ¬ P → ¬ (P ∧ Q) :=
begin
intro HnP,
-- goal is now ⊢ ¬ (P ∧ Q)
intro HPQ,
-- state now
-- HnP : ¬ P
-- HPQ : P ∧ Q
-- goal is ⊢ false
apply HnP, -- think of HnP : P → false
-- goal now P
cases HPQ with HP HQ,
exact HP
end