Move old non-constructive development into subdir, and get rid of c_ …

…prefixes in main development.

Ignore-this: f04b8063fd5c7a14f4d59bad51992b63

darcs-hash:20090423105535-bab43-5d58542d7a089364176c2119af85082464d6085f.gz

abstract.v

@@ -1,25 +1,121 @@
 Require Import reachability.
 Require Import List.
-Require Import util.
+Require Import dec_overestimator.
+Require Import list_util.
 Set Implicit Arguments.
+Require EquivDec.
+Require concrete.
 
-Record System: Type :=
-  { State: Set
-  ; state_eq_dec: forall s s': State, decision (s=s')
-  ; states: list State
-  ; states_exhaustive: forall s, In s states
-  ; initial: State -> bool
-  ; cont_trans: State -> list State
-  ; disc_trans: State -> list State
-      (* hm, why do we need to distinguish between these? *)
-  }.
-
-Implicit Arguments initial [s].
+Section contents.
+
+  Variable chs: concrete.System.
+
+  Section pre.
+
+    Context {Region: Set}.
+
+    Definition State := (concrete.Location chs * Region)%type.
+
+    Context
+      {Region_eq_dec: EquivDec.EqDec Region eq}
+      {regions: ExhaustiveList Region}.
+
+    Hypothesis NoDup_regions: NoDup regions.
+
+    Definition states := @ExhaustivePairList (concrete.Location chs) Region _ _.
+
+    Lemma NoDup_states : NoDup states.
+    Proof with auto.
+      unfold exhaustive_list. simpl.
+      apply NoDup_flat_map; intros.
+          destruct (fst (in_map_iff (pair a) regions x) H1).
+          destruct (fst (in_map_iff (pair b) regions x) H2).
+          destruct H3. destruct H4.
+          subst. inversion H4...
+        apply NoDup_map...
+        intros. inversion H2...
+      apply concrete.NoDup_locations.
+    Qed.
+
+  End pre.
+
+  Implicit Arguments State [].
+
+  Record System: Type :=
+    { Region: Set
+    ; Region_eq_dec: EquivDec.EqDec Region eq
+    ; regions: ExhaustiveList Region
+    ; NoDup_regions: NoDup regions
+    ; select_region: concrete.Point chs -> Region
+    ; initial_dec: State Region -> bool
+    ; initial_pred : initial_dec >=> (fun s : State Region =>
+      let (l, r) := s in
+        exists p, select_region p = r /\ concrete.initial (l, p))
+    ; disc_trans: State Region -> list (State Region)
+    ; NoDup_disc_trans: forall s, NoDup (disc_trans s)
+    ; disc_resp: forall s1 s2 : concrete.State chs,
+        let (l1, p1) := s1 in
+        let (l2, p2) := s2 in
+          concrete.disc_trans s1 s2 ->
+          In (l2, select_region p2) (disc_trans (l1, select_region p1))
+    ; cont_trans: State Region -> list Region
+    ; NoDup_cont_trans: forall s, NoDup (cont_trans s)
+    ; cont_resp: forall l s1 s2,
+        concrete.cont_trans' chs l s1 s2 ->
+        In (select_region s2) (cont_trans (l, select_region s1))
+    }.
+
+  Variable ahs: System.
+
+  Let State := State (Region ahs).
+  Let c_State := concrete.State chs.
+
+  Definition abs (s : c_State) : State :=
+    let (l, p) := s in
+      (l, select_region ahs p).
+
+  Definition trans (b : bool) (s1 s2 : State) : Prop :=
+    let (l1, p1) := s1 in
+    let (l2, p2) := s2 in
+      if b then
+        l1 = l2 /\ In p2 (cont_trans _ s1)
+      else
+        In s2 (disc_trans _ s1).
+
+  Definition reachable (s : State) : Prop :=
+    exists is : State, 
+      initial_dec ahs is = true /\ reachable_alternating trans is s.
+
+  Lemma reachable_alternating_concrete_abstract (s : concrete.State chs) :
+    concrete.reachable_alternating s -> reachable (abs s).
+  Proof with auto.
+    intros. destruct H as [is [is_init ra]]. exists (abs is).
+    simpl. split.
+    change (do_pred (mk_DO (initial_pred ahs)) (abs is) = true).
+    apply do_over_true. destruct is as [il ip]. exists ip...
+    destruct ra as [b trace]. exists (negb b). 
+    induction trace. 
+    apply end_with_refl.
+    apply end_with_next with (abs y)...
+    set (dr := disc_resp ahs y z).
+    destruct y. destruct z. destruct b. unfold trans; simpl.
+    apply dr...
+    split.
+    destruct H...
+    apply cont_resp. destruct H...
+  Qed.
+
+  Lemma reachable_concrete_abstract (s : concrete.State chs) :
+    concrete.reachable s -> reachable (abs s).
+  Proof.
+    intros. apply reachable_alternating_concrete_abstract.
+    apply concrete.alternating_reachable. hyp.
+  Qed.
+
+End contents.
+
+Hint Resolve Region_eq_dec regions: typeclass_instances.
+Implicit Arguments State [].
+Implicit Arguments initial_dec [s].
 Implicit Arguments cont_trans [s].
 Implicit Arguments disc_trans [s].
