Improve the formatting of the generated docs

src/Beta.v

@@ -30,6 +30,7 @@ Example inner_bred :
 Proof. apply bred_appl. apply bred_lam. apply bred_base. Qed.
 
 (** [bred] is closed under applications of [lift] **)
+
 Lemma bred_lift_closed:
   forall M N, forall b k,
     bred M N -> bred (lift k b M) (lift k b N).
@@ -129,6 +130,7 @@ Proof.
 Qed.
 
 (** [bstar] is closed under the basic beta reduction **)
+
 Lemma bstar_bred_closed:
   forall M M' N,
          bstar M M' -> bstar (App (Lam M) N) (subst 0 N M').
@@ -164,6 +166,7 @@ Qed.
 
 (** [bstar] is closed under variable substitution, like all compatible
     relations **)
+
 Lemma bstar_weak_subst:
   forall M, forall k, forall N N',
     bstar N N' -> bstar (subst k N M) (subst k N' M).
@@ -188,6 +191,7 @@ Qed.
 
 (** The is the most useful statement: [bstar] is also substitutive, giving
     complete (parallel) closure under [subst] **)
+
 Lemma bstar_subst_closed:
   forall M M' N N',
    bstar M M' -> bstar N N' -> bstar (App (Lam M) N) (subst 0 N' M').
@@ -200,6 +204,7 @@ Qed.
 
 
 (** * Parallel [beta] reduction *)
+
 Inductive beta_par : lterm -> lterm -> Prop :=
   | beta_par_var: forall n,
         beta_par (Var n) (Var n)
