From 57d111b4ca270de0b841dd95bb208133f1232e49 Mon Sep 17 00:00:00 2001
From: Sergei Bozhko <sbozhko@mpi-sws.org>
Date: Mon, 27 Sep 2021 10:11:25 +0200
Subject: [PATCH] small clean up in util/step_function.v
---
util/step_function.v | 54 ++++++++++++++++++++++----------------------
1 file changed, 27 insertions(+), 27 deletions(-)
diff --git a/util/step_function.v b/util/step_function.v
index bb295c93a..9d02d75a7 100644
--- a/util/step_function.v
+++ b/util/step_function.v
@@ -5,8 +5,8 @@ Section StepFunction.
Section Defs.
- (* We say that a function f... *)
- Variable f: nat -> nat.
+ (* We say that a function [f]... *)
+ Variable f : nat -> nat.
(* ...is a step function iff the following holds. *)
Definition is_step_function :=
@@ -16,25 +16,25 @@ Section StepFunction.
Section Lemmas.
- (* Let f be any step function over natural numbers. *)
- Variable f: nat -> nat.
- Hypothesis H_step_function: is_step_function f.
+ (* Let [f] be any step function over natural numbers. *)
+ Variable f : nat -> nat.
+ Hypothesis H_step_function : is_step_function f.
(* In this section, we prove a result similar to the intermediate
value theorem for continuous functions. *)
Section ExistsIntermediateValue.
(* Consider any interval [x1, x2]. *)
- Variable x1 x2: nat.
- Hypothesis H_is_interval: x1 <= x2.
+ Variable x1 x2 : nat.
+ Hypothesis H_is_interval : x1 <= x2.
- (* Let t be any value such that f x1 < y < f x2. *)
- Variable y: nat.
- Hypothesis H_between: f x1 <= y < f x2.
+ (* Let [t] be any value such that [f x1 <= y < f x2]. *)
+ Variable y : nat.
+ Hypothesis H_between : f x1 <= y < f x2.
- (* Then, we prove that there exists an intermediate point x_mid such that
- f x_mid = y. *)
- Lemma exists_intermediate_point:
+ (* Then, we prove that there exists an intermediate point [x_mid] such that
+ [f x_mid = y]. *)
+ Lemma exists_intermediate_point :
exists x_mid, x1 <= x_mid < x2 /\ f x_mid = y.
Proof.
rename H_is_interval into INT, H_step_function into STEP, H_between into BETWEEN.
@@ -46,11 +46,11 @@ Section StepFunction.
{ move => x2 LE /andP [GEy LTy].
exploit (DELTA (x2 - x1));
first by apply/andP; split; last by rewrite addnBA // addKn.
- by rewrite addnBA // addKn.
+ by rewrite addnBA // addKn.
}
induction delta.
{ rewrite addn0; move => /andP [GE0 LT0].
- by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
+ by apply (leq_ltn_trans GE0) in LT0; rewrite ltnn in LT0.
}
{ move => /andP [GT LT].
specialize (STEP (x1 + delta)); rewrite leq_eqVlt in STEP.
@@ -59,18 +59,18 @@ Section StepFunction.
first by rewrite !addn1 in EQ; rewrite addnS EQ ltnS in LT.
rewrite [X in _ < X]addn1 ltnS in STEP.
apply: (leq_trans _ STEP).
- by rewrite addn1 -addnS ltnW.
+ by rewrite addn1 -addnS ltnW.
} clear STEP LT.
rewrite leq_eqVlt in LE.
move: LE => /orP [/eqP EQy | LT].
{ exists (x1 + delta); split; last by rewrite EQy.
- by apply/andP; split; [by apply leq_addr | by rewrite addnS].
+ by apply/andP; split; [apply leq_addr | rewrite addnS].
}
{ feed (IHdelta); first by apply/andP; split.
move: IHdelta => [x_mid [/andP [GE0 LT0] EQ0]].
exists x_mid; split; last by done.
apply/andP; split; first by done.
- by apply: (leq_trans LT0); rewrite addnS.
+ by apply: (leq_trans LT0); rewrite addnS.
}
}
Qed.
@@ -83,22 +83,22 @@ Section StepFunction.
value theorem, but for predicates of natural numbers. *)
Section ExistsIntermediateValuePredicates.
- (* Let P be any predicate on natural numbers. *)
+ (* Let [P] be any predicate on natural numbers. *)
Variable P : nat -> bool.
(* Consider a time interval [t1,t2] such that ... *)
Variables t1 t2 : nat.
Hypothesis H_t1_le_t2 : t1 <= t2.
- (* ... P doesn't hold for t1 ... *)
+ (* ... [P] doesn't hold for [t1] ... *)
Hypothesis H_not_P_at_t1 : ~~ P t1.
- (* ... but holds for t2. *)
+ (* ... but holds for [t2]. *)
Hypothesis H_P_at_t2 : P t2.
(* Then we prove that within time interval [t1,t2] there exists time
- instant t such that t is the first time instant when P holds. *)
- Lemma exists_first_intermediate_point:
+ instant [t] such that [t] is the first time instant when [P] holds. *)
+ Lemma exists_first_intermediate_point :
exists t, (t1 < t <= t2) /\ (forall x, t1 <= x < t -> ~~ P x) /\ P t.
Proof.
have EX: exists x, P x && (t1 < x <= t2).
@@ -106,7 +106,7 @@ Section StepFunction.
apply/andP; split; first by done.
apply/andP; split; last by done.
move: H_t1_le_t2; rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
- by exfalso; subst t2; move: H_not_P_at_t1 => /negP NPt1.
+ by exfalso; subst t2; move: H_not_P_at_t1 => /negP NPt1.
}
have MIN := ex_minnP EX.
move: MIN => [x /andP [Px /andP [LT1 LT2]] MIN]; clear EX.
@@ -116,12 +116,12 @@ Section StepFunction.
{ apply/andP; split; first by done.
apply/andP; split.
- move: NEQ1. rewrite leq_eqVlt; move => /orP [/eqP EQ | NEQ1]; last by done.
- by exfalso; subst y; move: H_not_P_at_t1 => /negP NPt1.
+ by exfalso; subst y; move: H_not_P_at_t1 => /negP NPt1.
- by apply ltnW, leq_trans with x.
}
- by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
+ by move: NEQ2; rewrite ltnNge; move => /negP NEQ2.
Qed.
End ExistsIntermediateValuePredicates.
-End StepFunction.
\ No newline at end of file
+End StepFunction.
--
GitLab