Propositions

This chapter introduces the type of propositions in Lean, along with fundamental logical connectives (∧, ∨, →, ¬, ↔︎). We will learn how to construct basic proofs using these concepts. By the end of this chapter, we will be able to write and prove simple logical statements in Lean.

What is a Proposition?

Propositions are statements that express a definite claim. In Lean, propositions belong to the built-in type Prop, which is fundamental to Lean’s logical system.

Examples:

• 2 + 2 = 4 is a proposition (true).
• 3 < 1 is also a proposition (false).

propositions.lean

-- Prop is the type of all propositions in Lean
#check Prop
#print Prop
-- Examples
#check 2 + 2 = 4
#check 3 < 1

In Lean, a proposition is a type that represents a logical statement. This means that propositions themselves are types, and proving a proposition is equivalent to constructing a term of that type. If we declare a variable P of type Prop, we can later define another variable h of type P. In Lean’s type-theoretic framework, we interpret h as a proof of P.

propositions.lean

variable (P : Prop)
variable (h : P)
-- We need to understand h as a proof of P
#check h

Declaring a variable P : Prop does not mean that P is immediately true. It simply introduces P as a proposition.

A proposition P is true if and only if there exists a term of type P—that is, a proof of P. If we can construct a term h : P, then P is true. Conversely, if no such term exists, then P is false. For example

• 2 + 2 = 4 is true because Lean can construct a proof of this proposition.
• 3 < 1 is false because no proof (no term of this type) can be constructed.

This perspective is central to constructive logic, where truth means having an explicit proof.

First proofs

The following Lean code defines a theorem called Th1. Let’s examine its components step by step to understand its purpose and functionality.

Th1.lean

theorem Th1 (h : P) : P := by
  exact h

This code defines a theorem named Th1. In Lean, a theorem is a proposition that has been or will be proven.

• (h : P) introduces a hypothesis h of type P, meaning h serves as a proof of the proposition P.
• : P represents the conclusion, stating that the theorem will establish the truth of P.
• := by signals that the proof will be constructed interactively using tactics, entering proof mode through indentation.
• The exact h tactic completes the proof by instructing Lean to use h (a proof of P) to establish P.

Essentially, Th1 asserts a fundamental logical principle: if a proof of P exists (h : P), then P is true. While seemingly obvious, this concept underlies the foundations of formal reasoning in Lean.

The theorem Th1 is now a reusable component that can be referenced and applied wherever needed, allowing us to build on previous results.

When checking its type, Lean shows ∀ (P : Prop), P → P. This indicates that P is an arbitrary proposition, and Th1 is a function that takes a proof of P and returns a proof of P. In other words, Th1 P belongs to the function type P → P.

Since we previously defined h : P, applying Th1 to P and h —written as Th1 P h— yields an element of type P. We will explore this concept further in the next sections.

Th1.lean

-- Th1 has type ∀ (P : Prop), P → P
#check Th1
-- Th1 P has type P → P
#check Th1 P
-- Th1 P h has type P
#check Th1 P h

Notice that Th1 is adaptable to any proposition it is applied to. For example, if we introduce a new variable Q : Prop, then Th1 Q becomes an element of type Q → Q. This means Th1 can be used with any proposition, reinforcing its generality in formal reasoning.

Th1.lean

variable (Q : Prop)
-- Th1 Q has type Q → Q
#check Th1 Q

It is worth noting that when we use #print Th1, Lean returns the following code:

theorem Th1 : ∀ (P : Prop), P → P := fun P h => h

The difference occurs because Lean automatically generalizes Th1 to its most abstract form.

However, this notation can sometimes be cumbersome since applying a theorem requires explicitly providing all necessary hypotheses. To simplify this, we can define implicit variables. For example, let’s introduce our second theorem:

Th2.lean

theorem Th2 {P : Prop} (h : P) : P := by
  exact h

