logic | brain

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.25 Common Proof Mistakes and Debugging

Lean proofs fail in predictable ways. The error messages often indicate a mismatch between the goal and the available assumptions, or a misuse of tactics. Effective debugging is a disciplined process: inspect the goal, inspect the context, and identify the exact mismatch. Problem A proof does not compile. Typical symptoms: tactic failed, no goals solved type mismatch unknown identifier failed to unify You need a systematic way to locate and...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.24 Simplification and Automation

Lean provides automation to reduce routine proof steps. The goal is to remove mechanical transformations while preserving the logical structure of the argument. The main tool is simp , supported by targeted tactics such as dsimp , simp_all , and lightweight automation like aesop . Problem Manual rewriting becomes repetitive: rw [Nat.add_zero] rw [Nat.zero_add] rw [Nat.add_comm] This obscures the intent. You want Lean to perform standard reductions automatically while keeping...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.22 Backward Reasoning

Backward reasoning starts from the goal and reduces it to simpler subgoals. Instead of building forward from assumptions, you ask: what must be true for this goal to hold? Lean supports this style through tactics like apply , refine , and introduction rules. Problem You have a goal that is not directly provable from the current context, but there exists a hypothesis or theorem whose conclusion matches the goal. P...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.23 Rewriting Strategies

Rewriting with equality is one of the most frequent operations in Lean. At scale, the challenge is not knowing that rw exists, but deciding what to rewrite, where, and in which direction so the proof remains stable and readable. Problem You have equalities available, but naive rewriting: fails because the shape does not match succeeds but makes the goal harder applies too broadly and breaks later steps You need a...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.20 Using Assumptions Effectively

An assumption is a local term that Lean may use to solve the current goal or produce another proof. In simple proofs, assumptions are often the whole proof. In larger proofs, the main work is to recognize which assumption should be applied, destructured, rewritten, or contradicted. Problem You have several hypotheses in the local context, and you need to decide how to use them. A typical context may look like...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.21 Forward Reasoning

Forward reasoning starts from the assumptions in the local context and derives new facts until the goal becomes immediate. This style is useful when the proof has a natural data flow: one hypothesis produces an intermediate result, another hypothesis consumes it, and the final result follows. Problem You have assumptions that can be composed, but the goal is not directly available. P Q R : Prop hp : P hPQ...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.19 Local Context Management

The local context is the list of variables, hypotheses, instances, and intermediate facts available at a point in a proof. Most Lean proofs are won or lost by keeping this context small enough to read and rich enough to solve the current goal. Problem You want to control which assumptions are available, how they are named, and when they should be introduced, removed, or generalized. A typical proof state looks...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.18 Naming Conventions

Names in Lean carry meaning. They determine how easily a proof can be read, refactored, and extended. Good naming makes the structure of the argument visible without inspecting every term. Problem You want names that reflect the role of each hypothesis and intermediate result, instead of relying on generic placeholders like h , h1 , h2 . Principles Use names that encode: the proposition or structure being described the direction...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.17 Proof Structuring Patterns

A Lean proof should expose the shape of the argument. The goal is not merely to make the theorem compile. The goal is to make the proof local, stable, and readable when the surrounding file changes. Problem You have a theorem that can be proved in several ways, but the proof becomes hard to read because assumptions, intermediate facts, and final construction steps are mixed together. Solution Use a simple...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.16 Introduction and Elimination Rules

Every logical connective in Lean has two sides. An introduction rule explains how to prove the connective. An elimination rule explains how to use a proof of the connective. Most beginner proof failures come from applying the wrong side of this distinction. Problem You want a mechanical method for deciding what to do next from the shape of the goal or the shape of a hypothesis. If the connective appears...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.12 Universal Quantifiers

A universal statement asserts that a property holds for every element of a type. In Lean, a proof of a universally quantified statement is a function that takes an arbitrary element and returns a proof of the property for that element. The usual notation: ∀ x : α, P x is implemented as a dependent function type. Problem You want to prove or use a statement of the form: ∀...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.14 Proof by Contradiction