-
-Definition reachable {system: System} (s: State system): Prop :=
-  exists i, initial i = true /\
-    reachable_alternating i
-      (fun a b => In b (disc_trans a))
-      (fun a b => In b (cont_trans a)) s.

abstract_as_graph.v

@@ -2,16 +2,16 @@ Require Import List.
 Require Import Bool.
 Require Import util.
 Require Import list_util.
-Require c_abstract.
+Require abstract.
 Require Import reachability.
 Require digraph.
 Require Import dec_overestimator.
 Set Implicit Arguments.
 
 Section using_duplication.
 
-  Variable chs: c_concrete.System.
-  Variable ahs: c_abstract.System chs.
+  Variable chs: concrete.System.
+  Variable ahs: abstract.System chs.
 
   Inductive TransKind := Cont | Disc.
 
@@ -25,11 +25,11 @@ Section using_duplication.
   Definition flip (k: TransKind) :=
     match k with Cont => Disc | Disc => Cont end.
 
-  Let a_State := c_abstract.State chs (c_abstract.Region ahs).
+  Let a_State := abstract.State chs (abstract.Region ahs).
 
   Let V := (TransKind * a_State)%type.
 
-  Definition all_abstract_states := @c_abstract.states chs _ _ (c_abstract.regions ahs).
+  Definition all_abstract_states := @abstract.states chs _ _ (abstract.regions ahs).
 
   Definition states_to_verts (s : list a_State) := map (pair Cont) s ++ map (pair Disc) s.
 
@@ -40,8 +40,8 @@ Section using_duplication.
     match k with
     | Cont => 
         let (l, r) := s in
-          map (pair l) (c_abstract.cont_trans _ s)
-    | Disc => c_abstract.disc_trans _ s
+          map (pair l) (abstract.cont_trans _ s)
+    | Disc => abstract.disc_trans _ s
     end.
 
   Definition next (v: V) : list V :=
@@ -52,8 +52,8 @@ Section using_duplication.
     intros. apply NoDup_map...
     destruct v. destruct a. destruct t; simpl. 
     apply NoDup_map...
-    apply c_abstract.NoDup_cont_trans.
-    apply c_abstract.NoDup_disc_trans.
+    apply abstract.NoDup_cont_trans.
+    apply abstract.NoDup_disc_trans.
   Qed.
 
   Lemma NoDup_states_to_verts s : NoDup s -> NoDup (states_to_verts s).
@@ -64,12 +64,12 @@ Section using_duplication.
   Qed.
 
   Definition g : digraph.DiGraph :=
-    @digraph.Build (TransKind * c_abstract.State chs (c_abstract.Region ahs)) _ _ _ NoDup_next.
+    @digraph.Build (TransKind * abstract.State chs (abstract.Region ahs)) _ _ _ NoDup_next.
 
   Lemma respect (s : a_State) : 
