17.2. Logical Connectives

Conjunction is implemented as the inductively defined proposition And. The constructor And.intro represents the introduction rule for conjunction: to prove a conjunction, it suffices to prove both conjuncts. Similarly, And.elim represents the elimination rule: given a proof of a conjunction and a proof of some other statement that assumes both conjuncts, the other statement can be proven. Because And is a subsingleton, And.elim can also be used as part of computing data. However, it should not be confused with PProd: using non-computable reasoning principles such as the Axiom of Choice to define data (including Prod) causes Lean to be unable to compile and run the resulting program, while using them in a proof of a proposition causes no such issue.

In a tactic proof, conjunctions can be proved using And.intro explicitly via apply, but constructor is more common. When multiple conjunctions are nested in a proof goal, and_intros can be used to apply And.intro in each relevant location. Assumptions of conjunctions in the context can be simplified using cases, pattern matching with let or match, or rcases.

structure

And (a b : Prop) : Prop

And a b, or a ∧ b, is the conjunction of propositions. It can be constructed and destructed like a pair: if ha : a and hb : b then ⟨ha, hb⟩ : a ∧ b, and if h : a ∧ b then h.left : a and h.right : b.

Conventions for notations in identifiers:

The recommended spelling of ∧ in identifiers is and.
The recommended spelling of /\ in identifiers is and (prefer ∧ over /\).

Constructor

And.intro

And.intro : a → b → a ∧ b is the constructor for the And operation.

Fields

left : a

Extract the left conjunct from a conjunction. h : a ∧ b then h.left, also notated as h.1, is a proof of a.

right : b

Extract the right conjunct from a conjunction. h : a ∧ b then h.right, also notated as h.2, is a proof of b.

def

And.elim.{u_1} {a b : Prop} {α : Sort u_1}
  (f : a → b → α) (h : a ∧ b) : α

Non-dependent eliminator for And.

Disjunction implemented as the inductively defined proposition Or. It has two constructors, one for each introduction rule: a proof of either disjunct is sufficient to prove the disjunction. While the definition of Or is similar to that of Sum, it is quite different in practice. Because Sum is a type, it is possible to check which constructor was used to create any given value. Or, on the other hand, forms propositions: terms that prove a disjunction cannot be interrogated to check which disjunct was true. In other words, because Or is not a subsingleton, its proofs cannot be used as part of a computation.

In a tactic proof, disjunctions can be proved using either constructor (Or.inl or Or.inr) explicitly via apply. Assumptions of disjunctions in the context can be simplified using cases, pattern matching with match, or rcases.

inductive predicate

Or (a b : Prop) : Prop

Or a b, or a ∨ b, is the disjunction of propositions. There are two constructors for Or, called Or.inl : a → a ∨ b and Or.inr : b → a ∨ b, and you can use match or cases to destruct an Or assumption into the two cases.

Conventions for notations in identifiers:

The recommended spelling of ∨ in identifiers is or.
The recommended spelling of \/ in identifiers is or (prefer ∨ over \/).

Constructors

inl {a b : Prop} (h : a) : a ∨ b

Or.inl is "left injection" into an Or. If h : a then Or.inl h : a ∨ b.

inr {a b : Prop} (h : b) : a ∨ b

Or.inr is "right injection" into an Or. If h : b then Or.inr h : a ∨ b.

When either disjunct is decidable, it becomes possible to use Or to compute data. This is because the decision procedure's result provides a suitable branch condition.

def

Or.by_cases.{u} {p q : Prop} [Decidable p]
  {α : Sort u} (h : p ∨ q) (h₁ : p → α)
  (h₂ : q → α) : α

Construct a non-Prop by cases on an Or, when the left conjunct is decidable.

def

Or.by_cases'.{u} {q p : Prop} [Decidable q]
  {α : Sort u} (h : p ∨ q) (h₁ : p → α)
  (h₂ : q → α) : α

Construct a non-Prop by cases on an Or, when the right conjunct is decidable.

Rather than encoding negation as an inductive type, ¬P is defined to mean P → False. In other words, to prove a negation, it suffices to assume the negated statement and derive a contradiction. This also means that False can be derived immediately from a proof of a proposition and its negation, and then used to prove any proposition or inhabit any type.

def

Not (a : Prop) : Prop

