brain

The tactic `simp` performs normalization by repeated rewriting using a curated set of lemmas.

Propositional equality in Lean is generated from a small set of core operations.

Lemmas provide reusable equalities that drive most rewriting.

Rewriting is the primary way to apply propositional equalities in Lean.

In most proofs, equalities come from the local context.

Complex equalities are rarely achieved in a single step.

When types depend on values, rewriting affects both terms and their types.

Rewriting systems can diverge if rules are poorly oriented or interact cyclically.

Equality becomes useful when it propagates through larger expressions.

Propositional equality is the explicit notion of equality in Lean.

The behavior of `simp` depends entirely on the set of rewrite rules it uses.

Case analysis splits a goal according to the structure of a value.

Structures package multiple fields into a single value.

Equality between functions requires a different treatment than equality between values.

Substitution is the direct elimination of equalities from the context.

Definitional equality is the built-in notion of equality used by the kernel of Lean.

Reasoning often alternates between propositional equality `a = b` and boolean equality `a == b`.

Pattern matching performs case analysis by selecting a branch based on the shape of a value.

The `conv` tactic provides fine-grained control over rewriting.

Rewriting is most effective when guided by a small set of consistent strategies.

Rewriting can target either the goal or the local context.

In Lean, propositions live in `Prop`, a universe where proof irrelevance holds.

Rewriting failures in Lean usually come from a small set of recurring issues.

Even when the algorithmic idea is correct, implementations fail in predictable ways.

Data representation is the choice of concrete form used to store the objects in a problem.

Stability and determinism describe how predictably an algorithm behaves when there are ties, repeated values, or multiple valid answers.

Implementation discipline means translating an algorithm into code without changing its meaning accidentally.

Algorithms are usually described with mathematical integers and real numbers.

Benchmarking measures how an implementation behaves on real inputs and real hardware.

Randomized algorithms use random choices during execution.

Pseudocode is a bridge between the problem statement and an implementation.

Dynamic programming solves problems by storing answers to subproblems and reusing them.

Amortized analysis studies the average cost of operations over a sequence, even when individual operations are sometimes expensive.

A reduction transforms one problem into another problem.

A greedy algorithm builds a solution by making one locally best choice at a time.

Testing does not prove an algorithm correct, but it exposes mistakes in specifications, invariants, edge cases, and implementation details.

A brute force baseline is the simplest correct algorithm you can write from the problem statement.

Divide and conquer solves a problem by splitting it into smaller subproblems, solving those subproblems, and combining their answers.

A lower bound states that every algorithm for a problem must perform at least a certain amount of work in some model of computation.

Edge cases are valid inputs that sit at the boundary of the specification.

Space complexity measures how much memory an algorithm uses as a function of input size.

Big O notation provides a formal way to describe how a function grows.

Recursive algorithms replace loop structure with self-reference.

Time complexity describes how the running time of an algorithm grows as the input size grows.

Loop invariants are the primary tool for reasoning about iterative algorithms.

An algorithm does not operate on an abstract idea of data.

A correctness argument explains why an algorithm returns an acceptable output for every valid input.

An algorithm begins with a precise statement of the problem.

This section combines multiple patterns from the chapter into complete, end-to-end linked list algorithms.

Pointer code should be tested by checking structure, not only values.

An intrusive list stores the linkage fields inside the objects being linked.

Memory ownership describes which part of a program is responsible for creating, linking, unlinking, and destroying a node.

Edge cases are inputs that sit near the boundary of an algorithm's assumptions.

An iterator is an object or procedure that visits the nodes of a linked list one at a time.

Pointer aliasing occurs when two or more references point to the same node.

Linked list algorithms are dominated by pointer traversal and constant-time link updates.

A persistent list is a list that preserves older versions after an update.

A dummy head is a fixed node placed before the real head of a singly linked list.

A stack is a last-in, first-out (LIFO) structure.

A queue is a first-in, first-out structure.

A skip list augments a sorted linked list with multiple levels of forward pointers.

Insertion adds nodes into a linked list by creating new links while preserving reachability of all existing nodes.

An LRU cache stores a fixed number of key-value entries and removes the least recently used entry when capacity is exceeded.

A cycle exists in a linked list when some node’s `next` pointer eventually leads back to a previously visited node.

Deletion removes one or more nodes from a linked list by changing links around them.

Merging is a family of constructions that combine multiple linked lists into one or more output lists while preserving structural invariants.

Splitting a linked list means cutting one list into two or more lists while preserving the original nodes.

Reversal transforms a linked list so that the direction of all edges is flipped.

A singly linked list is a sequence of nodes where each node stores a value and a reference to the next node.

A sentinel node is an artificial node placed at the boundary of a linked list.

Fast and slow pointers are two references that traverse the same linked structure at different speeds.

Merging combines two sorted singly linked lists into one sorted list by relinking nodes.

A doubly linked list is a sequence of nodes where each node stores a value, a reference to the next node, and a reference to the previous node.

Spiral traversal visits a matrix layer by layer, moving right across the top row, down the right column, left across the bottom row, and up the left column,...

Boundary conditions define the valid domain of indices, ranges, and states in an algorithm.

Array and string problems often look different on the surface, but many reduce to a small number of reusable patterns.

Flood fill explores a connected region in a grid starting from a seed cell and marks or transforms all cells that belong to the same region.

Rolling hashes assign numeric fingerprints to substrings so that many substring comparisons can be done quickly.

Matrix traversal processes a two-dimensional array in a defined order.

String comparison determines the ordering or equality of two strings.

A trie is a tree structure for storing a set of strings so that common prefixes are shared.

Parsing expressions converts a sequence of tokens into a structured form that reflects operator precedence and associativity.

Anagrams are strings or sequences that contain the same elements with the same multiplicities, possibly in different order.

Substring search locates occurrences of a pattern `p` inside a text `s`.

A palindrome is a sequence that reads the same forward and backward.

A frequency table records how many times each value appears in an array, string, or stream.

Run-Length Encoding (RLE) compresses sequences by replacing consecutive equal values with a pair `(value, count)`.

Array rotation moves elements by a fixed offset while preserving their relative circular order.

Partitioning rearranges an array so that elements are grouped by a predicate.

String scanning is the basic operation behind parsing, tokenization, validation, search, and text normalization.

In-place modification changes an array without allocating another array of the same size.

Deduplication removes repeated values while preserving a chosen notion of identity and, optionally, order.

Tokenization converts a string into a sequence of meaningful units called tokens.

Sliding windows maintain a contiguous subarray `[l, r)` while both endpoints move forward.

The two pointers technique uses two indices that move through an array or string in a controlled way.

Prefix sums are a preprocessing technique for answering repeated range sum queries on an array.

Array traversal is the base operation for all algorithms over linear data.

A difference array is the inverse pattern of a prefix sum.

Lean proofs fail in predictable ways.

Lean provides automation to reduce routine proof steps.