vm_setoid

Author: k32

_CoqProject

@@ -6,6 +6,7 @@ theories/TokenMachine.v
 theories/TransitionSystem.v
 theories/Queue.v
 theories/Pid.v
+theories/ListSelector.v
 theories/VM.v
 theories/Handlers/Storage.v
 theories/Handlers/Mailbox.v

theories/ListSelector.v

@@ -1,7 +1,11 @@
 From Coq Require Import
   List.
+
 Import ListNotations.
 
+From Hammer Require Import
+  Tactics.
+
 Section defn.
   Context {A : Type}.
 
@@ -15,14 +19,11 @@ End defn.
 
 Section tests.
   Goal forall a l',
-      Pick [1; 2] a l' ->
-      (a = 1 /\ l' = [2]) \/ (a = 2 /\ l' = [1]).
+      Pick [1; 2; 3] a l' ->
+        (a = 1 /\ l' = [2; 3]) \/
+        (a = 2 /\ l' = [1; 3]) \/
+        (a = 3 /\ l' = [1; 2]).
   Proof.
-    intros a l' H.
-    inversion_clear H.
-    - now left.
-    - inversion_clear H0.
-      + now right.
-      + inversion H.
+    sauto.
   Qed.
 End tests.

theories/Multifunction.v

@@ -207,7 +207,7 @@ Section mfun_prod.
   Context {A B C D : Type} `{setoidA : Setoid A} `{setoidB : Setoid B} `{setoidC : Setoid C} `{setoidD : Setoid D}.
 
   Program Definition mfun_prod (f : @MFun A B setoidA setoidB) (g : @MFun C D setoidC setoidD) :
-    @MFun (A * C) (B * D) (setoidPair A C) (setoidPair B D) :=
+    @MFun (A * C) (B * D) (pair_setoid A C) (pair_setoid B D) :=
     {| morphism x y :=
         let (x_l, x_r) := x in
         let (y_l, y_r) := y in
@@ -224,7 +224,7 @@ Section mfun_sum.
   Context {A A' B : Type} `{setoidA : Setoid A} `{setoidA' : Setoid A'} `{setoidB : Setoid B}.
 
   Program Definition mfun_sum_l (f : @MFun A A' setoidA setoidA') :
-    @MFun (A * B) (A' * B) (setoidPair A B) (setoidPair A' B) :=
+    @MFun (A * B) (A' * B) (pair_setoid A B) (pair_setoid A' B) :=
     {| morphism x y :=
         let (x_l, x_r) := x in
         let (y_l, y_r) := y in
@@ -237,7 +237,7 @@ Section mfun_sum.
   Qed.
 
   Program Definition mfun_sum_r (f : @MFun A A' setoidA setoidA') :
-    @MFun (B * A) (B * A') (setoidPair B A) (setoidPair B A') :=
+    @MFun (B * A) (B * A') (pair_setoid B A) (pair_setoid B A') :=
     {| morphism x y :=
         let (x_l, x_r) := x in
         let (y_l, y_r) := y in

theories/Setoids.v

@@ -1,28 +1,32 @@
 From Coq Require Export
-  SetoidClass.
+  SetoidClass
+  Permutation.
 
 From Coq Require Import
   Program.
 
 From Hammer Require Import
   Tactics.
 
-Section setoid_pair.
+Section pair.
   Context (A B : Type) `{Setoid A} `{Setoid B}.
 
-  Program Instance setoidPair : Setoid (A * B) :=
+  Global Program Instance pair_setoid : Setoid (A * B) :=
     {| equiv (a b : (A * B)) :=
         let (a_l, a_r) := a in
         let (b_l, b_r) := b in
         equiv a_l b_l /\ equiv a_r b_r;
     |}.
   Solve All Obligations with sauto unfold:Reflexive,Symmetric,Transitive.
-End setoid_pair.
+End pair.
 
-Section setoid_option.
+Definition pair_setoid' {A B : Type} (a : Setoid A) (b : Setoid B) :=
+  @pair_setoid A B a b.
+
+Section option.
   Context (T : Type) `{Setoid T}.
 
-  Program Instance setoid_option : Setoid (option T) :=
+  Global Program Instance setoid_option : Setoid (option T) :=
     {| equiv (a b : option T) :=
         match a, b with
         | Some a, Some b => equiv a b
@@ -31,4 +35,11 @@ Section setoid_option.
         end;
     |}.
   Solve All Obligations with sauto unfold:Reflexive,Symmetric,Transitive.
-End setoid_option.
+End option.
+
+Section permutation.
+  Context (T : Type).
+
+  Global Program Instance setoid_permutation : Setoid (list T) | 10 :=
+    {| equiv a b := Permutation a b |}.
+End permutation.

theories/TransitionSystem.v

@@ -28,7 +28,7 @@ Section TransitionSystem.
   Definition ts_ret (Event : Type) := option (Event * State).
 
   Definition ts_ret_setoid (Event : Type) (Hss : Setoid State) :=
-    let sp := @setoidPair Event State (eq_setoid _) Hss in
+    let sp := @pair_setoid Event State (eq_setoid _) Hss in
     @setoid_option (Event * State) sp.
 
   Class TransitionSystem {Event : Type} :=

theories/VM.v

@@ -1,13 +1,15 @@
 From Coq Require Import
   List
   ZArith
-  SetoidClass.
+  SetoidClass
+  SetoidDec.
 Import ListNotations.
 
 From SLOT Require Import
   Setoids
   TransitionSystem
-  Pid.
+  Pid
+  ListSelector.
 
 From Hammer Require Import
   Tactics.
@@ -21,7 +23,7 @@ Section IOHandler.
   Context {Request : Type} {Reply : Request -> Type}.
 
   Definition MFunRet Ret State `{HRet : Setoid Ret} `{HState : Setoid State} :=
-    @MFun State (Ret * State) HState (@setoidPair _ _ HRet HState).
+    @MFun State (Ret * State) HState (@pair_setoid _ _ HRet HState).
 
   Class IOHandler := {
       h_state : Type;
@@ -39,8 +41,7 @@ Section VM.
   | p_dead : (* Program terminted *)
       Program
   | p_yield :
-      (* Wait for signal.
-
+      (* Interrupt the computation without producing any side effects.
       This primitive is used to softly introduce the concept of
       Erlang's "reductions", and to side-step termination checker,
       making programs non-Turing in a practically useful, as opposed
@@ -77,6 +78,22 @@ Section VM.
 
   #[export] Instance etaX : Settable _ := settable! mkVM <world; runq; sleepq; child_ctr>.
 
+  Program Definition vm_setoid : Setoid VM :=
+    {| equiv a b :=
+        let (w1, rq1, sq1, cc1) := a in
+        let (w2, rq2, sq2, cc2) := b in
+        let w_eq := @equiv _ h_setoid in
+        let p_eq := @equiv _ (setoid_permutation (PID * Program)) in
+        w_eq w1 w2 /\
+          p_eq rq1 rq2 /\
+          p_eq sq1 sq2 /\
+          @equiv _ (eq_setoid _) cc1 cc2;
+    |}.
+  Next Obligation.
+    sauto unfold:Reflexive,Symmetric,Transitive
+          use:Permutation_sym,Permutation_trans.
+  Qed.
+
   Definition new_child_id (parent : PID) (v : VM) : VM * positive :=
     let cc := child_ctr v in
     let (cc, ctr) :=