Not p, or ¬p, is the negation of p. It is defined to be p → False, so if your goal is ¬p you can use intro h to turn the goal into h : p ⊢ False, and if you have hn : ¬p and h : p then hn h : False and (hn h).elim will prove anything. For more information: Propositional Logic

Conventions for notations in identifiers:

The recommended spelling of ¬ in identifiers is not.

def

absurd.{v} {a : Prop} {b : Sort v} (h₁ : a)
  (h₂ : ¬a) : b

Anything follows from two contradictory hypotheses. Example:

example (hp : p) (hnp : ¬p) : q := absurd hp hnp

For more information: Propositional Logic

def

Not.elim.{u_1} {a : Prop} {α : Sort u_1}
  (H1 : ¬a) (H2 : a) : α

Ex falso for negation: from ¬a and a anything follows. This is the same as absurd with the arguments flipped, but it is in the Not namespace so that projection notation can be used.

Implication is represented using function types in the universe of propositions. To prove A → B, it is enough to prove B after assuming A. This corresponds to the typing rule for Lean.Parser.Term.fun : termfun. Similarly, the typing rule for function application corresponds to modus ponens: given a proof of A → B and a proof of A, B can be proved.

Truth-Functional Implication

The representation of implication as functions in the universe of propositions is equivalent to the traditional definition in which A → B is defined as (¬A) ∨ B. This can be proved using propositional extensionality and the law of the excluded middle:

theorem truth_functional_imp {A B : Prop} :
    ((¬ A) ∨ B) = (A → B) := byA:PropB:Prop⊢ (¬A ∨ B) = (A → B)
  apply propextaA:PropB:Prop⊢ ¬A ∨ B ↔ A → B
  constructora.mpA:PropB:Prop⊢ ¬A ∨ B → A → Ba.mprA:PropB:Prop⊢ (A → B) → ¬A ∨ B
  .a.mpA:PropB:Prop⊢ ¬A ∨ B → A → B rintro (h | h) aa.mp.inlA:PropB:Proph:¬Aa:A⊢ Ba.mp.inrA:PropB:Proph:Ba:A⊢ B <;>a.mp.inlA:PropB:Proph:¬Aa:A⊢ Ba.mp.inrA:PropB:Proph:Ba:A⊢ B trivialAll goals completed! 🐙
  .a.mprA:PropB:Prop⊢ (A → B) → ¬A ∨ B intro ha.mprA:PropB:Proph:A → B⊢ ¬A ∨ B
    by_cases AposA:PropB:Proph:A → Bh✝:A⊢ ¬A ∨ BnegA:PropB:Proph:A → Bh✝:¬A⊢ ¬A ∨ B
    .posA:PropB:Proph:A → Bh✝:A⊢ ¬A ∨ B apply Or.inrpos.hA:PropB:Proph:A → Bh✝:A⊢ B; solve_by_elimAll goals completed! 🐙
    .negA:PropB:Proph:A → Bh✝:¬A⊢ ¬A ∨ B apply Or.inlneg.hA:PropB:Proph:A → Bh✝:¬A⊢ ¬A; trivialAll goals completed! 🐙

Logical equivalence, or “if and only if”, is represented using a structure that is equivalent to the conjunction of both directions of the implication.

structure

Iff (a b : Prop) : Prop

If and only if, or logical bi-implication. a ↔ b means that a implies b and vice versa. By propext, this implies that a and b are equal and hence any expression involving a is equivalent to the corresponding expression with b instead.

Conventions for notations in identifiers:

The recommended spelling of ↔ in identifiers is iff.
The recommended spelling of <-> in identifiers is iff (prefer ↔ over <->).

Constructor

Iff.intro

If a → b and b → a then a and b are equivalent.

Fields

mp : a → b

Modus ponens for if and only if. If a ↔ b and a, then b.

mpr : b → a

Modus ponens for if and only if, reversed. If a ↔ b and b, then a.

def

Iff.elim.{u_1} {a b : Prop} {α : Sort u_1}
  (f : (a → b) → (b → a) → α) (h : a ↔ b) : α

Non-dependent eliminator for Iff.

syntaxPropositional Connectives

The logical connectives other than implication are typically referred to using dedicated syntax, rather than via their defined names:

term ::= ...
    | `And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.term ∧ term

term ::= ...
    | `Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.


Conventions for notations in identifiers:

 * The recommended spelling of `∨` in identifiers is `or`.term ∨ term

term ::= ...
    | `Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.¬ term

term ::= ...
    | If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.term ↔ term