diff --git a/util/epsilon.v b/util/epsilon.v
index dae64637cd4cd8a7a326c82609a45586dc7822e6..91d91c9d3aa6f910fcf06ddcde5d6b1389cc5597 100644
--- a/util/epsilon.v
+++ b/util/epsilon.v
@@ -1,6 +1,6 @@
Section Epsilon.
- (* ε is defined as the smallest positive number. *)
+ (* [ε] is defined as the smallest positive number. *)
Definition ε := 1.
End Epsilon.
\ No newline at end of file
diff --git a/util/list.v b/util/list.v
index 4ef25ae293b936d59c7380f65ea9106ac2d711c8..a829ba2e1fdaf6bc103037c68f96b9656c2c12fd 100644
--- a/util/list.v
+++ b/util/list.v
@@ -43,7 +43,7 @@ Section Last0.
Proof. by intros; rewrite nth_last. Qed.
(** We prove that for any non-empty sequence [xs] there is a sequence [xsh]
- such that [xsh ++ [::last0 x] = xs]. *)
+ such that [xsh ++ [::last0 x] = [xs]]. *)
Lemma last0_ex_cat:
forall x xs,
xs <> [::] ->
@@ -81,7 +81,7 @@ End Last0.
(** Additional lemmas about max0. *)
Section Max0.
- (** We prove that max0 (x::xs) is equal to max {x, max0 xs}. *)
+ (** We prove that [max0 (x::xs)] is equal to [max {x, max0 xs}]. *)
Lemma max0_cons: forall x xs, max0 (x :: xs) = maxn x (max0 xs).
Proof.
have L: forall s x xs, foldl maxn s (x::xs) = maxn x (foldl maxn s xs).
@@ -206,9 +206,9 @@ Section Max0.
(** Let's introduce the notion of the nth element of a sequence. *)
Notation "xs [| n |]" := (nth 0 xs n) (at level 30).
- (** If any n'th element of a sequence xs is less-than-or-equal-to
- n'th element of ys, then max of xs is less-than-or-equal-to max
- of ys. *)
+ (** If any element of a sequence [xs] is less-than-or-equal-to
+ the corresponding element of a sequence [ys], then max of
+ [xs] is less-than-or-equal-to max of [ys]. *)
Lemma max_of_dominating_seq:
forall (xs ys : seq nat),
(forall n, xs[|n|] <= ys[|n|]) ->
@@ -254,7 +254,7 @@ End Max0.
(* Additional lemmas about rem for lists. *)
Section RemList.
- (* We prove that if x lies in xs excluding y, then x also lies in xs. *)
+ (* We prove that if [x] lies in [xs] excluding [y], then [x] also lies in [xs]. *)
Lemma rem_in:
forall (T: eqType) (x y: T) (xs: seq T),
x \in rem y xs -> x \in xs.
@@ -272,8 +272,8 @@ Section RemList.
}
Qed.
- (* We prove that if we remove an element x for which P x from
- a filter, then the size of the filter decreases by 1. *)
+ (* We prove that if we remove an element [x] for which [P x] from
+ a filter, then the size of the filter decreases by [1]. *)
Lemma filter_size_rem:
forall (T: eqType) (x:T) (xs: seq T) (P: T -> bool),
(x \in xs) ->
@@ -300,8 +300,7 @@ End RemList.
(* Additional lemmas about sequences. *)
Section AdditionalLemmas.
- (* First, we show that if [n > 0], then [n]'th element of a sequence
- [x::xs] is equal to [n-1]'th element of sequence [xs]. *)
+ (* First, we show that if [n > 0], then [nth (x::xs) n = nth xs (n-1)]. *)
Lemma nth0_cons:
forall x xs n,
n > 0 ->
@@ -332,8 +331,8 @@ Section AdditionalLemmas.
by apply eq_S.
Qed.
- (* Next, we prove that x ∈ xs implies that xs can be split
- into two parts such that xs = xsl ++ [::x] ++ xsr. *)
+ (* Next, we prove that [x ∈ xs] implies that [xs] can be split
+ into two parts such that [xs = xsl ++ [::x] ++ [xsr]]. *)
Lemma in_cat:
forall {X : eqType} (x : X) (xs : list X),
x \in xs -> exists xsl xsr, xs = xsl ++ [::x] ++ xsr.
@@ -347,8 +346,8 @@ Section AdditionalLemmas.
by subst; exists (a::xsl), xsr.
Qed.
- (* We prove that for any two sequences xs and ys the fact that xs is a subsequence
- of ys implies that the size of xs is at most the size of ys. *)
+ (* We prove that for any two sequences [xs] and [ys] the fact that [xs] is a sub-sequence
+ of [ys] implies that the size of [xs] is at most the size of [ys]. *)
Lemma subseq_leq_size:
forall {X : eqType} (xs ys: seq X),
uniq xs ->
@@ -413,7 +412,7 @@ Section AdditionalLemmas.
End AdditionalLemmas.
-(** Function [rem] from ssreflect removes only the first occurrence of
+(** Function [rem] from [ssreflect] removes only the first occurrence of
an element in a sequence. We define function [rem_all] which
removes all occurrences of an element in a sequence. *)
Fixpoint rem_all {X : eqType} (x : X) (xs : seq X) :=
@@ -423,7 +422,7 @@ Fixpoint rem_all {X : eqType} (x : X) (xs : seq X) :=
if a == x then rem_all x xs else a :: rem_all x xs
end.
-(** Additional lemmas about rem_all for lists. *)
+(** Additional lemmas about [rem_all] for lists. *)
Section RemAllList.
(** First we prove that [x ∉ rem_all x xs]. *)
diff --git a/util/nat.v b/util/nat.v
index de8a68a7326c7bfaeb451eaec80d2e78ab1291f5..ae9067692c5201ccd20f768fdb7c4dc785423f00 100644
--- a/util/nat.v
+++ b/util/nat.v
@@ -30,7 +30,7 @@ Section NatLemmas.
- by apply leq_trans with (m+p); first rewrite leq_addl.
Qed.
- (* Simplify n + a - b + b - a = n if n >= b. *)
+ (* Simplify [n + a - b + b - a = n] if [n >= b]. *)
Lemma subn_abba:
forall n a b,
n >= b ->
@@ -97,20 +97,20 @@ End Interval.
Section NatOrderLemmas.
- (* Mimic the way implicit arguments are used in ssreflect. *)
+ (* Mimic the way implicit arguments are used in [ssreflect]. *)
Set Implicit Arguments.
Unset Strict Implicit.
- (* ltn_leq_trans: Establish that m < p if m < n and n <= p, to mirror the
- lemma leq_ltn_trans in ssrnat.
+ (* [ltn_leq_trans]: Establish that [m < p] if [m < n] and [n <= p], to mirror the
+ lemma [leq_ltn_trans] in [ssrnat].
- NB: There is a good reason for this lemma to be "missing" in ssrnat --
- since m < n is defined as m.+1 <= n, ltn_leq_trans is just
- m.+1 <= n -> n <= p -> m.+1 <= p, that is (@leq_trans n m.+1 p).
+ NB: There is a good reason for this lemma to be "missing" in [ssrnat] --
+ since [m < n] is defined as [m.+1 <= n], [ltn_leq_trans] is just
+ [m.+1 <= n -> n <= p -> m.+1 <= p], that is [@leq_trans n m.+1 p].
Nonetheless we introduce it here because an additional (even though
arguably redundant) lemma doesn't hurt, and for newcomers the apparent
- absence of the mirror case of leq_ltn_trans can be somewhat confusing. *)
+ absence of the mirror case of [leq_ltn_trans] can be somewhat confusing. *)
Lemma ltn_leq_trans n m p : m < n -> n <= p -> m < p.
Proof. exact (@leq_trans n m.+1 p). Qed.
diff --git a/util/nondecreasing.v b/util/nondecreasing.v
index ea66693eee5df5ba10d450b1b1167016514a677c..7d4e5803706435ad8e57f7389445a4c5f1c0a4b7 100644
--- a/util/nondecreasing.v
+++ b/util/nondecreasing.v
@@ -13,8 +13,8 @@ Section NondecreasingSequence.
(** In this section we provide the notion of a non-decreasing sequence. *)
Section Definitions.
- (** We say that a sequence xs is non-decincreasing iff for any two indices n1 and n2
- such that [n1 <= n2 < size xs] condition [xs[n1] <= xs[n2]] holds. *)
+ (** We say that a sequence [xs] is non-decreasing iff for any two indices [n1] and [n2]
+ such that [n1 <= n2 < size [xs]] condition [[xs][n1] <= [xs][n2]] holds. *)
Definition nondecreasing_sequence (xs : seq nat) :=
forall n1 n2,
n1 <= n2 < size xs ->
@@ -29,7 +29,7 @@ Section NondecreasingSequence.
(** For a non-decreasing sequence we define the notion of
distances between neighboring elements of the sequence. *)
(** Example:
- Consider the following sequence of natural numbers: xs = [:: 1; 10; 10; 17; 20; 41].
+ Consider the following sequence of natural numbers: [xs] = [:: 1; 10; 10; 17; 20; 41].
Then [drop 1 xs] is equal to [:: 10; 10; 17; 20; 41].
Then [zip xs (drop 1 xs)] is equal to [:: (1,10); (10,10); (10,17); (17,20); (20,41)]
And after the mapping [map (fun '(x1, x2) => x2 - x1)] we end up with [:: 9; 0; 7; 3; 21]. *)
@@ -254,8 +254,8 @@ Section NondecreasingSequence.
Qed.
(** Alternatively, consider an arbitrary natural number x that is
- bounded by the first and the last element of a sequence xs. Then
- there is an index n such that xs[n] <= x < x[n+1]. *)
+ bounded by the first and the last element of a sequence [xs]. Then
+ there is an index n such that [xs[n] <= x < x[n+1]]. *)
Lemma belonging_to_segment_of_seq_is_total:
forall (xs : seq nat) (x : nat),
2 <= size xs ->
@@ -293,7 +293,7 @@ Section NondecreasingSequence.
}
Qed.
- (** Note that the last element of a nondecreasing sequence is the max element. *)
+ (** Note that the last element of a non-decreasing sequence is the max element. *)
Lemma last_is_max_in_nondecreasing_seq:
forall (xs : seq nat) (x : nat),
nondecreasing_sequence xs ->
@@ -324,8 +324,8 @@ Section NondecreasingSequence.
End NonDecreasingSequence.
- (** * Properties of Undup of Non-Decreasing Sequence *)
- (** In this section we prove a few lemmas about undup of non-decreasing sequences. *)
+ (** * Properties of [Undup] of Non-Decreasing Sequence *)
+ (** In this section we prove a few lemmas about [undup] of non-decreasing sequences. *)
Section Undup.
(** First we prove that [undup x::x::xs] is equal to [undup x::xs]. *)
@@ -443,7 +443,7 @@ Section NondecreasingSequence.
(** In this section we prove a few lemmas about function [distances]. *)
Section Distances.
- (** We beging with a simple lemma that helps us unfold [distances]
+ (** We begin with a simple lemma that helps us unfold [distances]
of lists with two consecutive cons [x0::x1::xs]. *)
Lemma distances_unfold_2cons:
forall x0 x1 xs,
@@ -546,8 +546,8 @@ Section NondecreasingSequence.
Qed.
(** Note that the distances-function has the expected behavior indeed. I.e. an element
- on the n-th position of the distance-sequence is equal to the difference between
- n+1-th and n-th elements. *)
+ on the position [n] of the distance-sequence is equal to the difference between
+ elements on positions [n+1] and [n]. *)
Lemma function_of_distances_is_correct:
forall (xs : seq nat) (n : nat),
(distances xs)[|n|] = xs[|n.+1|] - xs[|n|].
@@ -689,9 +689,9 @@ Section NondecreasingSequence.
- eapply L with (indx := indy) (indy := indx) (x := y) (y := x); eauto.
Qed.
- (** Given a nondecreasing sequence xs with length n, we show that the difference
- between the last element of xs and the last element of the distances-sequence
- of xs is equal to the (n-2)'th element of xs. *)
+ (** Given a non-decreasing sequence [xs] with length n, we show that the difference
+ between the last element of [xs] and the last element of the distances-sequence
+ of [xs] is equal to [xs[n-2]]. *)
Lemma last_seq_minus_last_distance_seq:
forall (xs : seq nat),
nondecreasing_sequence xs ->
@@ -718,8 +718,8 @@ Section NondecreasingSequence.
by rewrite addn1.
Qed.
- (** The max element of the distances-sequence of a sequence xs is bounded
- by the last element of xs. Note that all elements of xs are positive.
+ (** The max element of the distances-sequence of a sequence [xs] is bounded
+ by the last element of [xs]. Note that all elements of [xs] are positive.
Thus they all lie within the interval [0, last xs]. *)
Lemma max_distance_in_seq_le_last_element_of_seq:
forall (xs : seq nat),
@@ -765,7 +765,7 @@ Section NondecreasingSequence.
}
Qed.
- (** Let xs be a non-decreasing sequence. We prove that
+ (** Let [xs] be a non-decreasing sequence. We prove that
distances of sequence [[seq Ï <- index_iota 0 k.+1 | Ï \in xs]]
coincide with sequence [[seq x <- distances xs | 0 < x]]]. *)
Lemma distances_iota_filtered:
@@ -810,7 +810,7 @@ Section NondecreasingSequence.
}
Qed.
- (** Let xs again be a non-decreasing sequence. We prove that
+ (** Let [xs] again be a non-decreasing sequence. We prove that
distances of sequence [undup xs] coincide with
sequence of positive distances of [xs]. *)
Lemma distances_positive_undup:
@@ -847,10 +847,10 @@ Section NondecreasingSequence.
Qed.
- (** Consider two nondecreasing sequences xs and ys and assume that
- (1) first element of xs is at most the first element of ys and
- (2) distances-sequences of xs is dominated by distances-sequence of
- ys. Then xs is dominated by ys. *)
+ (** Consider two non-decreasing sequences [xs] and [ys] and assume that
+ (1) first element of [xs] is at most the first element of [ys] and
+ (2) distances-sequences of [xs] is dominated by distances-sequence of
+ [ys]. Then [xs] is dominated by [ys]. *)
Lemma domination_of_distances_implies_domination_of_seq:
forall (xs ys : seq nat),
first0 xs <= first0 ys ->
diff --git a/util/rewrite_facilities.v b/util/rewrite_facilities.v
index eddaa84b44e045d8f41c38d027a8ecd5f164e108..584df5a1f72ba98676128f1f72804505123b38b9 100644
--- a/util/rewrite_facilities.v
+++ b/util/rewrite_facilities.v
@@ -78,27 +78,27 @@ Section RewriteFacilities.
(*
(* Simplifying some relatively sophisticated
expressions can be quite tedious. *)
- Goal f ((a == b) && f false) = f false.
- Proof.
- (* Things like simpl/compute make no sense here. *)
+ [Goal f ((a == b) && f false) = f false.]
+ [Proof.]
+ (* Things like [simpl/compute] make no sense here. *)
(* One can use [replace] to generate a new goal. *)
- replace (a == b) with false; last first.
+ [replace (a == b) with false; last first.]
(* However, this leads to a "loss of focus". Moreover,
the resulting goal is not so trivial to prove. *)
- { apply/eqP; rewrite eq_sym eqbF_neg.
- by apply/eqP; intros EQ; subst b; apply H_npb. }
- by rewrite Bool.andb_false_l.
- Abort.
+ [{ apply/eqP; rewrite eq_sym eqbF_neg.]
+ [ by apply/eqP; intros EQ; subst b; apply H_npb. }]
+ [ by rewrite Bool.andb_false_l.]
+ [Abort.]
*)
(*
(* The second attempt. *)
- Goal f ((a == b) && f false) = f false.
+ [Goal f ((a == b) && f false) = f false.]
(* With the lemmas above one can compose multiple
transformations in a single rewrite. *)
- by rewrite (eqbool_false (neq_sym (neqprop_to_neqbool (diseq _ _ _ H_npb H_pa))))
- Bool.andb_false_l.
- Qed.
+ [ by rewrite (eqbool_false (neq_sym (neqprop_to_neqbool (diseq _ _ _ H_npb H_pa))))]
+ [ Bool.andb_false_l.]
+ [Qed.]
*)
End Example.
diff --git a/util/search_arg.v b/util/search_arg.v
index 555c06df937ef9a46bd3d747e8c0519810d5531b..dc908086f5baeeb49894ae7dd88f901c0983c11c 100644
--- a/util/search_arg.v
+++ b/util/search_arg.v
@@ -1,16 +1,16 @@
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype.
Require Import rt.util.tactics.
-(** This file introduces a function called search_arg that allows finding the
+(** This file introduces a function called [search_arg] that allows finding the
argument within a given range for which a function is minimal w.r.t. to a
given order while satisfying a given predicate, along with lemmas
- establishing the basic properties of search_arg.
+ establishing the basic properties of [search_arg].
Note that while this is quite similar to [arg min ...] / [arg max ...] in
- ssreflect (fintype), this function is subtly different in that it possibly
+ [ssreflect] ([fintype]), this function is subtly different in that it possibly
returns None and that it does not require the last element in the given
- range to satisfy the predicate. In contrast, ssreflect's notion of
- extremum in fintype uses the upper bound of the search space as the
+ range to satisfy the predicate. In contrast, [ssreflect]'s notion of
+ extremum in [fintype] uses the upper bound of the search space as the
default value, which is rather unnatural when searching through a schedule.
*)
@@ -42,7 +42,7 @@ Section ArgSearch.
(** In the following, we establish basic properties of [search_arg]. *)
- (* To begin, we observe that the search yields None iff predicate [P] does
+ (* To begin, we observe that the search yields [None] iff predicate [P] does
not hold for any of the points in the search interval. *)
Lemma search_arg_none:
forall a b,
@@ -151,7 +151,7 @@ Section ArgSearch.
Hypothesis R_total: total R.
(* ...then [search_arg] yields an extremum w.r.t. to [a, b), that is, if
- [search_arg] yields a point x, then [R (f x) (f y)] holds for any y in the
+ [search_arg] yields a point x, then [R (f x) (f y)] holds for any [y] in the
search range [a, b) that satisfies [P]. *)
Lemma search_arg_extremum:
forall a b x,
diff --git a/util/seqset.v b/util/seqset.v
index 554e3c90de481e27e4c3569082ce777fa19927a4..4b47f7e548b807ff0835f24d68c4f0b4f58f56a3 100644
--- a/util/seqset.v
+++ b/util/seqset.v
@@ -12,7 +12,7 @@ Section SeqSet.
_ : uniq _set_seq (* no duplicates *)
}.
- (* Now we add the ssreflect boilerplate code. *)
+ (* Now we add the [ssreflect] boilerplate code. *)
Canonical Structure setSubType := [subType for _set_seq].
Definition set_eqMixin := [eqMixin of set by <:].
Canonical Structure set_eqType := EqType set set_eqMixin.
diff --git a/util/sum.v b/util/sum.v
index b8fa33b1e253d0e8f6a32f65f00c6ef840756329..424376b38c7b7e102e55ccce7fbfb4c0d8326f09 100644
--- a/util/sum.v
+++ b/util/sum.v
@@ -107,7 +107,7 @@ Section ExtraLemmas.
by apply sum0.
Qed.
- (* We prove that if any element of a set r is bounded by constant const,
+ (* We prove that if any element of a set r is bounded by constant [const],
then the sum of the whole set is bounded by [const * size r]. *)
Lemma sum_majorant_constant:
forall (T: eqType) (r: seq T) (P: pred T) F const,
@@ -138,10 +138,10 @@ Section ExtraLemmas.
}
Qed.
- (* We prove that if for any element x of a set xs the following two statements hold
+ (* We prove that if for any element x of a set [xs] the following two statements hold
(1) [F1 x] is less than or equal to [F2 x] and (2) the sum [F1 x_1, ..., F1 x_n]
is equal to the sum of [F2 x_1, ..., F2 x_n], then [F1 x] is equal to [F2 x] for
- any element x of xs. *)
+ any element x of [xs]. *)
Lemma sum_majorant_eqn:
forall (T: eqType) xs F1 F2 (P: pred T),
(forall x, x \in xs -> P x -> F1 x <= F2 x) ->
diff --git a/util/tactics.v b/util/tactics.v
index 2cc3189a1aa87f9fa8a053f0be3eb706d9224e0d..808d2c9440fae943ebe841651325781844c7f91b 100644
--- a/util/tactics.v
+++ b/util/tactics.v
@@ -1,6 +1,6 @@
From mathcomp Require Import ssreflect ssrbool ssrnat eqtype bigop.
-(** Lemmas & tactics adopted (with permission) from V. Vafeiadis' Vbase.v. *)
+(** Lemmas & tactics adopted (with permission) from [V. Vafeiadis' Vbase.v]. *)
Lemma neqP: forall (T: eqType) (x y: T), reflect (x <> y) (x != y).
Proof. intros; case eqP; constructor; auto. Qed.
@@ -11,7 +11,7 @@ Ltac ins := simpl in *; try done; intros.
(** ** Exploiting a hypothesis *)
(* ************************************************************************** *)
-(** Exploit an assumption (adapted from CompCert). *)
+(** Exploit an assumption (adapted from [CompCert]). *)
Ltac exploit x :=
refine ((fun x y => y x) (x _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _) _)