Removing vec_util and instead using CoLoR (to avoid duplication and m…

…oving code back-and-forth)

darcs-hash:20090606171913-20b81-722dd1e5c68959adca9c70fc096204ab6e90e7a3.gz

SConstruct

@@ -1,18 +1,6 @@
 import os, glob, string
 corn_dir = '~/coq_libs/CoRN'
-
-Rs = [(corn_dir, 'CoRN'), ('.', 'hybrid')]
-Rs = string.join(map(lambda (x,y): '-R "' + x + '" ' + y, Rs))
-
-coqc = 'coqc ' + Rs
-
-def make_abs(s):
-  if s[0] != '/': return Dir("#").abspath + "/" + s
-  else: return s
-
-def coq_scan(node, env, path):
-  return map(make_abs, os.popen("coqdep -I . " + Rs + " -w " + str(node) + " 2> /dev/null").read().strip().split(' ')[2:])
-
+coqc = 'coqc -R ' + corn_dir + ' CoRN'
 env = DefaultEnvironment(ENV = os.environ)
 env.Append(BUILDERS = {'Coq' : Builder(action = coqc + ' $SOURCE', suffix = '.vo', src_suffix = '.v')})
 env.Append(SCANNERS = Scanner(skeys = ['.v'], function = coq_scan))

bool_util.v

@@ -1,4 +1,30 @@
 Require Export Bool.
+Require Setoid.
+
+Set Implicit Arguments.
+
+Section beq.
+
+  Variable A : Type.
+  Variable beq : A -> A -> bool.
+  Variable beq_ok : forall x y, beq x y = true <-> x = y.
+
+  Lemma beq_refl : forall x, beq x x = true.
+  Proof.
+    intros. rewrite (beq_ok x x). reflexivity.
+  Qed.
+
+End beq.
+
+Lemma andb_intro : forall a b, a = true -> b = true -> a && b = true.
+Proof.
+  intros. subst. reflexivity.
+Qed.
+
+Lemma andb_elim : forall a b, a && b = true -> a = true /\ b = true.
+Proof.
+  destruct a; destruct b; intuition.
+Qed.
 
 Lemma band_discr : forall b1 b2,
   b1 = true ->

room_heating.v

@@ -1,10 +1,13 @@
 Require Import QArith.
-Require Export vec_util.
+Require Import util.
 Require Import c_util.
 Require Import nat_util.
+Require Import list_util.
 Require Import Program.
-Require square_abstraction.
 Require Import CRln.
+Require Import hs_solver.
+Require Import CoLoR.Util.Vector.VecUtil.
+Require square_abstraction.
 
 Set Implicit Arguments.
 
@@ -29,7 +32,7 @@ Module Type RoomHeatingSpec.
 
    (** For every room the [on] threshold needs to be strictly 
        smaller than the [off] threshold. *)
-  Parameter on_lt_off : Vforall2 (fun on off => on < off) on off.
+  Parameter on_lt_off : Vforall2n (fun on off => on < off) on off.
 
    (** heater can be moved to room [i] only if the 
        temperature in this room is below [get_i]. *)
@@ -79,12 +82,12 @@ Module RoomHeating (Import RHS : RoomHeatingSpec).
 
    (** initial state predicate *)
   Definition initial (s : State) : Prop :=
-    let init_room i :=
-      match initHeaters [[i]] with 
+    let init_room i ip :=
+      match initHeaters [@ip] with 
       | false => NoHeater
       | true =>
-          let temp := initTemp [[i]] in
-          let threshold := on [[i]] in
+          let temp := initTemp [@ip] in
+          let threshold := on [@ip] in
             match Qlt_le_dec temp threshold with
             | left _ => HeaterOn
             | right _ => HeaterOff
@@ -93,37 +96,37 @@ Module RoomHeating (Import RHS : RoomHeatingSpec).
     in
     let check_temp actual prescribed := actual = 'prescribed in
       ds s = Vbuild init_room /\
