From 65c56a7a2efc07c5bc7ab1c90d04b2356e51e003 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 21 Feb 2016 17:00:01 -0500
Subject: [PATCH] Tweak model-checking library support

---
 Frap.v       | 12 +++++++---
 ModelCheck.v | 63 +++++++++++++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 71 insertions(+), 4 deletions(-)

diff --git a/Frap.v b/Frap.v
index 75a9f4c..b50e9d5 100644
--- a/Frap.v
+++ b/Frap.v
@@ -96,8 +96,11 @@ Ltac first_order := firstorder idtac.
 Ltac model_check_done :=
   apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst;
   repeat match goal with
-         | [ H : _ |- _ ] => invert H
-         end; simplify; equality.
+         | [ H : ?P |- _ ] =>
+           match type of P with
+           | Prop => invert H; simplify
+           end
+         end; equality.
 
 Ltac singletoner :=
   repeat match goal with
@@ -110,7 +113,10 @@ Ltac model_check_step :=
     repeat (apply oneStepClosure_empty
             || (apply oneStepClosure_split; [ simplify;
                                               repeat match goal with
-                                                     | [ H : _ |- _ ] => invert H; simplify; try congruence
+                                                     | [ H : ?P |- _ ] =>
+                                                       match type of P with
+                                                       | Prop => invert H; simplify; try congruence
+                                                       end
                                                      end; solve [ singletoner ] | ]))
   | simplify ].
 
diff --git a/ModelCheck.v b/ModelCheck.v
index f7a25ab..233a0bc 100644
--- a/ModelCheck.v
+++ b/ModelCheck.v
@@ -1,4 +1,7 @@
-Require Import Invariant Sets.
+Require Import Invariant Relations Sets.
+
+Set Implicit Arguments.
+
 
 Definition oneStepClosure_current {state} (sys : trsys state)
            (invariant1 invariant2 : state -> Prop) :=
@@ -95,3 +98,61 @@ Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A),
 Proof.
   unfold union; simpl; auto.
 Qed.
+
+
+(** * Abstraction *)
+
+Inductive simulates state1 state2 (R : state1 -> state2 -> Prop)
+  (sys1 : trsys state1) (sys2 : trsys state2) : Prop :=
+| Simulates :
+  (forall st1, sys1.(Initial) st1
+               -> exists st2, R st1 st2
+                              /\ sys2.(Initial) st2)
+  -> (forall st1 st2, R st1 st2
+                      -> forall st1', sys1.(Step) st1 st1'
+                                      -> exists st2', R st1' st2'
+                                                      /\ sys2.(Step) st2 st2')
+  -> simulates R sys1 sys2.
+
+Inductive invariantViaSimulation state1 state2 (R : state1 -> state2 -> Prop)
+  (inv2 : state2 -> Prop)
+  : state1 -> Prop :=
+| InvariantViaSimulation : forall st1 st2, R st1 st2
+  -> inv2 st2
+  -> invariantViaSimulation R inv2 st1.
+
+Lemma invariant_simulates' : forall state1 state2 (R : state1 -> state2 -> Prop)
+  (sys1 : trsys state1) (sys2 : trsys state2),
+  (forall st1 st2, R st1 st2
+                   -> forall st1', sys1.(Step) st1 st1'
+                                   ->  exists st2', R st1' st2'
+                                                    /\ sys2.(Step) st2 st2')
+  -> forall st1 st1', sys1.(Step)^* st1 st1'
+                      -> forall st2, R st1 st2
+                                     -> exists st2', R st1' st2'
+                                                     /\ sys2.(Step)^* st2 st2'.
+Proof.
+  induction 2; simpl; intuition eauto.
+
+  eapply H in H2.
+  firstorder.
+  apply IHtrc in H2.
+  firstorder; eauto.
+  eauto.
+Qed.
+
+Local Hint Constructors invariantViaSimulation.
+
+Theorem invariant_simulates : forall state1 state2 (R : state1 -> state2 -> Prop)
+  (sys1 : trsys state1) (sys2 : trsys state2) (inv2 : state2 -> Prop),
+  simulates R sys1 sys2
+  -> invariantFor sys2 inv2
+  -> invariantFor sys1 (invariantViaSimulation R inv2).
+Proof.
+  inversion_clear 1; intros.
+  unfold invariantFor; intros.
+  apply H0 in H2.
+  firstorder.
+  apply invariant_simulates' with (sys2 := sys2) (R := R) (st2 := x) in H3; auto.
+  firstorder; eauto.
+Qed.