The Exam Mindset

The final is handwritten. That changes the goal: you are not trying to memorize Lean output, you are training proof-state prediction. A proof state has a context above the line and a goal below it. Before each tactic step, ask what the context contains and what exact goal remains.

One Safe First Move

If the goal is an implication, use assume. If the goal is Q -> P, assume q : Q; the remaining goal becomes P, already available as p. If the goal instead matches a term in the context exactly, exact closes it.

variables P Q : Prop
example (p : P) : Q -> P :=
begin
  assume q,
  exact p,
end

The Evidence Problem

From not (P /\ Q), you know the pair cannot exist. You do not yet know whether P failed, whether Q failed, or both. That is why the direction not (P /\ Q) -> not P \/ not Q needs classical help in the course treatment.

Classical De Morgan Pattern

variables P Q : Prop
open classical

theorem dm2_em :
  not (P /\ Q) -> not P \/ not Q :=
begin
  assume npq,
  cases em P with p np,
  right,
  assume q,
  apply npq,
  constructor,
  exact p,
  exact q,
  left,
  exact np,
end

Universal Chaining

variables A : Type
variables PP QQ : A -> Prop

example : (forall x : A, PP x) ->
  (forall y : A, PP y -> QQ y) ->
  forall z : A, QQ z :=
begin
  assume p pq a,
  apply pq,
  apply p,
end

Existential Chaining

variables A : Type
variables PP QQ : A -> Prop

example : (exists x : A, PP x) ->
  (forall y : A, PP y -> QQ y) ->
  exists z : A, QQ z :=
begin
  assume p pq,
  cases p with a pa,
  existsi a,
  apply pq,
  exact pa,
end

Boolean Definition From Rows

Fix the first Boolean input. If the row pattern says "return the second input", write | tt b := b. If it says "always true", write | ff b := tt.

def bimp : bool -> bool -> bool
| tt b := b
| ff b := tt

Natural Reduction Trace

For course-style addition, recursion follows the second argument. Reduction means unfolding the matching equation until constructors remain:

def add : ℕ -> ℕ -> ℕ
| m 0 := m
| m (nat.succ n) := nat.succ (add m n)

So reduce by stripping successors from the second input until the base case appears.

Boolean Definitions Worth Knowing

def bxor : bool -> bool -> bool
| tt b := bnot b
| ff b := b

def biff : bool -> bool -> bool
| tt b := b
| ff b := bnot b

bxor flips the second input when the first input is true. biff keeps the second input when the first input is true and flips it when the first input is false.

Boolean-to-Proposition Bridge

&&, ||, and bnot compute on Boolean data. /\, \/, and not combine propositions. The lecture bridge is is_tt b, meaning the Boolean value b is true as a proposition.

List Shape

#check (@list.nil)
#check (@list.cons)

[1,2,3] is shorthand for 1 :: 2 :: 3 :: []. If a :: l = b :: m, then injection gives equality of heads and equality of tails. No-confusion says nil cannot equal a cons list.

Tree Shape

inductive Tree : Type
| leaf : Tree
| node : Tree -> ℕ -> Tree -> Tree

Tree sort builds a binary-search tree, then reads it with in-order traversal: left subtree, root, right subtree.

Insertion Example

The revision notes keep the list-insertion example ins 5 [6, 4, 2]. With the retained comparator, it reduces to [6, 5, 4, 2]. The exam skill is to trace one comparison at a time, not to recite the whole sorting algorithm.

What Can Be Tested

No-confusion and injectivity matter. [] cannot equal a :: l, and a :: l = b :: m gives both a = b and l = m. The notes say the injection tactic itself is not the exam target, but the injective property is still fair game.