The curly braces around P indicate that P is an implicit variable. This means that Lean will automatically infer the value of P based on the context when Th2 is used, so we don’t need to manually provide P as an argument each time. This makes the code cleaner and more concise, as Lean handles the inference for us.

Th2.lean

-- Th2 has type ∀ {P : Prop}, P → P
#check Th2
-- Th2 h has type P, infered from h
#check Th2 h

We can also prove this theorem using a third method, where we employ the apply tactic. The apply tactic allows us to use a previously defined theorem—in this case, Th2—to progress towards the current goal.

For apply to work, the conclusion of the theorem we want to apply must match or be unifiable with the current goal, which is true in this case. Once we apply Th2, Lean will prompt us to prove the necessary hypotheses required by the theorem to complete the proof. This approach leverages the power of previously established results to build new proofs more efficiently.

Th3.lean

theorem Th3 {P : Prop} (h : P) : P := by
  apply Th2
  exact h

have

The have keyword in Lean is a powerful tool used in proofs to introduce intermediate results or hypotheses. It helps break down complex proofs into smaller, more manageable steps by allowing us to prove and name intermediate statements. These intermediate results can be referenced later in the proof, making the overall structure clearer and easier to follow. This approach is particularly useful when working through multi-step arguments, as it enables us to focus on individual pieces of the proof before combining them to reach the final conclusion.

Th4.lean

theorem Th4 {P : Prop} (h : P) : P := by
  have h2 : P := by
    exact h
  exact h2

apply? exact?

One of the most powerful features of Lean is the ability to use the apply? command within a proof. The apply? tactic automatically searches through the available theorems in the current context and suggests relevant ones that could be applied to prove the current goal. For example, in the theorem Th3 above, if we write apply?, Lean responds with

Try this: exact h

Additionally, we can use the exact? tactic to prompt Lean to suggest the hypothesis needed to conclude a theorem. When invoked, exact? analyzes the current goal and offers possible hypotheses or terms that could directly satisfy the goal.

These tactics are especially useful when working with numerous results, as they save time by automatically searching for and suggesting relevant theorems or hypotheses. This eliminates the need to manually search for the specific result needed, streamlining the proof process significantly.

example

We can use the example keyword to define an anonymous theorem. This allows us to demonstrate a proof without giving it a specific name. The structure is similar to a regular theorem, but the difference is that it’s not assigned a name, making it ideal for quick demonstrations or illustrating concepts. Here’s an example that follows the structure from above:

Example.lean

example (h : P) : P := by
  exact h

Since examples are anonymous, they cannot be referenced or reused later in the code.

sorry

The sorry command in Lean is a placeholder that allows us to temporarily skip the proof of a theorem or definition. When we use sorry, Lean assumes that the proof is correct without actually verifying it. This can be useful during the development process when we want to focus on the structure of our code or test parts of our work without completing all the proofs. However, it’s important to note that sorry does not provide a valid proof. If left in the code, Lean cannot guarantee the correctness of the theorem or definition, as the proof is incomplete. It’s a useful tool for incremental development, but should be removed or replaced with a valid proof before finalizing the code.

Sorry.lean

theorem Th3 (h : P) : P := by
  sorry

Logical connectives

In this section, we will introduce logical connectives, explore their implementation in Lean, and demonstrate how to prove statements involving them.

Conjunction

The logical And connective, represented by the symbol ∧ (which can be typed in Lean using \and), is used to combine two propositions, asserting that both are true simultaneously. In Lean, the And connective is implemented as a built-in logical construct. Specifically, if P and Q are propositions, then P ∧ Q is also a proposition. This is read as “P and Q,” meaning that P is true and Q is true.

And.lean

#check And P Q
#check P ∧ Q

If we #print And, Lean returns

structure And : Prop → Prop → Prop
number of parameters: 2
constructor:
And.intro : ∀ {a b : Prop}, a → b → a ∧ b
fields:
left : a
right : b

