Equalities

This chapter provides an introduction to the concept of equality in the Lean theorem prover. It explores how equality is defined and utilized in Lean’s type theory.

Throughout this chapter, we assume that X is an arbitrary type, x and y are terms of type X, as are a, b, c, and d. Additionally, P is a predicate on X, meaning P : X → Prop.

Predicate.lean

variable (X : Type)
variable (x y a b c d : X)
variable (P : X → Prop)

Equality

Given two terms of any given type we can consider the type of their equality (Eq), which is a term of type Prop.

Equality.lean

#check Eq
#check Eq x y
#check x = y

If we #print Eq, Lean returns

inductive Eq.{u_1} : {α : Sort u_1} → α → α → Prop
number of parameters: 2
constructors:
Eq.refl : ∀ {α : Sort u_1} (a : α), a = a

Eq is an inductive type that takes two implicit parameters: a universe level u_1 and {α : Sort u_1}, a type at this universe level. Given any two values of type α—the elements being compared for equality—it returns a proposition in Prop, asserting their equality.

The negation of an equality a = b is expressed in Lean using Ne or the symbol ≠ (written as \neq). This is simply the negation of the equality proposition, meaning ¬ (a = b).

NegEquality.lean

#check Ne
#check Ne x y
#check x ≠ y

Reflexivity

The Eq type has a single constructor, Eq.refl, which captures the principle of reflexivity: every element is equal to itself. This constructor takes an implicit type α : Sort u_1 and an element a : α, producing a proof of the proposition a = a. In other words, it establishes that any element is identical to itself. This is a more powerful theorem than it may appear at first, because although the statement of the theorem is a = a, Lean will allow anything that is definitionally equal to that type. So, for instance, 2 + 2 = 4 is proven in Lean by reflexivity.

As a shorthand, we can use rfl instead of Eq.refl. The key difference is that rfl infers a implicitly rather than requiring it explicitly. Here’s an example demonstrating how the constructor works:

Rfl.lean

theorem TEqRfl (a : X) : a = a := by
  exact rfl
  
theorem T1 : 2 + 2 = 4 := by
  exact rfl

Symmetry

If we have h : a = b as a hypothesis, we can derive b = a using the symmetric property of equality. This is achieved by applying Eq.symm to h. Alternatively, the shorthand h.symm can be used in place of Eq.symm h to provide a proof of b = a.

Symm.lean

theorem TEqSymm (h : a = b) : (b = a) := by
  exact Eq.symm h -- also (exact h.symm)

Transitivity

If we have h1 : a = b and h2 : b = c as hypotheses, we can derive a = c using the transitive property of equality. This is achieved by applying Eq.trans to h1 and h2. Alternatively, the shorthand h1.trans h2 can be used in place of Eq.trans h1 h2 to provide a proof of a = c.

Trans.lean

theorem TEqTrans (h1 : a = b) (h2 : b = c) : (a = c) := by
  exact Eq.trans h1 h2 -- also (exact h1.trans h2)

Rewrite

The rewrite [e] tactic applies the identity e as a rewrite rule to the target of the main goal.

• The rewrite [e₁, ..., eₙ] tactic applies the given rewrite rules sequentially.
  
• The rewrite [e] at l variant applies the rewrite at specific locations l, which can be either * (indicating all applicable places) or a list of hypotheses in the local context.

We can also use rw, which automatically attempts to close the goal by applying rfl after performing the rewrite.

Rw.lean

theorem TEqRw (h1 : a = b) : P b ↔ P a := by
  apply Iff.intro
  -- P b → P a
  intro h2 
  rewrite [h1] -- rewrites the goal using h1
  exact h2 
  -- P a → P b
  intro h2
  rw [h1] at h2 -- rewrites h2 using h1
  exact h2 

calc

The calc command allows for structured reasoning by chaining a sequence of equalities or inequalities. This approach makes multi-step proofs clearer and easier to follow. The general syntax is:

calc
  expr₁ = expr₂     : justification₁
  _     = expr₃     : justification₂
  _     = expr₄     : justification₃
  
  _     = exprₙ     : justificationₙ

Here:

• expr₁, expr₂, expr₃, ... are expressions.
  
• justification₁, justification₂, ... are proofs or explanations that establish each equality or inequality.
  
• The _ syntax connects the steps, ensuring a logical flow.

Here’s an example demonstrating the use of the calc command.

Calc.lean

theorem TCalc (h1 : a = b) (h2 : b = c) (h3: c = d) : (a = d) := by
  calc
    a = b := by rw [h1]
    _ = c := by rw [h2]
    _ = d := by rw [h3]

Types with meaningful equality

