Style Guide

Tabs

• Size: 2.
• Spaces.

Spacing

One blank line between two separate things. This does not include comments for title of functions or function steps.

Import and Scopes - Ordering

1. Imports from Stdlib.
2. Imports from Temporal - Sections should be ordered by number.
3. Open scopes - Z should be final scope.

Comments

All functions referring to the Temporal Proposal should have a comment like this:

(* 1.1.1 SomeFunction *)
Definition SomeFunction ...

The function steps of mechanized functions should be commented like this (as far as possible):

(*>> 1. Let x be 2 <<*)
let x := 2 in
(*>> 2. Let y be 7 <<*)
let y := 2 in
(*>> 3. Return x + y <<*)
x + y.

Definitions and proofs

"Helper" statements should use the Lemma keyword, while statements that stand on their own use Theorem. Lemmas or theorems always start with Proof., and the proof is indented.

Obligations omit the Proof.. If an obligation can be proved with only a few tactics, it may be defined on a single line.

Prefer Definition, then Program Definition, then Definition with a tactic body:

(* best: *)
Definition five : {n : nat | n = 5} := exist _ 5 eq_refl.

(* good: *)
Program Definition five : {n : nat | n = 5} := 5.
Next Obligation. reflexivity. Qed.

(* in an emergency: *)
Definition five : {n : nat | n = 5}.
  exists 5.
  reflexivity.
Defined.

Naming Theorems

Theorems should start with the function name, then an underscore, followed by a description like this:

Theorem IsValidNumber_is_always_valid ...

Tactics

Use a space between the arrow and the name to rewrite with:

rewrite <- Z.gtb_ltb.