From 93b40629e4e1775652fc5ee21e05f03fed273ad2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Bj=C3=B6rn=20Brandenburg?= <bbb@mpi-sws.org>
Date: Thu, 2 Apr 2020 21:11:07 +0200
Subject: [PATCH] add trivial replace_at definition rewriting lemma
---
analysis/facts/transform/replace_at.v | 12 ++++++++++--
1 file changed, 10 insertions(+), 2 deletions(-)
diff --git a/analysis/facts/transform/replace_at.v b/analysis/facts/transform/replace_at.v
index 51a0aad4f..eabb21998 100644
--- a/analysis/facts/transform/replace_at.v
+++ b/analysis/facts/transform/replace_at.v
@@ -25,8 +25,16 @@ Section ReplaceAtFacts.
t'. *)
Let sched' := replace_at sched t' nstate.
- (** We begin with the trivial observation that the schedule doesn't change at
- other times. *)
+ (** We begin with the trivial observation that [replace_at sched t' nstate]
+ indeed returns [nstate] at time [t']. *)
+ Lemma replace_at_def:
+ sched' t' = nstate.
+ Proof.
+ rewrite /sched' /replace_at.
+ now apply ifT.
+ Qed.
+
+ (** Equally trivially, the schedule doesn't change at other times. *)
Lemma rest_of_schedule_invariant:
forall t, t <> t' -> sched' t = sched t.
Proof.
--
GitLab