Proofs

Implication & logic

Use assumptions to construct proofs. An implication is a function from one proof to another.

theorem identity_proof (P : Prop) : P → P := by
  intro h
  exact h

theorem swap_and (P Q : Prop) : P ∧ Q → Q ∧ P := by
  intro h
  constructor
  · exact h.right
  · exact h.left

Explanation

`Prop`

The type of propositions. P and Q stand for arbitrary propositions.

`intro h`

To prove an implication, assume its premise and name the resulting hypothesis h.

`constructor`

Builds a conjunction by asking for a proof of each side.

`exact`

Supplies a term whose type matches the current goal.

Expected output

Reference only. Run the file to check its actual result.

File checked successfully.

Exercise

Prove P → Q → P using two intro steps.