STYLE.txt

		     CONVENTIONS AND STYLE GUIDE
		    =============================

1. ORGANIZATION

The Coq files of the HoTT library live in the theories/ directory.
They are currently in several groups:

- Overture, PathGroupoids, Equivalences, Contractible

  These files contain basic definitions that underlie everything else

- types/*

  This subdirectory contains a file corresponding to each basic type
  former, which proves the "computational" rules for the path-types,
  transport, functorial action, etc. of that type former.

- HLevel, HProp, HSet

  Files about hlevels, which currently use some results from the
  types/ directory.

- HoTT

  This file imports and exports everything.  Thus, in a development
  based on the HoTT library, you can say simply "Require Import HoTT"
  to pull in everything.


2. NAMING CONVENTIONS

See the introduction to PathGroupoids.v.
[Should we move it to here?]

In general, the name of a theorem (or definition, or instance, etc.)
should begin with the property (or structure, or class, or record,
etc.) being proven, and then state the object or construction it is
being proven about.  For instance, "isequiv_idmap" proves "IsEquiv
idmap", and "equiv_compose" constructs an "Equiv" record by composing
two given equivalences.


3. RECORDS, STRUCTURES, TYPECLASSES

We use Coq Records when appropriate for important definitions.  For
instance, contractibility and equivalences are both Record types.  The
file types/Record.v contains some tactics for proving
semiautomatically that record types are equivalent to the
corresponding Sigma-types, so that the relevant general theorems can
be applied to them.

We are using typeclasses in preference to canonical structures.
Typeclasses are particularly convenient for h-properties of objects.
Here are some of the typeclasses we are using:

- equivalences: IsEquiv
- hlevels: Contr, HLevel
- axioms (see below): Funext, Univalence

HProp and HSet are notations for "HLevel -1" and "HLevel 0",
respectively, while "HLevel -2" reduces to "Contr".

When constructing terms in a typeclass record such as IsEquiv, Contr,
or HLevel, one has the choice to declare it as an "Instance", in which
case it is added to the hint database that is searched when Coq tries
to do typeclass instance resolution.  Care must be taken with this, as
indiscriminately adding theorems to this database can easily result in
infinite loops (or at least very long loops).

In general, it seems to be better not to add Instances which suggest
an open-ended search.  E.g. the theorem that h-levels are closed under
equivalence is a bad candidate for an Instance, because when Coq is
searching for a proof of "Contr B" this theorem could cause it to look
through all possible types A for an equivalence "A <~> B" and a proof
of "Contr A".  Results of this sort should be proven as "Definition"s
or "Theorems", not as "Instances".  If you need to use a result of
this sort in the middle of a proof, use a tactic like "pose" or
"assert" to add a particular instance of its conclusion to the
context; then it will be found by subsequent typeclass resolution.

If you have determined through trial and error that a particular
result should not be an Instance (e.g. when making it an Instance, a
tactic in some other proof loops, but changing it to a Definition
prevents this), please add a comment to that effect where it is
defined.  This way no one else will come along and helpfully change it
back to an Instance.

Try to avoid ever giving a name to variables inhabiting typeclasses.
When introducing such a variable, you can write "intros ?" to put it
in the hypotheses without specifying a name for it.  When using such a
variable, typeclass resolution means you shouldn't eve need to refer
to it by name: you can write "_" in tactics such as "refine" and Coq
will find typeclass instances from the context.  Even "exact _" works.

Unfortunately, it is not currently possible to write "_" in a
"refine"d term for an inhabitant of a typeclass and have Coq generate
a subgoal if it can't find an instance; Coq will die if it can't
resolve a typeclass variable from the context.  You have to "assert"
or "pose" such an inhabitant first, or give an explicit term for it.


4. AXIOMS

The "axioms" of Univalence and Funext (function extensionality) are
also typeclasses rather than Coq Axioms.  This means that any theorem
which depends on one or the other must technically take an argument of
the appropriate type.  It is simple to write this using typeclass
magic as follows:

Theorem uses_univalence `{Univalence} (A : Type) ...

The axiom-term witnessing univalence does not have to be named, nor
does it have to be passed explicitly to any other lemma which uses
univalence; once it is in the typeclass context, it should be found
automatically.

For longer developments using Univalence or Funext, it is probably
preferable to assume it as part of the context.

Section UsesUnivalence.
Context `{Univalence}.

Now everything defined and proven in this section can use univalence
without saying so explicitly, and at the end of the section it will be
implicitly generalized if necessary.  The backquote syntax
`{Univalence} allows us to avoid giving a name to the hypothesis.
(Backquote syntax is also used for implicit generalization of
variables, but that is not needed for univalence and funext.)


5. TRANSPARENCY AND OPACITY

If the value of something being defined matters, then you must either
give an explicit term defining it, or construct it with tactics and
end the proof with "Defined.".  But if all that matters is that you
have defined something with a given type, you can construct it with
tactics and end the proof with "Qed.".  The latter makes the term
"opaque" so that it doesn't "compute".

If something *can* be made opaque, it is generally preferable to do
so, for performance reasons.  However, many things which a traditional
type theorist would make opaque cannot be opaque in homotopy type
theory.  For instance, none of the higher-groupoid structure in
PathGroupoids can be made opaque, not even the "coherence laws".  If
you doubt this, try making some of it opaque and you will find that
the "higher coherences" such as "pentagon" and "eckmann_hilton" will
fail to typecheck.

In general, it is okay to contruct something transparent using
tactics; it's often a matter of aesthetics whether an explicit proof
term or a tactic proof is more readable or elegant, and personal
aesthetics may differ.  Consider, for example, the explicit proof term
given for "eckmann_hilton": some may consider it optimally elegant,
while others would prefer to be able to step through a tactic proof to
understand what is happening step-by-step.

The important thing is that when defining a transparent term with
tactics, you should restrict yourself to tactics which maintain a high
degree of control over the resulting term; "blast" tactics like
"autorewrite" should be eschewed.  Even plain "rewrite" is usually to
be avoided in this context: although the terms it produces are at
least predictable, they are one big "transport" (under a different
name) whereas a term we would want to reason about ought to be
constructed using smaller pieces like "ap" and "concat" which we can
understand.

Here are some acceptable tactics to use in transparent definitions
(this is probably not an exhaustive list):

- intros, revert, generalize
- pose, assert, set, cut
- fold, unfold, simpl, hnf
- case, elim, destruct, induction
- apply, eapply, assumption, eassumption, refine, exact
- reflexivity

Conversely, if you want to use "rewrite", that is fine, but you should
then make the thing you are defining opaque.  If it turns out later
that you need it to be transparent, then you should go back and prove
it without using "rewrite".

Currently, there are some basic facts in the library, such as the
"adjointify" lemma, which are proven using "rewrite" and hence are at
least partially opaque.  It might be desirable one day to prove these
more explicitly and make them transparent, but so far it has not been
necessary.

Note that it *is* acceptable for the definition of a transparent
theorem to invoke other theorems which are opaque.  For instance,
the "adjointify" lemma itself is actually transparent, but it invokes
an opaque sublemma that computes the triangle identity (using
"rewrite").  Making the main lemma transparent is necessary so that
the other parts of an equivalence -- the inverse function and
homotopies -- will compute.  Thus, a transparent definition will not
generally be "completely transparent".

It is possible to make subterms of a term opaque by using the abstract
tactic. The assert tactic also produces opaque subterms. For a 
transparent subterm use refine.

6. FORMATTING

All "Require" commands should be placed at the top of a file.  They
should generally be followed by all "[Local] Open Scope" commands, and
then by "Generalizable Variables" commands.  The latter two might
also occur in Sections later on in the file, but in that case they
should usually come at the beginning of the Section.

Lines of code should be of limited width; try to restrict yourself to
not much more than 70 characters.  Remember that when Coq code is
often edited in split-screen so that the screen width is cut in half,
and that not everyone's screen is as wide as yours.

Text in comments, on the other hand, should not contain hard newlines.
If editing in Emacs, turn off auto-fill-mode and turn on visual-line
mode; then you'll be able to read comment paragraphs without scrolling
horizontally, no matter how narrow your window is.  Putting hard
newlines in text makes it extremely ugly when viewed in a window that
is more narrow than the width to which you filled it.

Unfortunately, when viewing source code on Github, these long comment
lines are not wrapped, making them hard to read.  If you use the
Stylish plugin, you can make them wrap by adding the following style:
    @-moz-document domain(github.com) {
        div.line {
            white-space: pre-wrap;
        }
    }
This messes up the line-numbering, though, you'll have to turn it
off in order to link to or comment on a particular line.

When writing tactic scripts, use newlines as a "logical grouping"
construct.  Important tactic invocations, such as a top-level
"induction" which create a branch point in the proof, should generally
be on lines by themselves.  Other lines can contain several short
tactic commands (separated by either periods or semicolons), if they
together implement a single idea or finish off a subgoal.

For long proofs with multiple significant subgoals, use branching
constructs to clarify the structure.  [Insert more instructions here.]

[The following formatting guidelines are a tentative suggestion.]

If the entire type of a theorem or definition does not fit on one
line, then it is better to put the result type (the part after the
colon) on an indented line by itself, together with the colon to make
it clear that this is the result type.

Definition triangulator {A : Type} {x y z : A} (p : x = y) (q : y = z)
  : concat_p_pp p 1 q @ whiskerR (concat_p1 p) q.

Of course, if the list of input types does not fit on a line by
itself, it should be broken across lines as well, with later lines
indented, and similarly for the result type.

Definition pentagon {A : Type} {v w x y z : A}
  (p : v = w) (q : w = x) (r : x = y) (s : y = z)
  : whiskerL p (concat_p_pp q r s)
      @ concat_p_pp p (q@r) s
      @ whiskerR (concat_p_pp p q r) s.

For definitions given with an explicit term, that term should usually
also be on an indented line by itself, together with the := to make it
clear that this is the definition.

Definition concat_p1 {A : Type} {x y : A} (p : x = y) : p @ 1 = p
  := match p with idpath => 1 end.

Of course, if the term is longer than one line, it should be broken
across lines, with later lines indented further.