Equality (=) is a fundamental concept in Lean, defined for all types. However, its interpretation and behavior depend on the structure of the specific type. While equality is always available, its computational properties—such as whether it is decidable—vary depending on the type.

DecidableEq.lean

#eval x = y -- Returns error
#eval 2 + 2 = 4 -- Returns true

Decidable Equality

A type has decidable equality if there exists an algorithm to determine whether any two elements of that type are equal. In Lean, this is captured by the DecidableEq type class.

If we #print DecidableEq Lean returns

@[reducible] def DecidableEq.{u} : Sort u → Sort (max 1 u) :=
fun α => (a b : α) → Decidable (a = b)

An example of a type with decidable equality is Bool. The following proof defines an instance of DecidableEq for booleans:

DecidableEqBool.lean

def DecidableEqBool : DecidableEq Bool := by
  intro a b
  match a, b with
    | false, false => exact isTrue rfl
    | false, true  => exact isFalse (fun h => Bool.noConfusion h)
    | true , false => exact isFalse (fun h => Bool.noConfusion h)
    | true , true  => exact isTrue rfl

In Lean, the noConfusion principle is a powerful tool for reasoning about inductive types. It captures two essential properties of constructors: they are disjoint (no two distinct constructors can produce equal values) and injective (equal constructor applications imply equal arguments). For the type Bool, which has exactly two constructors—true and false—these properties mean that true ≠ false and false ≠ true. The expression Bool.noConfusion h exploits this fact: when we assume a contradictory equality like true = false, noConfusion produces a logical contradiction, allowing us to conclude that such an assumption is invalid. More generally, noConfusion can be used to eliminate impossible equalities between constructors or to extract equalities of their arguments when constructors match.

Some other examples of types with decidable equality include:

• Basic types such as Nat, Int, and String, which all have decidable equality.
  
• Inductive types and structures, provided that their components also have decidable equality.

DecidableEq.lean

#check Nat.decEq
#check Int.decEq
#check String.decEq

Consider the following functions.

Char.lean

-- Function Charp
def Charp : Nat → Nat → Bool := by
  intro n m
  by_cases n = m
  -- Case n = m
  exact true
  -- Case n ≠ m
  exact false

-- Function Charp2
def Charp2 : Nat → Nat → Bool := fun n m => if n = m then true else false

-- Function Charpoint
noncomputable def Charpoint {A : Type} : A → A → Bool := by
  intro a b
  by_cases a = b
  -- Case a = b
  exact true
  -- Case a ≠ b
  exact false

-- Function Charpoint2
def Charpoint2 {A : Type} [DecidableEq A] : A → A → Bool :=
fun n m => if n = m then true else false

The function Charp takes two natural numbers, n and m, and determines whether they are equal. It returns true if n = m and false otherwise. This is achieved using the by_cases tactic, which performs a case distinction: if n = m, the function returns true, and if n ≠ m, it returns false. An alternative implementation, Charp2, expresses the same function using an if ... then ... else expression.

In general, equality in an arbitrary type is not necessarily computable. For instance, in the function Charpoint, which generalizes Charp to an arbitrary type A, the use of by_cases a = b introduces a logical case distinction that may not be computable. Consequently, the function is marked as noncomputable, indicating that it relies on classical reasoning rather than constructive computation. To ensure computability, the alternative function Charpoint2 explicitly assumes that A has decidable equality by requiring the type class instance [DecidableEq A]. This assumption allows Lean to treat equality on A as a computable procedure, ensuring that the function remains fully computable.

Equality in Prop

In Prop, the type of propositions, equality is defined in terms of logical equivalence, as stated by the axiom of propositional extensionality, written propext. An axiom is a fundamental assumption accepted without proof.

If we #print propext, Lean returns:

axiom propext : ∀ {a b : Prop}, (a ↔ b) → a = b

This means that if two propositions a and b are logically equivalent (a ↔︎ b), then they are considered equal. Note that propext is an axiom. Axioms are accepted by definition, rather than being derived from existing theorems. This axiom enables the substitution of equivalent propositions within any context. However, unlike equality for concrete types such as Nat or Int, logical equivalence is generally undecidable—determining whether two arbitrary propositions are equivalent is, in general, an undecidable problem.

propext.lean

theorem TEqProp {Q : Prop} : (Q ∧ True) = Q := by
  apply propext
  apply Iff.intro
  -- Q ∧ True → Q
  intro h2
  exact h2.left
  -- Q → Q ∧ True
  intro h2
  apply And.intro
  exact h2
  trivial

We can always inspect the axioms upon which a theorem relies by using the #print axioms command. For instance, to check the axioms involved in the TEqProp theorem, we can run:

#print axioms TEqProp

The above code returns 'TEqProp' depends on axioms: [propext].