This declares And as a structure in Lean. And takes two arguments of type Prop and returns a new Prop. In other words, And is a binary logical connective, requiring two parameters, both of type Prop. The constructor for And is And.intro, which is a function that takes two propositions a and b (implicitly defined) and two proofs —one proof of a (of type a) and one proof of b (of type b)— and returns a proof of a ∧ b. Here’s an example of how the constructor works:

And.lean

-- To prove a proposition of the form P ∧ Q
-- we need a proof of P and a proof of Q
theorem ThAndIn (hP : P) (hQ : Q) : P ∧ Q := by
  exact And.intro hP hQ 

The And structure has two fields: left and right. The left field stores the proof of the first proposition a, and the right field stores the proof of the second proposition b. These fields are essential for constructing a proof of a ∧ b, as they hold the individual proofs required to establish the truth of both propositions simultaneously. Here’s an example of how the fields work:

And.lean

-- From a proof of P ∧ Q, we can obtain a proof of P
theorem ThAndOutl (h : P ∧ Q) : P := by
  exact h.left
-- We can also obtain a proof for Q
theorem ThAndOutr (h : P ∧ Q) : Q := by
  exact h.right

Disjunction

The logical Or connective, represented by the symbol ∨ (which can be typed in Lean using \or), is used to combine two propositions, asserting that at least one of them is true. In Lean, the Or connective is implemented as a built-in logical construct. Specifically, if P and Q are propositions, then P ∨ Q is also a proposition. This is read as “P or Q,” meaning that P is true or Q is true.

Or.lean

#check Or P Q
#check P ∨ Q

If we #print Or, Lean returns

inductive Or : Prop → Prop → Prop
number of parameters: 2
constructors:
Or.inl : ∀ {a b : Prop}, a → a ∨ b
Or.inr : ∀ {a b : Prop}, b → a ∨ b

This declares Or as an inductive type in Lean. Or takes two arguments of type Prop and returns a new Prop. In other words, Or is a binary logical connective that requires two parameters, both of which are of type Prop. There are two constructors for Or: Or.inl and Or.inr. These constructors are functions that take two propositions, a and b, implicitly defined, and a proof—either a proof of a (of type a) or a proof of b (of type b)—and return a proof of a ∨ b. The two constructors Or.inl and Or.inr correspond to the two possible ways a disjunction can be true: either by proving a or by proving b. Here’s an example of how the constructors work:

Or.lean

-- From a proof of P, we can obtain a proof of P ∨ Q
theorem ThOrInl (h : P) : P ∨ Q := by
  exact Or.inl h
-- From a proof of Q, we can obtain a proof of P ∨ Q
theorem ThOrInr (h : Q) : P ∨ Q := by
  exact Or.inr h

Unlike the And type, Or does not have fields associated with it. However, the absence of fields does not mean we cannot reason with elements of this type. In cases where we have a hypothesis of type P ∨ Q, we can reason by cases. In Lean, the cases keyword is used for pattern matching and case analysis on inductive types. It allows us to break down a hypothesis or term into its possible constructors and handle each case separately.

For example, if we have a hypothesis of type P ∨ Q, we know that there are two possible cases to consider: either we have a proof of P (using Or.inl), or we have a proof of Q (using Or.inr). The cases tactic will break down the goal into two branches, one for each case, allowing us to reason about each case individually. Let’s look at how we can use cases to handle such a scenario:

Or.lean

-- From a proof of P ∨ Q, we can obtain a proof of Q ∨ P
theorem ThOrCases (h : P ∨ Q) : Q ∨ P := by
  cases h 
  -- Case 1
  rename_i hP
  exact Or.inr hP
  -- Case 2
  rename_i hQ 
  exact Or.inl hQ 

This code defines a theorem in Lean that demonstrates how to reason by cases using the cases tactic. The theorem proves that if you have a proof of P ∨ Q, you can derive a proof of Q ∨ P. Here’s how the proof works:

