Coq styleguide for the semantics course homework assignments

Styleguide.md

Code Style Guide

Naming conventions

• Prefer snake_case for the names of function arguments, inductive datatypes, definitions, and lemmas.

• Prefer CamelCase for the names of hypothesis, variables inside sections, modules, and sections.

Module Foo.

  Section Bar.

    Variable Hb : bool.

    Definition lt_zero x := x < 0.

    Inductive tri_bool := 
    | tri_true
    | tri_false
    | tri_unknown

    Lemma lt_zero_lt_one x (HLtZ : lt_zero x) : 
      x < 1.
    Proof. admit. Admitted.

  End Bar.

End Foo. 
  

Indentation

• Use two spaces to indent a new block (do not use tabs).

• Always indent a content of the Module and Section (see example above).

• Start a proof on a new line and indent a content of the Proof block, except when the proof is short and can fit into one line.

(* one line proof *)
Lemma lt_zero_lt_one x (HLtZ : x < 0) : 
  x < 1.
Proof. omega. Qed.

(* multi line proof *)
Lemma le_or_gt_zero x : 
  {x <= 0} + {x > 0}.
Proof. 
  tac1.
  tac2.
  tac3.
Qed.

• When defining a lemma, always put the conclusion of the lemma into new line and indent it.

• Always put regular arguments of the lemmas first, before the hypothesis.

• When hypothesis of the lemma do not fit into one line, put them to the next lines and ensure that assumptions have more indentation than the conclusion.

Lemma not_le_and_gt_zero x 
      (HLeZ : x <= 0)
      (HGtZ : x > 0) : 
  False.
Proof. omega. Qed.

Spaces

• Binary operators should be surrounded by spaces: t : T, a := 2 + 2, A -> B etc.

• The ; tactical should not be separated from the preceding tactic: apply Hx; auto.

• When using goal selectors, do not separate goal numbers by spaces and do not put spaces before :.

apply Hx.
1,2,3: omega.
all: congruence.

• When using destruct, induction or inversion separate conjuncts by single space. Also surround disjuncts separator | by spaces. But do not put spaces after opening bracket [ or before closing bracket ].

destruct HAnd as [HA HB].

destruct HOr as [HA | HB].

destruct HExist as [x [HA HB]].

destruct HOption as [|HH].

• Same rules apply when using [|] to handle subgoals by different tactics.

apply Hx; [apply Hy | apply Hz].

apply Hx; [apply Hy |].

Goal bookkeeping

• Use curly brackets {} instead of bullets +, -, *, etc in order to focus on the subgoal.

• Put a space after opening bracket { and before closing bracket }.

• When selecting a subgoal with brackets always start the subgoal's proof on a new line and use indentation.

• Do not leave opening { or closing bracket } alone on a line.

• Do not focus the last subgoal (rule of thumb: there're no two } on the line and there's no } preceding Qed.).

apply Hx.
{ omega. }
{ apply Ha.
  apply Hb. }
apply Hy.

• When introducing a new subgoal via assert always give an explicit name to the hypothesis (same applies to pose proof and similar tactics). When using assert put the name before the hypothesis and do not use as ... syntax.

assert (Hx : x < 0).

• Avoid references to the autogenerated names like H0 when possible.