An implication P → Q means "if P is true, then Q is true." It's the most fundamental connective in logic. Every time you say "if ... then ..." in everyday life, you're using implication.
To prove an implication, you assume the hypothesis and show the conclusion follows. "Assume it's raining. Then the ground is wet." That's it. You don't need to prove it's actually raining — you just show what happens if it is.
To use an implication you already have, you apply it. If you know P → Q and you know P, then you can conclude Q. Logicians call this modus ponens.
Two key tactics make implication work in Lean 4:
intro h — When your goal is P → Q, this tactic says "assume P, call it h." The goal changes to Q, and you now have h : P in your context.
exact — When you have exactly the right term to close the goal, exact finishes the proof. If hpq : P → Q and hp : P, then exact hpq hp produces a proof of Q by function application.
-- The identity function: P implies P theorem identity (P : Prop) : P → P := by intro h exact h -- Using a hypothesis of type P → Q theorem modus_ponens (P Q : Prop) (hp : P) (hpq : P → Q) : Q := by exact hpq hp -- You can also use `apply` to work backwards theorem modus_ponens' (P Q : Prop) (hp : P) (hpq : P → Q) : Q := by apply hpq exact hp
Notice that in Lean 4, P → Q is really just a function type. A proof of P → Q is a function that takes a proof of P and returns a proof of Q. So hpq hp is just function application.
Replace sorry with a proof. Copy this into Lean 4 Web and make it compile.
theorem my_impl (P Q : Prop) (hp : P) (hpq : P → Q) : Q := by sorry
You have hpq : P → Q (a function from P to Q) and hp : P (a proof of P). What happens when you apply the function to the argument?
theorem my_impl (P Q : Prop) (hp : P) (hpq : P → Q) : Q := by exact hpq hp