1. Hypothesis: We start with the hypothesis h : P ∨ Q, which asserts that at least one of the propositions P or Q is true.

2. Case Analysis with cases: The cases tactic is applied to h to break it into two subgoals, each corresponding to a possible way the disjunction could have been constructed:

   • Case 1: If h is constructed using Or.inl, it means we have a proof of P (denoted hP using rename_i), so hP : P. To prove Q ∨ P, we use Or.inr to inject P into the right side of the disjunction, giving us the proof Q ∨ P.
   • Case 2: If h is constructed using Or.inr, it means we have a proof of Q (denoted hQ using rename_i), so hQ : Q. To prove Q ∨ P, we use Or.inl to inject Q into the left side of the disjunction, completing the proof.

In both cases, we construct a valid proof of Q ∨ P by appropriately using the constructors Or.inl and Or.inr. The cases tactic allows us to handle each scenario separately and derive the desired result.

We can alternatively use the keyword Or.elim to provide an alternative proof by cases.

Or.lean

theorem ThOrCases2 (h : P ∨ Q) : Q ∨ P := by
  apply Or.elim h
  -- Case P
  intro hP
  exact Or.inr hP
  -- Case Q
  intro hQ
  exact Or.inl hQ

Implication

The logical implication connective, represented by the symbol → (which can be typed in Lean using \to), is used to combine two propositions and describe a conditional relationship between them. Specifically, if P and Q are propositions, then P → Q is also a proposition, which reads as “if P, then Q”, or “P implies Q.” This means that if P is true, then Q must also be true. If P is false, the implication P → Q is considered true regardless of the truth value of Q. This is known as a vacuous truth.

In Lean, implication is treated as a function type: a proof of P → Q is a function that takes a proof of P and produces a proof of Q. To prove an implication P → Q, you assume that P is true and then show that Q must also be true under this assumption. This is typically done using the intro tactic, which introduces the assumption P into the proof context. Let’s look at an example to illustrate this.

Implication.lean

-- From a proof of Q, we can obtain a proof of P → Q
theorem ThImpIn (hQ : Q) : P → Q := by
  intro hP
  exact hQ

Additionally, if we have a proof of P → Q and a proof of P, we can derive a proof of Q. This is an application of modus ponens, a fundamental rule of inference in logic. The process involves applying the proof of P → Q to the proof of P, which allows us to conclude Q.

Conceptually, this process is similar to how a function operates: just as a function takes an input and transforms it into an output, the implication P → Q takes the proof of P (the input) and transforms it into a proof of Q (the output).

Implication.lean

-- From a proof P → Q and a proof of P, we can obtain a proof of Q
theorem ThModusPonens (h : P → Q) (hP : P) : Q := by
  exact h hP

Double implication

The double implication connective, Iff (represented by the symbol ↔︎, which can be typed in Lean using \iff), is used to combine two propositions, expressing a biconditional relationship between them. Specifically, if P and Q are propositions, then P ↔︎ Q is also a proposition. This is read as “P if, and only if, Q,” meaning that P is true if Q is true, and Q is true if P is true.

In other words, P ↔︎ Q asserts that P and Q are logically equivalent: if one is true, the other must also be true, and if one is false, the other must also be false. This biconditional relationship combines two implications: P → Q and Q → P. Both directions must hold for P ↔︎ Q to be true, meaning that P and Q are interchangeable in terms of truth values.

Iff.lean

#check Iff P Q
#check P ↔ Q

If we #print Iff, Lean returns

structure Iff : Prop → Prop → Prop
number of parameters: 2
constructor:
Iff.intro : ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
fields:
mp : a → b
mpr : b → a

Thus, Iff is a structure that takes two propositions (a and b) as inputs and returns a new proposition (a ↔︎ b). The constructor for Iff is named Iff.intro. It requires two proofs: one of a → b and one of b → a. Using these two proofs, it constructs a proof of a ↔︎ b.

