From 8d250037e754039136ce376af09b4326ec9b35dc Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 24 Apr 2016 14:38:05 -0400
Subject: [PATCH] SharedMemory: prove that our running-time bound relation is
 not total

---
 SharedMemory.v | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/SharedMemory.v b/SharedMemory.v
index 757b326..2c87f2c 100644
--- a/SharedMemory.v
+++ b/SharedMemory.v
@@ -656,6 +656,32 @@ Inductive boundRunningTime : cmd -> nat -> Prop :=
     -> boundRunningTime c2 n2
     -> boundRunningTime (Par c1 c2) (pow2 (n1 + n2)).
 
+Theorem boundRunningTime_not_total : exists c, forall n, ~boundRunningTime c n.
+Proof.
+  Fixpoint scribbly (n : nat) : cmd :=
+    match n with
+    | O => Return 0
+    | S n' => _ <- Write n' 0; scribbly n'
+    end.
+
+  Lemma scribbly_time : forall n m,
+      boundRunningTime (scribbly n) m
+      -> m >= n.
+  Proof.
+    induct n; invert 1; auto.
+    invert H2.
+    specialize (H4 n0).
+    apply IHn in H4.
+    linear_arithmetic.
+  Qed.
+
+  exists (n <- Read 0; scribbly n); propositional.
+  invert H.
+  specialize (H4 (S n2)).
+  apply scribbly_time in H4.
+  linear_arithmetic.
+Qed.
+
 Lemma pow2_pos : forall n,
     pow2 n > 0.
 Proof.