-    c_abstract.reachable _ s ->
+    abstract.reachable _ s ->
     exists k, exists v : digraph.Vertex g,
-    c_abstract.initial_dec chs (snd v) = true /\
+    abstract.initial_dec chs (snd v) = true /\
     digraph.reachable v (k, s).
   Proof with auto.
     intros s [absS [init [tt reach_alt]]].
@@ -89,12 +89,12 @@ Section using_duplication.
   Qed.
 
   Definition graph_unreachable_prop s (v : digraph.Vertex g) : Prop :=
-    c_abstract.initial_dec chs (snd v) = true ->
+    abstract.initial_dec chs (snd v) = true ->
     ~digraph.reachable v (Cont, s) /\ ~digraph.reachable v (Disc, s).
 
   Lemma respect_inv (s: a_State) :
     (forall v: digraph.Vertex g, graph_unreachable_prop s v) ->
-    ~c_abstract.reachable _ s.
+    ~abstract.reachable _ s.
   Proof with auto.
     intros s rc abs_reach.
     destruct (respect abs_reach) as [tt [v [init reach]]].
@@ -103,21 +103,21 @@ Section using_duplication.
   Qed.
 
   Definition init_verts : list V :=
-    let is_initial v := c_abstract.initial_dec chs v in
+    let is_initial v := abstract.initial_dec chs v in
     let init_states := filter is_initial all_abstract_states in
       states_to_verts init_states.
 
   Lemma init_verts_eq_aux (tt : TransKind) ss :
-    map (pair tt) (filter (fun v => c_abstract.initial_dec chs (s:=ahs) v) ss) =
-    filter (fun s => c_abstract.initial_dec chs (snd s)) (map (pair tt) ss).
+    map (pair tt) (filter (fun v => abstract.initial_dec chs (s:=ahs) v) ss) =
+    filter (fun s => abstract.initial_dec chs (snd s)) (map (pair tt) ss).
   Proof.
     induction ss. ref. simpl. 
-    destruct (c_abstract.initial_dec chs a); simpl; rewrite IHss; ref.
+    destruct (abstract.initial_dec chs a); simpl; rewrite IHss; ref.
   Qed.
 
   Lemma init_verts_eq  :
     init_verts = 
-    filter (fun s => c_abstract.initial_dec chs (snd s)) 
+    filter (fun s => abstract.initial_dec chs (snd s))
     vertices.
   Proof.
     unfold init_verts, states_to_verts.
@@ -129,8 +129,8 @@ Section using_duplication.
   Proof.
     apply NoDup_states_to_verts.
     apply NoDup_filter.
-    apply c_abstract.NoDup_states.
-    apply c_abstract.NoDup_regions.
+    apply abstract.NoDup_states.
+    apply abstract.NoDup_regions.
   Qed.
 
   Definition state_reachable vr s : bool :=
@@ -149,7 +149,7 @@ Section using_duplication.
 Hint Resolve in_filter.
 
   Lemma over_abstract_reachable : 
-    state_reachable reachable_verts >=> c_abstract.reachable ahs.
+    state_reachable reachable_verts >=> abstract.reachable ahs.
   Proof with auto.
     intros s sur. apply respect_inv. intros v init_t.
     unfold state_reachable, reachable_verts in sur.
@@ -168,15 +168,15 @@ Hint Resolve in_filter.
   Lemma states_unreachable (ss : list a_State) :
     some_reachable ss = false ->
     forall s cs, 
-      In s ss -> c_abstract.abs ahs cs = s -> ~c_concrete.reachable cs.
+      In s ss -> abstract.abs ahs cs = s -> ~concrete.reachable cs.
   Proof with auto.
     intros. intro.
     contradict H. apply not_false_true.
     apply (snd (existsb_exists (state_reachable reachable_verts) ss)).
     exists s; split...
-    subst. apply over_true with a_State (c_abstract.reachable ahs).
+    subst. apply over_true with a_State (abstract.reachable ahs).
     apply over_abstract_reachable.
-    apply c_abstract.reachable_concrete_abstract...
+    apply abstract.reachable_concrete_abstract...
   Qed.
 
 End using_duplication.