@@ -215,6 +220,7 @@ Inductive beta_par : lterm -> lterm -> Prop :=
 (** Again, we prove a couple of useful results about [beta_par] **)
 
 (** Parallel beta reduction is reflexive on all [lterm]'s **)
+
 Lemma beta_par_refl:
   forall t, beta_par t t.
 Proof.
@@ -228,6 +234,7 @@ Proof.
 Qed.
 
 (** Parallel beta subsumes [bred] **)
+
 Lemma bred_imp_beta_par:
   forall M N,
     bred M N -> beta_par M N.
@@ -238,6 +245,7 @@ Proof.
 Qed.
 
 (** [beta_par] implies [bstar] **)
+
 Lemma beta_par_imp_bstar:
   forall M N,
     beta_par M N -> bstar M N.
@@ -251,6 +259,7 @@ Proof.
 Qed.
 
 (** [beta_par] is closed under [shift k] **)
+
 Lemma beta_par_shift:
   forall k, forall M M', beta_par M M' -> beta_par (shift k M) (shift k M').
 Proof.
@@ -275,6 +284,7 @@ Proof.
 Qed.
 
 (** Transitive closure of [beta_par] **)
+
 Definition beta_par_trans := clos_trans lterm beta_par.
 
 (** We now show the equivalence between [bstar] and the transitive closure of

src/Eta.v

@@ -14,22 +14,25 @@ Module Export Eta.
 (** We define [eta] conversion as the compatible closure of the [eta_base]
     relation. In literature eta-conversion is usually specified as:
 
-        [[λx. (f x) ~> f]], if [[x]] is not free in [[f]]
+        [λx. (f x) -> f], if [x] is not free in [f]
 
     Using de Bruijn indices this corresponds to ensuring that
-    [[f]] contains no references to the variable with index [0] (or any of it's
+    [f] contains no references to the variable with index [0] (or any of it's
     lifted occurrences), which can be expressed by the condition
+
         [f = shift 0 g]
-    Ensuring that *all* variables in [[g]] are of higher binding level.
+
+    ensuring that _all_ variables in [g] are of higher binding level.
 
     Moreover, after the eta-conversion we have lost one λ binder,
-    hence we "un-shift" [[f]] to [[g]].
+    hence we "un-shift" [f] to [g].
 **)
 
 Inductive eta_prim : lterm -> lterm -> Prop :=
    eta_base (f g: lterm): (f = shift 0 g) -> eta_prim (Lam (App f (Var 0))) g.
 
 (** We defined [eta] as the compatible closure of the primitive relation. **)
+
 Definition eta := clos_compat eta_prim.
 
 (** A couple of examples to make sure our definition works with at least
@@ -53,7 +56,9 @@ Qed.
 
 (** We prove a couple of substitution lemmas regarding [eta]. **)
 
-(** [eta_prim] is substitutive (as per Barendregt's definition) **)
+(** [eta_prim] is substitutive (as per Barendregt's definition)
+**)
+
 Lemma eta_prim_substitutive:
   forall (M N L: lterm) (n: nat),
     eta_prim M N -> eta_prim (subst n L M) (subst n L N).
@@ -181,6 +186,7 @@ Proof.
 Qed.
 
 (** Additionally, [eta_star] is closed under lifting **)
+
 Lemma eta_star_lift_closed:
   forall M N, forall k b,
     eta_star M N -> eta_star (lift k b M) (lift k b N).
@@ -240,6 +246,7 @@ Inductive eta_par : lterm -> lterm -> Prop :=
 (** Some general properties about [eta_par] **)
 
 (** Parallel eta is reflexive on all [lterm]s **)
+
 Lemma eta_par_refl:
   forall t, eta_par t t.
 Proof.
@@ -252,6 +259,7 @@ Proof.
 Qed.
 
 (** Parallel eta is closed under lifting **)
+
 Lemma eta_par_lift_closed:
   forall M N, forall k b,
     eta_par M N -> eta_par (lift k b M) (lift k b N).
@@ -276,6 +284,7 @@ Proof.
 Qed.
 
 (** [eta_par] is substitutive **)
+
 Lemma eta_par_substitutive:
   forall (M N L: lterm) (n: nat),
   eta_par M N -> eta_par (subst n L M) (subst n L N).
@@ -294,6 +303,7 @@ Proof.
 Qed.
 
 (** [eta_par] is fully closed under parallel substitution **)
+
 Lemma eta_par_subst_closed:
   forall (M M' N N': lterm), forall n,
     eta_par M M' -> eta_par N N' -> eta_par (subst n N M) (subst n N' M').
@@ -323,6 +333,7 @@ Qed.
 (** We now describe the relationships between [eta], [eta_par] and [eta_star] **)
 
 (** [eta] implies [eta_par] **)
+
 Lemma eta_imp_eta_par:
   forall M N, eta M N -> eta_par M N.
 Proof.
@@ -336,6 +347,7 @@ Proof.
 Qed.
 
 (** [eta_par] implies [eta_star] **)
+
 Lemma eta_par_imp_eta_star:
   forall M N,
     eta_par M N -> eta_star M N.
@@ -349,10 +361,12 @@ Proof.
 Qed.
 
 (** The transitive closure of [eta_par] **)
+
 Definition eta_par_trans := clos_trans lterm eta_par.
 
 (** Finally, we show that [eta_star] is equivalent to the transitive closure of
     [eta_par] **)
+
 Lemma eta_star_eq_closure_of_eta_par:
   forall M N,
     eta_star M N <-> eta_par_trans M N.
@@ -375,6 +389,7 @@ Qed.
 
 (** We now define a function for expressing a [k]-fold [eta] expansion of
     an [lterm]. **)
+
 Fixpoint lam_k (k: nat) (M: lterm) : lterm :=
   match k with
     | 0 => M
@@ -403,13 +418,15 @@ Proof.
 Qed.
 
 (** A trivial fact **)
+
 Example lam_k_zero:
   forall M, lam_k 0 M = M.
 Proof.
   auto.
 Qed.
 
 (** This commutativity lemma which will be useful later. **)
+
 Lemma shift_0_lam_commute:
     forall n, forall t,
       shift 0 (lam_k n t) = (lam_k n (shift 0 t)).
@@ -426,8 +443,8 @@ Proof.
 Qed.
 
 
-(** We now prove some basic properties about the relationship between [[eta]]
-    and [[lam_k]]. (This is Lemma 3.2 in the Takahashi paper.) **)
+(** We now prove some basic properties about the relationship between [eta]
+    and [lam_k]. (This is Lemma 3.2 in the Takahashi paper.) **)
 
 (* Lemma 3.2 (1) *)
 Lemma eta_par_lam_k_var:

src/Postpone.v

@@ -64,6 +64,7 @@ Qed.
 
 (** Similarly, a [k]-fold eta-expansion of a lambda abstraction can be reduced
     to a single lambda abstraction via parallel beta reduction. **)
+
 Lemma lam_k_beta_lam:
   forall k, forall M M',
     beta_par M M' -> beta_par (lam_k k (Lam M)) (Lam M').
@@ -87,6 +88,7 @@ Qed.
 
 (** In case of an application, we can also contract the whole eta-expansion of
     the applied term via parallel beta reduction *)
+
 Lemma lam_k_beta_app:
   forall k, forall M M' N N',
     beta_par M M' -> beta_par N N' ->
@@ -132,6 +134,7 @@ Qed.
 **)
 
 (** Parallel beta is closed under eta-expansion. **)
+
 Lemma beta_par_lam_k_closed:
   forall k, forall M N,
     beta_par M N -> beta_par (lam_k k M) (lam_k k N).
@@ -146,6 +149,7 @@ Qed.
 
 (** We can now prove the postponement theorem for the specific case of parallel
     reductions. This is Lemma 3.4 in Takahashi. **)
+
 Lemma postpone_par:
   forall M P N,
     eta_par M P -> beta_par P N ->
@@ -224,6 +228,7 @@ Qed.
 
 (** We now define the beta-eta relation and its reflexive-transitive closure
 **)
+
 Definition beta_eta := union lterm bred eta.
 Definition beta_eta_star := clos_refl_trans lterm beta_eta.
 
@@ -239,6 +244,7 @@ Definition beta_eta_star := clos_refl_trans lterm beta_eta.
 (** Firstly, since the reflexive-transitive closures are equivalent
     to the transitive closures of the parallel relations, the following holds:
 **)
+
 Lemma star_exists_iff_par_exists:
   forall M N,
   (exists P, bstar M P /\ eta_star P N) <->
@@ -255,6 +261,7 @@ Qed.
 
 (** Also, it is obviously sufficient to show this to hold for parallel beta,
     in order for it to also hold for the transitive closure: *)
+
 Lemma par_impl_par_trans:
   forall M N,
     (exists P, beta_par M P /\ eta_par P N) ->
@@ -267,6 +274,7 @@ Qed.
 
 (** Finally, a couple of "one-sided" rewrites for convenience within the proof.
 **)
+
 Lemma rewrite_existential_eta:
   forall M N,
   (exists P, beta_par M P /\ eta_star P N) <->
@@ -300,6 +308,7 @@ Qed.
 
 (** Here we consider the case where we postpone [eta_star] in the presence
     of only a parallel beta. **)
+
 Lemma eta_baby_postpone_eta:
   forall M P N,
     eta_star M P -> beta_par P N ->
@@ -333,6 +342,7 @@ Qed.
 
 (** Similarly, here we consider only the postponement of [eta_par] in the
     presence [bstar]: **)
+
 Lemma eta_baby_postpone_beta:
   forall M P N,
     eta_par M P -> bstar P N ->
@@ -366,6 +376,7 @@ Qed.
 (** We now combine all the previous lemmas to prove a simplified version of the
     eta-postponement where we consider separate [eta_star] and [bstar] reductions,
     rather than a single reduction of their union. **)
+
 Theorem eta_postponement_basic:
   forall M N P,
     eta_star M P -> bstar P N -> (exists P', bstar M P' /\ eta_star P' N).
@@ -410,6 +421,7 @@ Qed.
 (** Finally, we prove the full eta-postponement theorem using the
     separate reduction version in [eta_postponement_basic].
 **)
+
 Theorem eta_postponement:
   forall M N,
     beta_eta_star M N -> (exists P, bstar M P /\ eta_star P N).

src/Subst.v

@@ -5,6 +5,7 @@ Require Import Coq.Arith.Plus.
 Require Import Coq.Arith.Lt.
 
 (** (l)ift (t)erms by some (l)evel if greater or equal the (b)ound **)
+
 Fixpoint lift (l: nat) (b: nat) (t: lterm) : lterm :=
   match t with
       | Var i as v =>  if (lt_dec i b) then v else Var (i+l)
@@ -15,7 +16,8 @@ Fixpoint lift (l: nat) (b: nat) (t: lterm) : lterm :=
 Definition shift (b: nat) (t: lterm) : lterm :=
   lift 1 b t.
 
-(** Substitute the variable with index [[v]] by [[r]] in the term [[t]] **)
+(** Substitute the variable with index [v] by [r] in the term [t] **)
+
 Fixpoint subst (v: nat) (r: lterm) (t: lterm) : lterm :=
   match t with
       | Var i =>  match (nat_compare i v) with
@@ -217,9 +219,10 @@ Qed.
 (** The substitution lemma.
     The named version looks like this:
 
-       [[x =/= y]] and [[x]] not free in [[L]] implies:
-           [M[x/N][y/L] = M[y/L][x/(N[y/L])]]
+       [x =/= y] and [x] not free in [L] implies:
+           [M[x/N][y/L] = M[y/L][x/(N[y/L])]
 **)
+
 Lemma subst_lemma: forall (M N L: lterm), forall (i j: nat),
    (i <= j) ->
        subst j L (subst i N M) = subst i (subst (j-i) L N) (subst (j+1) L M).
@@ -237,6 +240,7 @@ Qed.
 
 (** Attempting to substitute a variable with index [k] in a term which is
     already shifted by [k] simply un-shifts the term: **)
+
 Lemma subst_shift_ident:
     forall t, forall k v,
     subst k v (shift k t) =  t.
@@ -260,6 +264,7 @@ Qed.
 
 (** Similarly, if the variable we're substituting in is [Var 0], then
     it gets unshifted even more: **)
+
 Lemma subst_k_shift_S_k:
     forall t, forall k,
     subst k (Var 0) (shift (S k) t) = t.
@@ -310,6 +315,7 @@ Qed.
 
 (** Given compatible bounds, a sequence of [lift]s commutes in a very specific
     way: **)
+
 Lemma lift_lift:
     forall M, forall b1 b2 k1 k2,
       b1 <= b2 ->
@@ -353,6 +359,7 @@ Proof.
 Qed.
 
 (** This is a reverse statement of [lift_lift]: **)
+
 Lemma lift_lift_rev:
   forall wk k ws s t,
   k >= s + ws ->
@@ -366,6 +373,7 @@ Proof.
 Qed.
 
 (** [lift] distributes over [subst], also in a specific way: **)
+
 Lemma lift_distr_subst:
   forall M N, forall v, forall i b,
     v <= b ->