Additionally, the Iff structure has two fields: - mp (short for modus ponens), which is a proof of a → b - mpr (short for modus ponens reverse), which is a proof of b → a.

These fields store the two implications that together prove the equivalence a ↔︎ b. Essentially, the double implication a ↔︎ b is shorthand for the conjunction (a → b) ∧ (b → a), as we can see below:

Iff.lean

-- From P ↔ Q we can derive (P → Q) ∧ (Q → P)
theorem ThIffOut (h : P ↔ Q) : (P → Q) ∧ (Q → P) := by
  apply And.intro
  -- Left
  exact h.mp
  -- Right
  exact h.mpr 

In the previous proof, from P ↔︎ Q, we can derive (P → Q) ∧ (Q → P). To do this, we use the And.intro constructor To obtain the left hand side of the desired proposition we use the mp field and to obtain the right hand side we use the mpr field.

Iff.lean

-- From (P → Q) ∧ (Q → P) we can derive P ↔ Q 
theorem ThIffIn (h1 : P → Q) (h2 : Q → P) : P ↔ Q := by 
  exact Iff.intro h1 h2 

In the previous proof, from P → Q and Q → P we can derive P ↔︎ Q. To do this, we use the Iff.intro constructor.

True

The logical constant True is a proposition that is always true.

True.lean

#check True

If we #print True, Lean returns

inductive True : Prop
number of parameters: 0
constructors:
True.intro : True

The True type in Lean represents the logical proposition true. It is a proposition and has no parameters. The only constructor for True is True.intro. This constructor is the canonical proof of the proposition True. When we use True.intro, we are essentially providing a proof that True is true, which completes any proof that requires a True proposition.

True.lean

-- True can always be obtained
theorem ThTrueIn : True := by
  exact True.intro

An alternative way to obtain a proof of True is to write trivial, which is an element of type True.

True.lean

-- Trivial is an element of type True
theorem ThTrivial : True := by
  exact trivial

False

The logical constant False is a proposition that is always false.

False.lean

#check False

If we #print False, Lean returns

inductive False : Prop
number of parameters: 0
constructors:

The False type in Lean represents the logical proposition false. It is an inductive type, but unlike True, it has no constructors. This means that no terms or proofs of type False can exist. The absence of constructors implies that the type is uninhabited—there is no way to construct a proof of False. Given that False has no constructors, the principle of ex falso quodlibet (from falsehood, anything follows) holds: if we can derive a proof of False, we can derive any other proposition. This is the logical principle that allows us to infer arbitrary conclusions from a contradiction. To apply this principle, Lean provides the tactic False.elim. This tactic allows us to derive any proposition from a proof of False.

False.lean

-- False implies any proposition
theorem ThExFalso : False → P := by
  intro h 
  exact False.elim h

Negation

In Lean, the negation connective Not, represented by the symbol ¬, is used to express the negation of a proposition. Specifically, if P is a proposition, then ¬P is another proposition that reads as not P. In logical terms, ¬P means that P is false.

Not.lean

#check Not P
#check ¬P

If we #print Not, Lean returns

def Not : Prop → Prop :=
fun a => a → False

That is, ¬P is an abbreviation for the implication P → False. Therefore, to prove ¬P, we need to show that assuming P leads to a contradiction. Let’s see an example.

Not.lean

theorem ThModusTollens (h1 : P → Q) (h2 : ¬Q) : ¬P := by
  -- Assume P is true (to prove ¬P, which is P → False).
  intro h3
  -- Derive Q from P → Q and P.
  have h4 : Q := by
    exact h1 h3
  -- Use ¬Q (Q → False) and Q to derive False.
  exact h2 h4

In the above theorem, we are given the hypotheses h1 : P → Q and h2 : ¬Q, and our goal is to prove ¬P. To do this, we begin by assuming P and aim to derive False. From the assumption P, we can use h1 : P → Q to derive Q. Then, since we also have h2 : ¬Q, which asserts that Q is false, we reach a contradiction. This contradiction allows us to conclude False, which completes the proof of ¬P. The theorem demonstrates the well-known logical principle of Modus Tollens, a fundamental rule in classical logic.

