Proofs and Tactics | Cryptography Academy

Proofs Are Programs

In Lean, a proof of a proposition P is a term of type P. This is the Curry-Howard correspondence: propositions are types, proofs are programs.

-- The proposition "2 + 2 = 4" is a type
#check (2 + 2 = 4)  -- : Prop

-- A proof is a term of that type
example : 2 + 2 = 4 := rfl  -- rfl proves equality by computation

Key insight: When you see theorem foo : P := proof, read it as "foo is a proof of P".

Tactic Mode

Writing proofs directly as terms is possible but tedious. Tactics let you build proofs interactively, step by step. Enter tactic mode with by:

theorem add_comm_example (a b : Nat) : a + b = b + a := by
  -- Goal: a + b = b + a
  apply Nat.add_comm
  -- No more goals!

Each tactic transforms the current goal (what we need to prove) into simpler subgoals, until no goals remain.

Essential Tactics

These tactics appear frequently in cryptographic proofs:

intro

Introduces hypotheses. When the goal is ∀ x, P x or A → B, intro brings the variable or assumption into scope.

example : ∀ n : Nat, n = n := by
  intro n      -- introduces n, goal becomes: n = n
  rfl

apply

Uses a theorem or hypothesis. If we have h : A → B and goal B, then apply h changes the goal to A.

example (h : ∀ n, n + 0 = n) : 5 + 0 = 5 := by
  apply h     -- uses h with n = 5

exact

Provides exactly the term needed to close the goal.

example (h : 2 + 2 = 4) : 2 + 2 = 4 := by
  exact h     -- h is exactly what we need

rw (rewrite)

Substitutes equals for equals. If h : a = b, then rw [h] replaces a with b in the goal.

example (a b : Nat) (h : a = b) : a + 1 = b + 1 := by
  rw [h]      -- substitutes a with b, closes by rfl automatically

native_decide

Proves decidable propositions by computation. Useful for numeric equalities.

example : (1 + 2) * 3 = 9 := by
  native_decide  -- computes and verifies

constructor / cases

constructor builds a structure or And/Exists. cases destructs a hypothesis into its components.

-- Proving an And
example : 1 = 1 ∧ 2 = 2 := by
  constructor    -- splits into two goals
  · rfl          -- proves 1 = 1
  · rfl          -- proves 2 = 2

-- Using an And hypothesis
example (h : 1 = 1 ∧ 2 = 2) : 1 = 1 := by
  cases h with   -- splits h into left and right
  | intro left right => exact left

Reading a Proof

Here's a complete proof you might see in cryptographic formalization:

-- Binding property: can't open a commitment two ways
theorem binding (scheme : CommitmentScheme M R C)
    (h : scheme.commit m₁ r₁ = scheme.commit m₂ r₂)
    (hbind : scheme.isBinding) : m₁ = m₂ := by
  -- Apply the binding property
  apply hbind
  -- Provide the witness: same commitment
  exact h

Reading this proof:

We have a commitment scheme and know two commit outputs are equal
apply hbind uses the binding property, which says equal commitments imply equal messages
exact h provides the proof that the commitments are equal

The sorry Escape Hatch

sorry is a placeholder that "proves" anything. It's used for incomplete proofs:

theorem incomplete : 1 = 2 := by
  sorry  -- This "proves" the false statement!

Warning: Any theorem using sorry is not actually proven. Lean will warn you, and the theorem cannot be trusted. On this site, we clearly mark which proofs are complete.

Proof Patterns in Cryptography

Cryptographic proofs often follow these patterns:

Reduction proofs

"If adversary A breaks scheme S, then adversary B breaks assumption H." These use intro to assume A exists, then construct B.

Game-hopping

Transform a security game through a sequence of indistinguishable steps. Each hop uses calc or trans to chain inequalities.

Algebraic manipulation

Working in groups or rings. Use ring tactic for polynomial arithmetic, group for group theory.

Next Steps

You can now follow tactic proofs. Next, learn how to use Mathlib's algebraic structures:

Next: Using Mathlib →