Proof by contradiction is a classical proof pattern. To prove a proposition P , assume ¬ P , derive False , and conclude P . In Lean, this is usually written with by_contra . Problem You want to prove: P but the easiest route is to show that assuming ¬ P creates a contradiction. Solution Use by_contra . open Classical theorem by_contra_basic (P : Prop) (h : ¬ P ->...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.15 Case Analysis

Case analysis is the proof pattern for using data that has more than one possible constructor. In logic, it appears most often with disjunctions, existentials, booleans, natural numbers, and inductive propositions. The basic rule is simple: if a hypothesis could have been built in several ways, prove the goal for each possible way. Problem You have a hypothesis whose type has constructors, and you want to use the information inside...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.13 Classical vs Constructive Logic

Lean is constructive by default. This affects which proofs are available and what information a proof must contain. Classical reasoning can be enabled explicitly when needed. Problem You want to understand why some statements are easy to prove in mathematics but require additional assumptions in Lean, and how to control that boundary. Constructive Logic In constructive logic, a proof must provide explicit evidence. To prove ∃ x, P x ,...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.9 Rewriting with Equality

Rewriting is the main way to use equality in Lean. If you have a proof h : a = b , then rw [h] replaces matching occurrences of a with b . This is the proof assistant version of substitution. Problem You have an equality hypothesis and want to use it to simplify the goal or a hypothesis. h : a = b ⊢ a + 1 = b +...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.10 Symmetry and Transitivity

Equality supports two structural operations: reversing direction (symmetry) and chaining steps (transitivity). These operations turn isolated equalities into usable proof pipelines. Problem You have equalities in the wrong direction, or you need to combine several equalities to reach a target. Symmetry If you know: h : a = b then you can reverse it to obtain: b = a Tactic form theorem eq_sym_tactic (a b : Nat) (h : a...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.11 Existential Quantifiers

An existential statement says that some object exists with a given property. In Lean, a proof of Exists P contains two pieces of data: a witness and a proof that the witness satisfies the predicate. The usual mathematical notation: ∃ x, P x means: Exists (fun x => P x) Problem You want to prove or use a statement of the form: ∃ x : α, P x To prove...

Programming › Lean › Chapter 2. Propositions and Proofs ›

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 :=...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.6 False and Contradiction

False is the proposition with no constructors. It represents an impossible proof state. If the local context contains a proof of False , Lean can prove any proposition from it. Problem You want to use an impossible hypothesis to finish a proof, or you want to show that a collection of assumptions is contradictory. Solution Use cases on a proof of False . theorem false_elim_example (P : Prop) : False...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.8 Equality Basics

Equality expresses that two terms are identical. In Lean, equality is a proposition. A proof of a = b allows you to replace a with b in other expressions. Problem You want to prove statements involving equality or use equalities to transform goals. Core Idea Equality in Lean is written: a = b A proof of this type shows that a and b are interchangeable. Reflexivity Every term is equal...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.5 Negation

Negation represents "not". In Lean, ¬ P means that a proof of P would lead to False . So a proof of ¬ P is a function from P to False . ¬ P is notation for: P -> False Problem You want to prove or use a statement of the form: ¬ P To prove it, assume P and derive a contradiction. To use it, apply it to a...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.1 Propositions as Types

Lean identifies propositions with types and proofs with terms. This identification is the foundation of all proof construction in Lean. It is precise and operational. You do not reason about propositions abstractly. You construct inhabitants of types. Problem You want a model where logical statements can be manipulated with the same rules used for programs, so that proofs can be constructed, checked, and composed mechanically. Core Principle A proposition is...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.4 Disjunction

Disjunction represents "or". A proof of P ∨ Q contains one piece of evidence: either a proof of P or a proof of Q , tagged with the side from which it came. In Lean, disjunction behaves like a sum type for propositions. Problem You want to prove or use a statement of the form: P ∨ Q To prove it, you must choose one side and provide a proof...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.3 Conjunction

Conjunction represents "and". A proof of P ∧ Q contains two pieces of evidence: a proof of P and a proof of Q . In Lean, conjunction behaves like a pair whose fields are logical proofs. Problem You want to prove or use a statement of the form: P ∧ Q To prove it, you must prove both sides. To use it, you may extract either side. Solution Use constructor...

Programming › Lean › Chapter 2. Propositions and Proofs ›

2.2 Implication and Functions

Implication is the first logical connective to understand in Lean because it is also the ordinary function type. A proof of P -> Q is a function that receives a proof of P and returns a proof of Q . Problem You want to prove a statement of the form: P -> Q In Lean, this means you must write a function from proofs of P to proofs of Q...