Initial state changed to a predicate + a proof that initial implies i…

…nvariant.

darcs-hash:20090531211457-20b81-38808243fa7ff24944741e56e53cd10ef9f220d7.gz

room_heating.v

@@ -26,6 +26,10 @@ Module Type RoomHeatingSpec.
   Parameter on : vectorQ n.
   Parameter off : vectorQ n.
 
+   (** 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.
+
    (** heater can be moved to room [i] only if the 
        temperature in this room is below [get_i]. *)
   Parameter get : vectorQ n.
@@ -68,7 +72,8 @@ Module RoomHeating (Import RHS : RoomHeatingSpec).
   Program Definition temp (cs : CS) (ip : dom_lt n) : CR :=
     Vnth cs ip.
 
-  Definition initial : DS :=
+   (** initial state predicate *)
+  Definition initial (s : State) : Prop :=
     let init_room ip :=
       match Vnth initHeaters ip with 
       | false => NoHeater
@@ -81,7 +86,9 @@ Module RoomHeating (Import RHS : RoomHeatingSpec).
             end
       end
     in
-      Vbuild init_room.
+    let check_temp actual prescribed := actual = 'prescribed in
+      ds s = Vbuild init_room /\
+      Vforall2 check_temp (cs s) initTemp.
 
   Definition invariant (s : State) : Prop :=
     let check_room ip :=
@@ -98,4 +105,19 @@ Module RoomHeating (Import RHS : RoomHeatingSpec).
     in
       Vcheck_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 (Vnth initHeaters ip)...
+    unfold temp0.
+    destruct (Qlt_le_dec (Vnth initTemp ip) (Vnth on ip));
+      rewrite (Vforall2_elim _ _ _ init_cS ip);
+      eapply (proj2 (CRle_Qle _ _))...
+    apply Qlt_le_weak. apply Qlt_trans with (Vnth on ip)...
+    apply (Vforall2_elim _ _ _ on_lt_off).
+  Qed.
+
 End RoomHeating.

room_heating_ex.v

@@ -19,6 +19,14 @@ Module RHS <: RoomHeatingSpec.
   Definition initHeaters := vec_of_list [true; true; false].
   Definition initTemp := vec_of_list [20:Q; 20:Q; 20:Q].
 
+  Lemma on_lt_off : Vforall2 (fun on off => on < off) on off.
+  Proof.
+    apply Vforall2_intro. intros.
+    destruct ip.
+    do 3 (destruct x; [vm_compute; trivial | idtac]).
+    simpl in l. elimtype False. omega.    
+  Qed.
+
 End RHS.
 
 Module RHSex := RoomHeating RHS.

vec_util.v

@@ -9,13 +9,10 @@ Set Implicit Arguments.
 Implicit Arguments Vnil [A].
 Implicit Arguments Vcons.
 
-Section vector.
-
-Variable n : nat.
-Variable A : Type.
-
 Section Vnth.
 
+  Variable A : Type.  
+
   Program Fixpoint Vnth n (v : vector A n) : dom_lt n -> A :=
     match v with
     | Vnil => 
@@ -41,6 +38,8 @@ End Vnth.
 
 Section Vbuild.
 
+  Variable A : Type.
+
   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
@@ -62,7 +61,7 @@ Section Vbuild.
   Qed.
   Next Obligation.
     destruct_call Vbuild_spec. simpl.
-    destruct n0. discriminate.
+    destruct n. discriminate.
     inversion Heq_n. subst.
     destruct ip.
     simplify_eqs. destruct x0. unfold dom_build. pi.
@@ -71,12 +70,17 @@ Section Vbuild.
 
   Program Definition Vbuild n gen : vector A n := Vbuild_spec gen.
 
+  Lemma Vnth_Vbuild n (i : dom_lt n) gen : Vnth (Vbuild gen) i = gen i.
+  Proof.
+  Admitted.
+
 End Vbuild.
 
 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
@@ -87,20 +91,31 @@ End vec_of_list.
 
 Section Vforall2.
 
-  Variable R : A -> A -> Prop.
+  Variable A B : Type.
+  Variable R : A -> B -> Prop.
 
-  Fixpoint Vforall2_aux n1 (v1 : vector A n1) n2 (v2 : vector A n2) {struct v1} : Prop :=
+  Fixpoint Vforall2_aux n1 (v1 : vector A n1) n2 (v2 : vector B 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.
+  Definition Vforall2 n (v1 : vector A n) (v2 : vector B n) := Vforall2_aux v1 v2.
 
-End Vforall2.
+  Lemma Vforall2_elim n (v1 : vector A n) (v2 : vector B n) : 
+    Vforall2 v1 v2 -> 
+    forall ip, R (Vnth v1 ip) (Vnth v2 ip).
+  Proof.
+  Admitted.
+
+  Lemma Vforall2_intro n (v1 : vector A n) (v2 : vector B n) : 
+    (forall ip, R (Vnth v1 ip) (Vnth v2 ip)) ->
+    Vforall2 v1 v2.
+  Proof.
+  Admitted.
 
-End vector.
+End Vforall2.
 
 Section VCheck_n.
 
@@ -129,4 +144,9 @@ Section VCheck_n.
     omega.
   Qed.
 
+  Lemma Vcheck_n_holds : 
+    (forall (ip : dom_lt n), P ip) -> Vcheck_n.
+  Proof.
+  Admitted.
+
 End VCheck_n.