TransitionSystems WIP

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
+Record trsys state := {
-            -> forall s', step^* s s'
+  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)
+Theorem use_invariant : forall {state} (sys : trsys state) (invariant : state -> Prop) s s',
-  (step : state -> state -> Prop) (invariant : state -> Prop) s s',
+  sys.(Step)^* s s'
-  step^* s s'
+  -> sys.(Initial) s
-  -> initial s
+  -> invariantFor sys invariant
-  -> invariantFor initial step invariant
   -> invariant s'.
 Proof.
   firstorder.
 Qed.
 
-Theorem invariantFor_monotone : forall {state} (initial : state -> Prop)
+Theorem invariantFor_monotone : forall {state} (sys : trsys state)
-  (step : state -> state -> Prop) (invariant1 invariant2 : state -> Prop),
+  (invariant1 invariant2 : state -> Prop),
   (forall s, invariant1 s -> invariant2 s)
-  -> invariantFor initial step invariant1
+  -> invariantFor sys invariant1
-  -> invariantFor initial step invariant2.
+  -> invariantFor sys invariant2.
 Proof.
   unfold invariantFor; intuition eauto.
 Qed.
 
-Theorem invariant_induction : forall {state} (initial : state -> Prop)
+Theorem invariant_induction : forall {state} (sys : trsys state)
-  (step : state -> state -> Prop) (invariant : state -> Prop),
+  (invariant : state -> Prop),
-  (forall s, initial s -> invariant s)
+  (forall s, sys.(Initial) s -> invariant s)
-  -> (forall s, invariant s -> forall s', step s s' -> invariant s')
+  -> (forall s, invariant s -> forall s', sys.(Step) s s' -> invariant s')
-  -> invariantFor initial step invariant.
+  -> invariantFor sys invariant.
 Proof.
   unfold invariantFor; intros.
   assert (invariant s) by eauto.

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,