diff --git a/SConstruct b/SConstruct index de936d7..e7fdf38 100644 --- a/SConstruct +++ b/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)) diff --git a/bool_util.v b/bool_util.v index 9e86aa2..3a02fce 100644 --- a/bool_util.v +++ b/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 -> diff --git a/room_heating.v b/room_heating.v index 8a1900d..96dad3d 100644 --- a/room_heating.v +++ b/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]]). diff --git a/vec_util.v b/vec_util.v deleted file mode 100644 index 2f5dd3f..0000000 --- a/vec_util.v +++ /dev/null @@ -1,169 +0,0 @@ -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. - - Variable A : Type. - - Program Fixpoint Vnth n (v : vector A n) : dom_lt n -> A := - match v with - | Vnil => - fun ip => ! - | Vcons x p v' => - 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 H. - Qed. - Next Obligation. - Proof. - destruct ip. simpl in *. subst. auto with arith. - Qed. - -End Vnth. - -Notation "v '[[' p ']]'" := (Vnth v p) (at level 50) : vec_scope. - -Delimit Scope vec_scope with vec. -Local Open Scope vec_scope. - -Section Vmap. - - Variables (A B : Type) (f : A -> B). - - Fixpoint Vmap n (v : vector A n) {struct v} : vector B n := - match v with - | Vnil => Vnil - | Vcons a _ v' => Vcons (f a) (Vmap v') - end. - -End Vmap. - -Section Vbuild. - - Variable A : Type. - - Program Fixpoint Vbuild_spec n (gen : dom_lt n -> A) : - { v : vector A n | forall (ip : dom_lt n), v[[ip]] = gen ip } := - match n with - | 0 => Vnil - | S p => - 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. - destruct ip. elimtype False. subst. omega. - Qed. - Next Obligation. - destruct ip. simpl. omega. - Qed. - Next Obligation. - omega. - Qed. - Next Obligation. - destruct_call Vbuild_spec. simpl. - destruct n. discriminate. - inversion Heq_n. subst. - 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. - - 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 - | cons x m => Vcons x (vec_of_list m) - end. - -End vec_of_list. - -Section Vforall2. - - Variable A B : Type. - Variable R : A -> B -> 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 : vector A n) (v2 : vector B n) := Vforall2_aux v1 v2. - - 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 Vforall2. - -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. - - Lemma Vcheck_n_holds : - (forall (ip : dom_lt n), P ip) -> Vcheck_n. - Proof. - Admitted. - -End VCheck_n.