Lesson 6: Summary

• have, suff, wlog proof cuts, alternative to intermediate lemmas.
• set and pose abstracting sub terms,
• -[pattern]/expression substitutes an expression for a convertible one,
• Good practices for real proofs.

have: and suff:

• have i_items : statement. asks you to prove statement first.
• suff i_items : statement. asks you to prove statement first.
• have i_items := term. genralizes term and puts in on the top of the stack.

This last one is very useful as an alternative of Check, since you can play with the result which is on the top of the stack.

cf ssreflect documentation on rewrite

Example: Infinitude of primes

Teaser: Order and max, a matter of symmetry

Note the repetition, and the step dealing with symmetry.

Without loss of generality

• wlog i_items : generalizations / H in a goal G, lets you prove that
  • (H -> G) -> G as first goal
  • H -> G as a second goal.
• its typical use is for breaking the symmetry.

-[pattern]/term lets you replace a term by a convertible one.

e.g.

• -[2]/(1 + 1) replaces 2 by 1 + 1,
• -[2 ^ 2]/4 replaces 2 ^ 2 by 4,
• -[m]/(0 * d + m) replaces m by 0 * d + m.

Example: Euclidean division, simple and correct

set and pose naming expressions

• pose name := pattern, generalizes every hole in the pattern, and puts a definition name in the context for it. It does NOT change the conclusion.
• set name := pattern, finds the pattern in the conclusion, and puts a definition name in the context. Finally, it substitutes the pattern for name in the conclution.

Good practices for real proofs.

• Never unfold a definition from a library, unless you really mean it. (Unfolding will happen mostly for the symbols YOU defined)
• Take piece of paper and sketch the proof with a pen, do NOT let the proof assitant guide you, only let it assist you.
• Take a look at the header of the library you want to use, to know the concepts.
• Use Search _ symbol1 symbol2 to lookup the lemmas about these concepts.
• Read the name conventions and use them in your own proofs and searches.

A little tour of the div library

If time allows:

• dvdn, modn, divn, m = n %[mod d] ...
• juggling with specificies of division by 2.