2.7 True and Trivial Proofs

True is the proposition that always has a proof. It represents a goal with no mathematical content. In Lean, True has one constructor, called True.intro.

Problem

You want to prove a goal of the form:

True

or handle a hypothesis of type:

h : True

A proof of True is immediate. A hypothesis of type True carries no useful information.

Solution

Use trivial.

theorem true_example : True := by
  trivial

You can also use the constructor directly.

theorem true_intro_example : True := by
  exact True.intro

Both proofs close the goal because True.intro is a proof of True.

Discussion

True is an inductive proposition with one constructor. Its shape is morally:

inductive True : Prop where
  | intro : True

This means there is always exactly one canonical way to construct a proof of True.

By contrast, False has no constructors. This explains the practical difference:

True

is always provable, while:

False

can only be proved from inconsistent assumptions.

trivial

The tactic trivial tries to close simple goals such as True, reflexive equalities, and propositions already available in the context.

theorem trivial_true : True := by
  trivial

For a direct proof of True, trivial is idiomatic.

theorem implication_to_true (P : Prop) : P -> True := by
  intro hp
  trivial

The hypothesis hp : P is unused because proving True requires no information.

Term Form

The proof term is simply:

True.intro

So the theorem can be written without tactics.

theorem true_term : True :=
  True.intro

An implication into True is a function that ignores its input.

theorem implication_to_true_term (P : Prop) : P -> True :=
  fun _ => True.intro

The underscore means the argument is intentionally unused.

Using a Hypothesis of Type True

A hypothesis of type True contains no useful data.

theorem true_hypothesis_unused
    (P : Prop)
    (h : True)
    (hp : P) :
    P := by
  exact hp

The hypothesis h does not help prove P. It only says something already known.

You can still inspect it with cases.

theorem true_cases
    (P : Prop)
    (h : True)
    (hp : P) :
    P := by
  cases h
  exact hp

Since True has one constructor, cases h creates one branch and gives no new useful assumptions.

Conjunction with True

Conjunctions involving True often simplify.

theorem true_and_left
    (P : Prop) :
    True ∧ P -> P := by
  intro h
  exact h.right

The left component is trivial, and the right component contains the real proof.

theorem true_and_right
    (P : Prop) :
    P -> True ∧ P := by
  intro hp
  constructor
  · trivial
  · exact hp

The reverse form is similar.

theorem and_true_right
    (P : Prop) :
    P -> P ∧ True := by
  intro hp
  constructor
  · exact hp
  · trivial

Disjunction with True

A disjunction with True is always provable if you choose the True side.

theorem true_or
    (P : Prop) :
    True ∨ P := by
  left
  trivial

theorem or_true
    (P : Prop) :
    P ∨ True := by
  right
  trivial

If the goal contains a disjunction and one side is True, choose that side.

Functions Returning True

A predicate that always returns True is easy to satisfy.

def AlwaysTrue (α : Type) : α -> Prop :=
  fun _ => True

Every value satisfies this predicate.

theorem always_true_holds
    (α : Type)
    (a : α) :
    AlwaysTrue α a := by
  trivial

After unfolding AlwaysTrue, the goal reduces to True.

If Lean does not unfold it automatically, you can write:

theorem always_true_holds_unfold
    (α : Type)
    (a : α) :
    AlwaysTrue α a := by
  unfold AlwaysTrue
  trivial

True in Specifications

True is useful when a specification has no condition in a particular branch.

def IsAcceptable (n : Nat) : Prop :=
  if n = 0 then True else n > 0

For 0, the condition is trivial. For nonzero values, the condition contains the real predicate.

In early examples, True is also useful as a placeholder while the final property is still being designed.

structure CheckedValue where
  value : Nat
  proof : True

This structure records a proof field without imposing a meaningful invariant yet.

def checkedZero : CheckedValue :=
  { value := 0, proof := True.intro }

Later, the field can be replaced by a real invariant, such as value = 0 or value < 10.

simp and True

The simplifier knows many rules involving True.

theorem simplify_true_and
    (P : Prop) :
    True ∧ P -> P := by
  intro h
  simpa using h

The expression True ∧ P simplifies to P.

Similarly:

theorem simplify_and_true
    (P : Prop) :
    P ∧ True -> P := by
  intro h
  simpa using h

For beginner proofs, explicit projections are often easier to read. In larger proofs, simp removes trivial True components cleanly.

True Is Not a Useful Assumption

The following theorem cannot be proved from True alone:

-- This does not work:
-- theorem true_does_not_imply_anything (P : Prop) : True -> P := by
--   intro h
--   exact ?

After introducing h, the proof state is:

h : True
⊢ P

There is no way to construct an arbitrary proof of P from h : True.

This contrasts with False:

theorem false_implies_anything (P : Prop) : False -> P := by
  intro h
  cases h

True is always available but weak. False is impossible but strong once available.

Common Patterns

To prove:

⊢ True

use:

trivial

or:

exact True.intro

To prove a conjunction with one trivial side:

constructor
· trivial
· exact hp

To prove a disjunction with one trivial side:

left
trivial

or:

right
trivial

To remove True from simple propositions:

simp

Common Pitfalls

Do not expect h : True to prove an arbitrary proposition. It carries no useful mathematical content.

Do not confuse True with a boolean value. True : Prop is a proposition, while true : Bool is a boolean.

Do not overuse True in final specifications. It is useful as a placeholder, but meaningful specifications should eventually state real invariants.

Takeaway

True is the proposition with one trivial proof. To prove it, use trivial or True.intro. A hypothesis of type True usually provides no information. In proofs, True is most useful for simplifying specifications, filling harmless proof fields, and removing trivial branches.