Proof Finding Guide

This document describes certain well-trodden paths for finding proofs. These are just suggestions that might work.

Opening moves

Start a soundness or completeness proof with circuit_proof_start.
The simpset circuit_norm is supposed to bring the goal state to well-trodden forms: simp only [circuit_norm].
Often, custom definitions like MySubgadget.circuit need to be unfolded. You can do so by passing them along in the simp set: circuit_proof_start [MySubgadget.circuit] or simp only [circuit_norm, MySubgadget.circuit].
In many cases, it's needed to keep unfolding things so that only the math content remains.

The most usual moves are just simp only [...].
Most Clean definitions are meant to be unfolded away.
- Clean's subcircuit mechanism prevents you from seeing the internal operations of subcircuits, so it's usually fine to unfold everything that you don't know about.
- Exceptionally, it's usually better not to unfold loop constructions like Circuit.foldl. Use simp only [circuit_norm] to transform them into plain statements like ∀ i < m, .... To deal with the result, it can be beneficial to state a separate lemma for lifting properties to the loop, using induction.
When a context has an assumption h : something → something, probably it's helpful to specialize h (by ...).
If math is involved, you use lemmas from Mathlib or Utils. The goal state in Clean is usually too large for rw? (and also usually for apply?), so Loogle is your friend.

Once there is nothing about Clean and the goal is just about math, the proof branch is about to be closed.

When simp_all, aesop or grind quickly solves a goal, that proof is very maintainable.
When it's about natural numbers, addition, equality and less-than, omega or linarith might be useful.
When it's about 1 + 1 and 2 (as field elements), or distributing multiplication over addition, try ring_nf or field_simp.