-      Vforall2 check_temp (cs s) initTemp.
+      Vforall2n check_temp (cs s) initTemp.
 
    (** invariant *)
   Definition invariant (s : State) : Prop :=
-    let check_room i :=
-      let temp := (cs s) [[i]] in
-      let roomState := (ds s) [[i]] in
+    let check_room i ip :=
+      let temp := (cs s) [@ip] in
+      let roomState := (ds s) [@ip] in
         match roomState with
           (* no heater, no invariant *)
         | NoHeater => True
           (* heater on, temperature below [off] threshold *)
-        | HeaterOn => temp <= '(off [[i]])
+        | HeaterOn => temp <= '(off [@ip])
           (* heater off, temperature above [on] threshold *)
-        | HeaterOff => '(on [[i]]) <= temp
+        | HeaterOff => '(on [@ip]) <= temp
         end
     in
-      Vcheck_n check_room.
+      check_n check_room.
 
   Lemma initial_invariant s : initial s -> invariant s.
   Proof with auto.
     intros [dS cS] [init_dS init_cS].
     simpl in *. subst.
-    apply Vcheck_n_holds. intros. simpl in *.
-    unfold roomState. rewrite Vnth_Vbuild.
-    destruct (initHeaters [[ip]])...
+    apply check_n_holds. intros. simpl in *.
+    unfold roomState. rewrite Vbuild_nth.
+    destruct (initHeaters [@ip])...
     unfold temp.
-    destruct (Qlt_le_dec (initTemp [[ip]]) (on [[ip]]));
-      rewrite (Vforall2_elim _ _ _ init_cS ip);
+    destruct (Qlt_le_dec (initTemp [@ip]) (on [@ip]));
+      rewrite (Vforall2n_nth _ _ _ ip init_cS);
       eapply (proj2 (CRle_Qle _ _))...
-    apply Qlt_le_weak. apply Qlt_trans with (on [[ip]])...
-    apply (Vforall2_elim _ _ _ on_lt_off).
+    apply Qlt_le_weak. apply Qlt_trans with (on [@ip])...
+    apply (Vforall2n_nth _ _ _ ip on_lt_off).
   Qed.
 
   Definition temp_reset (l1 l2 : DS) : square_abstraction.Reset :=
@@ -135,18 +138,17 @@ Module RoomHeating (Import RHS : RoomHeatingSpec).
   Definition guard (s : State) (l2 : DS) : Prop :=
     let (l1, cs) := s in
       (* a heater is moved from room [j] to room [i] *)
-      exists i, exists j,
+      exists i, exists ip : (i < n)%nat,
+      exists j, exists jp : (j < n)%nat,
          (* rooms other than [i] and [j] remain unchanged *)
-        (forall p : dom_lt n, 
-          dom_lt_val p <> dom_lt_val i -> 
-          dom_lt_val p <> dom_lt_val j ->
-          l1 [[p]] = l2 [[p]]) /\
+        (forall k (kp : (k < n)%nat), 
+          k <> i -> k <> j -> l1 [@kp] = l2 [@kp]) /\
          (* room [i] had no heater and now gets one *)
-        hasHeater (l1 [[i]]) = false /\ hasHeater (l2 [[i]]) = true /\
+        hasHeater (l1 [@ip]) = false /\ hasHeater (l2 [@ip]) = true /\
          (* room [j] had a heater and now it's removed *)
-        hasHeater (l1 [[j]]) = true  /\ hasHeater (l2 [[j]]) = false /\
+        hasHeater (l1 [@jp]) = true  /\ hasHeater (l2 [@jp]) = false /\
          (* temperature in room [i] is <= [get_i] *)
-        cs [[i]] <= '(get [[i]]) /\
+        cs [@ip] <= '(get [@ip]) /\
          (* the difference of temperatures in rooms [j] and [i] is at 
             least [diff_i] *)
         '(diff [[i]]) <= (cs [[j]]) - (cs [[i]]).