18.1. Truth🔗

Fundamentally, there are only two propositions in Lean: True and False. The axiom of propositional extensionality (propext) allows propositions to be considered equal when they are logically equivalent, and every true proposition is logically equivalent to True. Similarly, every false proposition is logically equivalent to False.

True is an inductively defined proposition with a single constructor that takes no parameters. It is always possible to prove True. False, on the other hand, is an inductively defined proposition with no constructors. Proving it requires finding an inconsistency in the current context.

Both True and False are subsingletons; this means that they can be used to compute inhabitants of non-propositional types. For True, this amounts to ignoring the proof, which is not informative. For False, this amounts to a demonstration that the current code is unreachable and does not need to be completed.

inductive proposition

True : Prop
True : Prop

True is a proposition and has only an introduction rule, True.intro : True. In other words, True is simply true, and has a canonical proof, True.intro For more information: Propositional Logic

Constructors

intro : True

True is true, and True.intro (or more commonly, trivial) is the proof.

inductive proposition

False : Prop
False : Prop

False is the empty proposition. Thus, it has no introduction rules. It represents a contradiction. False elimination rule, False.rec, expresses the fact that anything follows from a contradiction. This rule is sometimes called ex falso (short for ex falso sequitur quodlibet), or the principle of explosion. For more information: Propositional Logic

Constructors

def

False.elim.{u} {C : Sort u} (h : False) : C
False.elim.{u} {C : Sort u} (h : False) :
  C

False.elim : False → C says that from False, any desired proposition C holds. Also known as ex falso quodlibet (EFQ) or the principle of explosion.

The target type is actually C : Sort u which means it works for both propositions and types. When executed, this acts like an "unreachable" instruction: it is undefined behavior to run, but it will probably print "unreachable code". (You would need to construct a proof of false to run it anyway, which you can only do using sorry or unsound axioms.)

Dead Code and Subsingleton Elimination

The fourth branch in the definition of f is unreachable, so no concrete String value needs to be provided:

def f (n : Nat) : String :=
  if h1 : n < 11 then
    "Small"
  else if h2 : n > 13 then
    "Large"
  else if h3 : n % 2 = 1 then
    "Odd"
  else if h4 : n ≠ 12 then
    False.elim (byn:Nath1:¬n < 11h2:¬n > 13h3:¬n % 2 = 1h4:n ≠ 12⊢ False omegaAll goals completed! 🐙)
  else "Twelve"

In this example, False.elim indicates to Lean that the current local context is logically inconsistent: proving False suffices to abandon the branch.

Similarly, the definition of g appears to have the potential to be non-terminating. However, the recursive call occurs on an unreachable path through the program. The proof automation used for producing termination proofs can detect that the local assumptions are inconsistent.

def g (n : Nat) : String :=
  if n < 11 then
    "Small"
  else if n > 13 then
    "Large"
  else if n % 2 = 1 then
    "Odd"
  else if n ≠ 12 then
    g (n + 1)
  else "Twelve"
termination_by n