From c750b189d10506e4c3e03dbc9cbde7001aacd1c7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Feb 2015 13:07:34 +0100
Subject: [PATCH] show that internal equality on discrete types is timeless
---
iris_core.v | 13 +++++++++++++
1 file changed, 13 insertions(+)
diff --git a/iris_core.v b/iris_core.v
index 5609f3f44..b6835b6b4 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -189,6 +189,19 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
End Timeless.
+ Section IntEqTimeless.
+ Context {T} `{tT: Setoid T}.
+ (* This only works for types with the discrete metric! *)
+ Local Instance mT: metric T := discreteMetric.
+
+ Lemma intEqTimeless (t1 t2: T):
+ valid(timeless(intEq t1 t2)).
+ Proof.
+ intros w n r. intros w' k r' Hsq Hlt.
+ simpl. tauto.
+ Qed.
+ End IntEqTimeless.
+
Section Ownership.
(** Ownership **)
--
GitLab