Definition of the invariant for the room heating example.

darcs-hash:20090531195756-20b81-868ad71e7e50753d83a4c9909850b98fe73bfd5f.gz

room_heating.v

@@ -1,7 +1,9 @@
 Require Import QArith.
 Require Export vec_util.
 Require Import c_util.
+Require Import nat_util.
 Require Import Program.
+Require Import CRln.
 
 Set Implicit Arguments.
 
@@ -38,6 +40,7 @@ Module Type RoomHeatingSpec.
 
 End RoomHeatingSpec.
 
+Local Open Scope CR_scope.
 
 (** * Instantiation of room heating to a given 
       specification *)
@@ -59,9 +62,14 @@ Module RoomHeating (Import RHS : RoomHeatingSpec).
   Definition CS := vector CR n.
 
   Definition State := (DS * CS)%type.
+  Definition ds : State -> DS := fst.
+  Definition cs : State -> CS := snd.
+
+  Program Definition temp (cs : CS) (ip : dom_lt n) : CR :=
+    Vnth cs ip.
 
   Definition initial : DS :=
-    let init_room i ip :=
+    let init_room ip :=
       match Vnth initHeaters ip with 
       | false => NoHeater
       | true =>
@@ -75,4 +83,19 @@ Module RoomHeating (Import RHS : RoomHeatingSpec).
     in
       Vbuild init_room.
 
+  Definition invariant (s : State) : Prop :=
+    let check_room ip :=
+      let temp := Vnth (cs s) ip in
+      let roomState := Vnth (ds s) ip in
+        match roomState with
+          (* no heater, no invariant *)
+        | NoHeater => True
+          (* heater on, temperature below [off] threshold *)
+        | HeaterOn => temp <= '(Vnth off ip)
+          (* heater off, temperature above [on] threshold *)
+        | HeaterOff => '(Vnth on ip) <= temp
+        end
+    in
+      Vcheck_n check_room.
+
 End RoomHeating.

util.v

@@ -206,3 +206,24 @@ Hint Constructors unit.
 Require Import Ensembles.
 Notation "x ⊆ y" := (Ensembles.Included _ x y) (at level 40).
 Implicit Arguments Complement [U].
+
+Require Import EqdepFacts.
+Require Import Eqdep_dec.
+
+Section eq_dep.
+
+Variables (U : Type) (eq_dec : forall x y : U, {x=y}+{~x=y}).
+
+Lemma eq_rect_eq : forall (p : U) Q x h, x = eq_rect p Q x p h.
+
+Proof.
+exact (eq_rect_eq_dec eq_dec).
+Qed.
+
+Lemma eq_dep_eq : forall P (p : U) x y, eq_dep U P p x p y -> x = y.
+
+Proof.
+exact (eq_rect_eq__eq_dep_eq U eq_rect_eq).
+Qed.
+
+End eq_dep.

vec_util.v

@@ -1,68 +1,72 @@
 Require Export Bvector.
 Require Import Program.
 Require Import Omega.
+Require Import nat_util.
+Require Import util.
 
 Set Implicit Arguments.
 
 Implicit Arguments Vnil [A].
 Implicit Arguments Vcons.
 
-Section Vnth.
+Section vector.
+
+Variable n : nat.
+Variable A : Type.
 
-  Variable A : Type.
+Section Vnth.
 
-  Program Fixpoint Vnth n (v : vector A n) : forall i, i < n -> A :=
+  Program Fixpoint Vnth n (v : vector A n) : dom_lt n -> A :=
     match v with
     | Vnil => 
-        fun i ip => !
+        fun ip => !
     | Vcons x p v' =>
-        fun i =>
-          match i with
-          | 0 => fun _ => x
-          | S j => fun H => Vnth v' (i:=j) _
+        fun ip =>
+          match dom_lt_val ip with
+          | 0 => x
+          | S j => Vnth v' (dom_build (i:=j) _)
           end
     end.
 
   Next Obligation.
   Proof.
-    inversion ip.
+    inversion ip. inversion H.
   Qed.
   Next Obligation.
   Proof.
-    auto with arith.
+    destruct ip. simpl in *. subst. auto with arith.
   Qed.
 
 End Vnth.
 
 Section Vbuild.
 
-  Variable A : Type.
-
-  Program Fixpoint Vbuild_spec (n : nat) (gen : forall i, i < n -> A) :
-    { v : vector A n | forall i (ip : i < n), Vnth v ip = gen i ip } :=
+  Program Fixpoint Vbuild_spec n (gen : dom_lt n -> A) :
+    { v : vector A n | forall (ip : dom_lt n), Vnth v ip = gen ip } :=
     match n with
     | 0 => Vnil
     | S p => 
-        let gen' := fun i ip => gen (S i) _ in
-          Vcons (gen 0 _) (@Vbuild_spec p gen')
+        let gen' ip := gen (dom_build (i:=S (dom_lt_val ip)) _) in
+          Vcons (gen (dom_build (i:=0) _)) (@Vbuild_spec p gen')
     end.
 
   Next Obligation.
   Proof.
-    elimtype False. subst n. omega.
+    destruct ip. elimtype False. subst. omega.
   Qed.
   Next Obligation.
-    omega.
+    destruct ip. simpl. omega.
   Qed.
   Next Obligation.
     omega.
   Qed.
   Next Obligation.
     destruct_call Vbuild_spec. simpl.
-    destruct n. discriminate.
+    destruct n0. discriminate.
     inversion Heq_n. subst.
-    simplify_eqs. destruct i. pi.
-    rewrite e. pi.
+    destruct ip.
+    simplify_eqs. destruct x0. unfold dom_build. pi.
+    rewrite e. unfold dom_build. pi.
   Defined.
 
   Program Definition Vbuild n gen : vector A n := Vbuild_spec gen.
@@ -73,12 +77,56 @@ Require Import List.
 
 Section vec_of_list.
 
-  Variable A : Type.
-
   Fixpoint vec_of_list (l : list A) : vector A (length l) :=
     match l with
     | nil => Vnil
     | cons x m => Vcons x (vec_of_list m)
     end.
 
 End vec_of_list.
+
+Section Vforall2.
+
+  Variable R : A -> A -> Prop.
+
+  Fixpoint Vforall2_aux n1 (v1 : vector A n1) n2 (v2 : vector A n2) {struct v1} : Prop :=
+    match v1, v2 with
+    | Vnil, Vnil => True
+    | Vcons a _ v, Vcons b _ w => R a b /\ Vforall2_aux v w
+    | _, _ => False
+    end.
+
+  Definition Vforall2 n (v1 v2 : vector A n) := Vforall2_aux v1 v2.
+
+End Vforall2.
+
+End vector.
+
+Section VCheck_n.
+
+  Variables 
+    (n : nat) 
+    (P : dom_lt n -> Prop).
+
+  Program Fixpoint Vcheck_n_aux (p : nat | p <= n) 
+    {measure (fun p => n - p) p} : Prop :=
+
+    match le_lt_dec n p with
+    | left _ => True
+    | right cmp =>
+        @P p /\ @Vcheck_n_aux (S p)
+    end.
+
+  Next Obligation.
+  Proof.
+    omega.
+  Qed.
+
+  Program Definition Vcheck_n := @Vcheck_n_aux 0.
+
+  Next Obligation.
+  Proof.
+    omega.
+  Qed.
+
+End VCheck_n.