# 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:

```lean
True
```

or handle a hypothesis of type:

```lean
h : True
```

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

## Solution

Use `trivial`.

```lean
theorem true_example : True := by
  trivial
```

You can also use the constructor directly.

```lean
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:

```lean
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:

```lean
True
```

is always provable, while:

```lean
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.

```lean
theorem trivial_true : True := by
  trivial
```

For a direct proof of `True`, `trivial` is idiomatic.

```lean
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:

```lean
True.intro
```

So the theorem can be written without tactics.

```lean
theorem true_term : True :=
  True.intro
```

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

```lean
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.

```lean
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`.

```lean
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.

```lean
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.

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

The reverse form is similar.

```lean
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.

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

```lean
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.

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

Every value satisfies this predicate.

```lean
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:

```lean
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.

```lean
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.

```lean
structure CheckedValue where
  value : Nat
  proof : True
```

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

```lean
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`.

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

The expression `True ∧ P` simplifies to `P`.

Similarly:

```lean
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:

```lean
-- 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:

```lean
h : True
⊢ P
```

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

This contrasts with `False`:

```lean
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:

```lean
⊢ True
```

use:

```lean
trivial
```

or:

```lean
exact True.intro
```

To prove a conjunction with one trivial side:

```lean
constructor
· trivial
· exact hp
```

To prove a disjunction with one trivial side:

```lean
left
trivial
```

or:

```lean
right
trivial
```

To remove `True` from simple propositions:

```lean
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.