Decidable propositions

A proposition is decidable if we can constructively determine whether it is true or false. That is, we have either a proof of the proposition or a proof of its negation. In Lean, decidability of a proposition is captured by the inductive type Decidable.

If we #print Decidable, Lean returns

inductive Decidable : Prop → Type
number of parameters: 1
constructors:
Decidable.isFalse : {p : Prop} → ¬p → Decidable p
Decidable.isTrue : {p : Prop} → p → Decidable p

Decidable takes a proposition p : Prop as a parameter. This type expresses the idea that we can constructively decide whether p holds or not—that is, we can either prove p or prove its negation ¬p. The Decidable type has two constructors: Decidable.isTrue and Decidable.isFalse. The constructor isTrue takes a proof of p and yields a value of type Decidable p, indicating that p is provably true. Conversely, isFalse takes a proof of ¬p and returns a value of type Decidable p, indicating that p is provably false.

In the code below, we prove that True and False are decidable, and that each logical connective is decidable—provided that the propositions they operate on are themselves decidable.

Decidable.lean

-- True is decidable
def DecidableTrue : Decidable True := by
  exact isTrue trivial

-- False is decidable
def DecidableFalse : Decidable False := by
  exact isFalse id

-- If `P` is decidable, then `¬ P` is decidable
def DecidableNot {P : Prop} : Decidable P → Decidable (¬ P) := by
  intro hP
  match hP with
    | isFalse hP => exact isTrue  (fun h => False.elim (hP h))
    | isTrue hP  => exact isFalse (fun h => False.elim (h hP))

-- If `P` and `Q` are decidable, then `P ∧ Q` is decidable
def DecidableAnd {P Q : Prop} : Decidable P → Decidable Q → Decidable (P ∧ Q) := by
  intro hP hQ
  match hP, hQ with
    | isFalse hP, _           => exact isFalse (fun h => hP h.left)
    | _         , isFalse hQ  => exact isFalse (fun h => hQ h.right)
    | isTrue hP , isTrue hQ   => exact isTrue (And.intro hP hQ)

-- If `P` and `Q` are decidable, then `P ∨ Q` is decidable
def DecidableOr {P Q : Prop} : Decidable P → Decidable Q → Decidable (P ∨ Q) := by
  intro hP hQ
  match hP, hQ with
    | isTrue hP , _            => exact isTrue (Or.inl hP)
    | _         , isTrue hQ    => exact isTrue (Or.inr hQ)
    | isFalse hP, isFalse hQ   => exact isFalse (fun h => h.elim hP hQ)

-- If `P` and `Q` are decidable, then `P → Q` is decidable
def DecidableImplies {P Q : Prop} : Decidable P → Decidable Q → Decidable (P → Q) := by
  intro hP hQ
  match hP, hQ with
    | isFalse hP , _          => exact isTrue  (fun h => False.elim (hP h))
    | _          , isTrue hQ  => exact isTrue  (fun _ => hQ)
    | isTrue hP  , isFalse hQ => exact isFalse (fun h => hQ (h hP))

-- If `P` and `Q` are decidable, then `P ↔ Q` is decidable
def DecidableIff {P Q : Prop} : Decidable P → Decidable Q → Decidable (P ↔ Q) := by
  intro hP hQ
  have hPtoQ : Decidable (P → Q) := DecidableImplies hP hQ
  have hQtoP : Decidable (Q → P) := DecidableImplies hQ hP
  match hPtoQ, hQtoP with
    | isFalse hPtoQ, _ => exact isFalse (fun h => hPtoQ h.mp)
    | _, isFalse hQtoP => exact isFalse (fun h => hQtoP h.mpr)
    | isTrue  hPtoQ, isTrue  hQtoP => exact isTrue (Iff.intro hPtoQ hQtoP)

