From 754784c2867847a82e48366e93b948c22f5be4d7 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adamc@csail.mit.edu>
Date: Mon, 8 Feb 2016 18:14:11 -0500
Subject: [PATCH] TransitionSystems WIP

---
 Invariant.v         | 40 +++++++++++++++++++++++-----------------
 TransitionSystems.v | 44 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 67 insertions(+), 17 deletions(-)

diff --git a/Invariant.v b/Invariant.v
index ce29c07..36047f1 100644
--- a/Invariant.v
+++ b/Invariant.v
@@ -1,35 +1,41 @@
 Require Import Relations.
 
+Set Implicit Arguments.
 
-Definition invariantFor {state} (initial : state -> Prop) (step : state -> state -> Prop) (invariant : state -> Prop) :=
-  forall s, initial s
-            -> forall s', step^* s s'
+
+Record trsys state := {
+  Initial : state -> Prop;
+  Step : state -> state -> Prop
+}.
+
+Definition invariantFor {state} (sys : trsys state) (invariant : state -> Prop) :=
+  forall s, sys.(Initial) s
+            -> forall s', sys.(Step)^* s s'
                           -> invariant s'.
 
-Theorem use_invariant : forall {state} (initial : state -> Prop)
-  (step : state -> state -> Prop) (invariant : state -> Prop) s s',
-  step^* s s'
-  -> initial s
-  -> invariantFor initial step invariant
+Theorem use_invariant : forall {state} (sys : trsys state) (invariant : state -> Prop) s s',
+  sys.(Step)^* s s'
+  -> sys.(Initial) s
+  -> invariantFor sys invariant
   -> invariant s'.
 Proof.
   firstorder.
 Qed.
 
-Theorem invariantFor_monotone : forall {state} (initial : state -> Prop)
-  (step : state -> state -> Prop) (invariant1 invariant2 : state -> Prop),
+Theorem invariantFor_monotone : forall {state} (sys : trsys state)
+  (invariant1 invariant2 : state -> Prop),
   (forall s, invariant1 s -> invariant2 s)
-  -> invariantFor initial step invariant1
-  -> invariantFor initial step invariant2.
+  -> invariantFor sys invariant1
+  -> invariantFor sys invariant2.
 Proof.
   unfold invariantFor; intuition eauto.
 Qed.
 
-Theorem invariant_induction : forall {state} (initial : state -> Prop)
-  (step : state -> state -> Prop) (invariant : state -> Prop),
-  (forall s, initial s -> invariant s)
-  -> (forall s, invariant s -> forall s', step s s' -> invariant s')
-  -> invariantFor initial step invariant.
+Theorem invariant_induction : forall {state} (sys : trsys state)
+  (invariant : state -> Prop),
+  (forall s, sys.(Initial) s -> invariant s)
+  -> (forall s, invariant s -> forall s', sys.(Step) s s' -> invariant s')
+  -> invariantFor sys invariant.
 Proof.
   unfold invariantFor; intros.
   assert (invariant s) by eauto.
diff --git a/TransitionSystems.v b/TransitionSystems.v
index ab7065b..0093e6d 100644
--- a/TransitionSystems.v
+++ b/TransitionSystems.v
@@ -110,6 +110,50 @@ Proof.
    * both [trc] and [fact_step]. *)
 Qed.
 
+(* It will be useful to give state machines more first-class status, as
+ * *transition systems*, formalized by this record type.  It has one type
+ * parameter, [state], which records the type of states. *)
+Record trsys state := {
+  Initial : state -> Prop;
+  Step : state -> state -> Prop
+}.
+
+Definition invariantFor {state} (sys : trsys state) (invariant : state -> Prop) :=
+  forall s, sys.(Initial) s
+            -> forall s', sys.(Step)^* s s'
+                          -> invariant s'.
+
+Theorem use_invariant : forall {state} (sys : trsys state) (invariant : state -> Prop) s s',
+  sys.(Step)^* s s'
+  -> sys.(Initial) s
+  -> invariantFor sys invariant
+  -> invariant s'.
+Proof.
+  firstorder.
+Qed.
+
+Theorem invariantFor_monotone : forall {state} (sys : trsys state)
+  (invariant1 invariant2 : state -> Prop),
+  (forall s, invariant1 s -> invariant2 s)
+  -> invariantFor sys invariant1
+  -> invariantFor sys invariant2.
+Proof.
+  unfold invariantFor; intuition eauto.
+Qed.
+
+Theorem invariant_induction : forall {state} (sys : trsys state)
+  (invariant : state -> Prop),
+  (forall s, sys.(Initial) s -> invariant s)
+  -> (forall s, invariant s -> forall s', sys.(Step) s s' -> invariant s')
+  -> invariantFor sys invariant.
+Proof.
+  unfold invariantFor; intros.
+  assert (invariant s) by eauto.
+  clear H1.
+  induction H2; eauto.
+Qed.
+
+
 (* To prove that our state machine is correct, we rely on the crucial technique
  * of *invariants*.  What is an invariant?  Here's a general definition, in
  * terms of an arbitrary *transition system* defined by a set of states,