Proofs

Reading mathematical notation

Read quantified statements and construct their proofs.

-- For every natural number n, there is a natural number m
-- such that m is n + 1 and is greater than n.
example : ∀ n : Nat, ∃ m : Nat, m = n + 1 ∧ n < m := by
  intro n
  exact ⟨n + 1, rfl, by omega⟩

-- “P and Q” holds if and only if “Q and P” holds.
example (P Q : Prop) : (P ∧ Q) ↔ (Q ∧ P) := by
  constructor
  · intro ⟨hp, hq⟩
    exact ⟨hq, hp⟩
  · intro ⟨hq, hp⟩
    exact ⟨hp, hq⟩

Explanation

`∀ · ∃`

∀ means “for every”; ∃ means “there exists.” Read the bound variables from left to right. Here the witness m may depend on n.

`∧ · ↔`

∧ joins two claims that must both hold. ↔ asks for implications in both directions.

`⟨ … ⟩`

Constructs a witness together with the required proofs, or combines proofs of a conjunction.

`Unicode input`

Type \forall, \exists, \and, or \iff and accept the editor suggestion with Enter or Tab. Symbols are Lean source characters, not rendered LaTeX.

Expected output

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

File checked successfully.

Exercise

Use n + 2 as the witness in the first theorem and update the statement accordingly.