Classical Logic

The statement P ∨ ¬P is a classic example of a proposition that cannot be proven in general without additional assumptions. This is because Lean’s logic is based on intuitionistic logic by default, which does not assume that every proposition must be either true or false. In intuitionistic logic, to prove P ∨ ¬P, we would need to provide a constructive proof for either P or ¬P, but such a proof does not always exist. Without more information about P, there is no general method to construct a proof of either P or ¬P. However, if we wish to work within classical logic in Lean, we can explicitly assume the law of excluded middle as an axiom. Lean provides a mechanism for doing this through the Classical namespace. Here’s how we can prove P ∨ ¬P using classical logic.

Em.lean

-- We open the `Classical` namespace
open Classical
-- We use `Classical.em` to prove the excluded middle
theorem ThExcludedMiddle : P ∨ ¬P := by
  exact em P

Another important classical equivalence is between P and ¬¬P. In classical logic, this equivalence allows for proving propositions by contradiction. To prove a proposition P by contradiction, we assume ¬P and derive a contradiction. This gives us ¬¬P, and by the equivalence between P and ¬¬P, we can conclude that P is true. This form of reasoning, known as proof by contradiction, can be reproduced in Lean by using the byContradiction tactic, as demonstrated below.

ByContra.lean

-- Classical Logic allows proofs by contradiction
theorem ThDoubNeg : P ↔ ¬¬P := by
  apply Iff.intro
  -- Implication P → ¬¬P
  intro hP
  intro hNP
  exact hNP hP
  -- Implication ¬¬P → P
  intro hNNP
  have hF : ¬P → False := by
    intro hNP
    exact hNNP hNP
  apply byContradiction hF

We observe that in the equivalence between P and ¬¬P, the implication P → ¬¬P holds in intuitionistic logic. However, the converse, ¬¬P → P, is the key result that the byContradiction tactic relies on. In intuitionistic logic, we cannot conclude P simply because assuming ¬P leads to a contradiction. Instead, intuitionistic logic only allows us to derive ¬¬P from such a contradiction, meaning that we can assert it is not the case that P is false, but we cannot constructively prove P itself. Therefore, the step from ¬¬P to P (double negation elimination) is not valid in intuitionistic logic, as it goes beyond what is constructively derivable.

An alternative is to use false_or_by_contra, which transforms the goal into False, switching to classical reasoning if the goal is not decidable.

Exercises

The following exercises are sourced from Daniel Clemente’s website.

Exercises.lean

namespace Exercises
variable (A B C D I L M P Q R : Prop)

theorem T51 (h1: P) (h2: P → Q) : P ∧ Q := by sorry

theorem T52 (h1: P ∧ Q → R) (h2: Q → P) (h3: Q) : R := by sorry

theorem T53 (h1: P → Q) (h2: Q → R) : P → (Q ∧ R) := by sorry

theorem T54 (h1: P) : Q → P := by sorry

theorem T55 (h1: P → Q) (h2: ¬Q) : ¬P := by sorry

theorem T56 (h1: P → (Q → R)) : Q → (P → R) := by sorry

theorem T57 (h1: P ∨ (Q ∧ R)) : P ∨ Q := by sorry

theorem T58 (h1: (L ∧ M) → ¬P) (h2: I → P) (h3: M) (h4: I) : ¬L := by sorry

theorem T59 : P → P := by sorry

theorem T510 : ¬ (P ∧ ¬P) := by sorry

theorem T511 : P ∨ ¬P := by sorry

theorem T512 (h1: P ∨ Q) (h2: ¬P) : Q := by sorry

theorem T513 (h1: A ∨ B) (h2: A → C) (h3: ¬D → ¬B) : C ∨ D := by sorry

theorem T514 (h1: A ↔ B) : (A ∧ B) ∨ (¬A ∧ ¬B) := by sorry

end Exercises