Proving Equalities

Use equality propositions, reflexivity, and contradiction.

14.1 a = b is evidence that values are equal

import std::Base

theorem two_plus_two(): (2: Nat) + 2 = 4 {
  Refl
}

// Reflexivity suffices because both sides compute to four.

✓ theorem two_plus_two : 2 + 2 = 4

a = b states that two terms of type Nat are equal. Refl provides reflexivity: a term equals itself. Because 2 + 2 and 4 reduce to the same form by computation, the kernel accepts this proof.

Do not confuse == with a = b. The former is an equality comparison used at runtime; the latter is a proposition in the proof layer.

An incorrect proposition is rejected.

import std::Base

theorem wrong(): (2: Nat) + 2 = 5 {
  Refl
}

// This deliberately asks reflexivity to prove a false equality.

✗ wrong

error 4:3: type mismatch: expected `2 + 2 = 5`, found `2 + 2 = 2 + 2`
  differing part: expected `5`, found `4`

The actual type error returned by the current CLI appears below the code.

The diagnostic says that Refl proves (4: Nat) = 4, not 2 + 2 = 5. Reflexivity proves only that the results of computation coincide.

14.2 Chain equalities

The proposition to be proved determines the type and terms of Refl. Write simply Refl in a proof.

import std::Base

theorem sym_ex(a: Nat, b: Nat, e: a = b): b = a {
  Eq::sym(e)
}

theorem trans_ex(
  a: Nat,
  b: Nat,
  c: Nat,
  e1: a = b,
  e2: b = c
): a = c {
  Eq::trans(e1, e2)
}

theorem congr_ex(a: Nat, b: Nat, e: a = b): Succ(a) = Succ(b) {
  Eq::congr(Succ, e)
}

// Use symmetry, transitivity, and congruence explicitly.

✓ theorem sym_ex : ∀ a: Nat. ∀ b: Nat. (a = b) -> b = a
✓ theorem trans_ex : ∀ a: Nat. ∀ b: Nat. ∀ c: Nat. (a = b) -> (b = c) -> a = c
✓ theorem congr_ex : ∀ a: Nat. ∀ b: Nat. (a = b) -> Succ(a) = Succ(b)

14.3 Assume an impossible equality

import std::Base

theorem two_plus_two_ne_five(h: (2: Nat) + 2 = 5): False {
  match h: False {
  }
}

// An impossible equality has no constructor to match.

✓ theorem two_plus_two_ne_five : ¬(2 + 2 = 5)

This theorem states that evidence for 2 + 2 = 5 would lead to a contradiction. Since 2 + 2 reduces to 4, (4: Nat) = 5 cannot match any form of Refl. A match with no arms expresses that there are no possible constructors.

14.4 What adding an axiom means

Declaring an axiom adopts an unproved assumption. That is not inherently illegitimate. For example, you can add the law of excluded middle as an axiom:

import std::Base

axiom em(P: Prop): P ∨ ¬P

theorem not_not(P: Prop, n: ¬¬P): P {
  Or::elim(em(P), p => p, np => False::elim(n(np)))
}

// Record the dependency on excluded middle rather than hiding the axiom.

✓ axiom em : ∀ P: Prop. Or(P, ¬P)
✓ theorem not_not : ∀ P: Prop. (¬(¬P)) -> P

ok      em (axioms: em)
ok      not_not (axioms: em)

The output records that not_not depends on the axiom em. A theorem using axioms is a result conditional on those axioms. Distinguish being proved from holding without axioms.

Exercise 14.1: Complete theorem reflexive(x: Nat): x = x.