Merge remote branch 'adam/master'

SConstruct

@@ -1,12 +1,13 @@
 import os, glob, string
 libs = os.environ["COQLIBS"]
+coqtop = os.environ["COQTOP"]
 corn_dir = libs + '/CoRN'
 color_dir = libs + '/color/color/trunk/color'
 
 Rs = [(corn_dir, 'CoRN'), (color_dir, 'CoLoR'), ('.', 'hybrid')]
 Rs = string.join(map(lambda (x,y): '-R "' + x + '" ' + y, Rs))
 
-coqc = 'coqc -noglob ' + Rs
+coqc = coqtop + '/bin/coqc -noglob ' + Rs
 
 def make_abs(s):
   if s[0] != '/': return Dir("#").abspath + "/" + s

abstract.v

@@ -5,6 +5,10 @@ Require Import Morphisms.
 Set Implicit Arguments.
 Require Import EquivDec.
 Require concrete.
+Require Import CoLoR.Util.Vector.VecUtil.
+Require Import hybrid.vector_setoid.
+Require hybrid.nat_util.
+Require Import hybrid.hlist_aux.
 
 Module c := concrete.
 
@@ -13,7 +17,7 @@ Section contents.
   Variable chs: concrete.System.
 
   Record Space: Type :=
-    { Region: Set
+    { Region: Type
     ; Region_eq_dec: EquivDec.EqDec Region eq
     ; regions: ExhaustiveList Region
     ; NoDup_regions: NoDup regions
@@ -62,23 +66,70 @@ Section contents.
     Let in_region_mor: Morphism (@cs_eq _ ==> eq ==> iff) in_region.
     Proof. unfold in_region. intros x x' e r r' e'. rewrite e, e'. split; auto. Qed.
 
-    Let regions_cover: forall (l : concrete.Location chs) (p : concrete.Point chs),
-      concrete.invariant (l, p) -> DN (sig (in_region p)).
-    Proof.
-      intros.
-      apply (DN_bind (regions_cover ap _ _ H)). intros [x i].
-      apply (DN_bind (regions_cover ap' _ _ H)). intros [x0 i0].
-      apply DN_return.
-      exists (x, x0).
-      split; assumption.
-    Qed. (* written with Program and monad notation, this should be much clearer *)
+    Program Definition regions_cover_prod l p : concrete.invariant (l, p) -> DN (sig (in_region p)) :=
+      fun H => 
+        C1 <- contents.regions_cover ap l p H;
+        C2 <- contents.regions_cover ap' l p H;
+        return [=(`C1, `C2)=].
+    Next Obligation.
+      split; crunch.
+    Qed.
 
     Definition prod_space: Space := Build_Space _ _
       (NoDup_ExhaustivePairList (NoDup_regions ap) (NoDup_regions ap'))
-      in_region_mor regions_cover.
+      in_region_mor regions_cover_prod.
 
   End prod_space.
 
+  (* We generalize the product space above from 2 to arbitrary 'n' dimensions,
+     hence generalizing abstraction by squares in 2 dimensional space to 
+     abstraction by hyper-cubes in n-dimensional space *)
+
+  Section hyper_space.
+
+    Variable n : nat.
+    Variable aps : list Space.
+
+    (* [Regions] is formed by an n-product of [Region]s of respective [Space]s,
+       epxressed with heterogenous list *)
+    Notation Regions aps := (@hlist _ Region aps).
+
+    Fixpoint in_region_aux (aps : list Space) (p : concrete.Point chs) : Regions aps -> Prop :=
+      match aps as aps return Regions aps -> Prop with
+      | [] => fun _ => True
+      | s::ss => fun rs =>
+          in_region s p (hhd rs) /\ @in_region_aux ss p (htl rs)
+      end.
+
+    Obligation Tactic := crunch.
+
+    Program Fixpoint regions_cover_aux (aps : list Space) l p : 
+      concrete.invariant (l, p) -> DN (sig (@in_region_aux aps p)) :=
+      match aps with
+      | [] => fun H => return [= HNil (H:=_) =]
+      | s::ss => fun H =>
+          C1 <- contents.regions_cover s l p H;
+          C2 <- @regions_cover_aux ss l p H;
+          return [= `C1:::`C2 =]
+      end.
+
+    Lemma in_region_aux_morph : Morphism (@st_eq _ ==> eq ==> iff) (@in_region_aux aps).
+    Proof.
+      repeat intro; split; induction aps; crunch.
+    Qed.
+
+    Obligation Tactic := program_simpl; auto with typeclass_instances.
+
+    Hint Resolve NoDup_regions.
+
+    Program Definition hyper_space : Space := @Build_Space (Regions aps) _ _ _ 
+      (@in_region_aux aps) in_region_aux_morph (@regions_cover_aux aps).
+    Next Obligation.
+      set (w := NoDup_ExhaustiveHList); simpl in w; apply w; auto.
+    Qed.
+
+  End hyper_space.
+
   Variable ap: Space.
 
   Instance abs: Container (c.State chs) (State ap) := fun s s' =>
@@ -95,7 +146,7 @@ Section contents.
 
   End CoverRelandsuch.
 
-  Definition CompleteCoverList (cs: c.State chs -> Prop): Set :=
+  Definition CompleteCoverList (cs: c.State chs -> Prop): Type :=
     sig (LazyProp ∘ (CompleteCover cs: list (State ap) -> Prop)).
 
   Section safe.
@@ -145,7 +196,7 @@ Section contents.
   Definition cont_trans (l: c.Location chs): relation (Region ap)
     := fun r r' => exists p q, p ∈ r /\ q ∈ r' /\ c.can_flow chs l p q.
 
-  Definition sharing_transition_overestimator (R: relation (concrete.State chs)): Set :=
+  Definition sharing_transition_overestimator (R: relation (concrete.State chs)): Type :=
     forall s: State ap, sig (fun l: list (State ap) => LazyProp (NoDup l /\
       SharedCover (concrete.invariant ∩ (overlap s ∘ util.flip R)) l)).
         (* the invariant part is important because it means the overestimators can use

abstract_as_graph.v

@@ -14,7 +14,7 @@ Section using_duplication.
     (ap: abstract.Space chs)
     (ahs: abstract.System ap).
 
-  Let Vertex := bool * abstract.State ap.
+  Let Vertex : Type := bool * abstract.State ap.
 
   Definition nexts (v: Vertex): list (abstract.State ap) :=
     let (k, s) := v in

decreasing_exponential_flow.v

@@ -474,3 +474,5 @@ Section contents.
   Qed.
 
 End contents.
+
+Hint Resolve inv_correct.

digraph.v

@@ -4,7 +4,7 @@ Require EquivDec.
 Set Implicit Arguments.
 
 Record DiGraph: Type := Build
-  { Vertex: Set
+  { Vertex: Type
   ; Vertex_eq_dec: EquivDec.EqDec Vertex eq
   ; vertices: ExhaustiveList Vertex
   ; edges: Vertex -> list Vertex
@@ -29,7 +29,7 @@ Section reachability.
   Definition edge: relation (Vertex g) := fun v w => In w (edges v).
   Let ved := Vertex_eq_dec g.
 
-  Definition Edge: Set := (Vertex g * Vertex g)%type.
+  Definition Edge := (Vertex g * Vertex g)%type.
   Definition Edge_eq_dec: forall (e e': Edge), decision (e=e')
     := pair_eq_dec ved ved.
 

examples/room_heating/abs.v

@@ -0,0 +1,33 @@
+Require Import hybrid.tactics.
+Require Import hybrid.abstract.
+Require Import hybrid.geometry.
+Require Import hybrid.square_abstraction.
+Require Import hybrid.flow.
+
+Require Import hybrid.examples.room_heating.conc.
+
+Set Implicit Arguments.
+
+Local Open Scope CR_scope.
+Local Open Scope vec_scope.
+
+Module RoomHeatingAbstract (Import RHS : RoomHeatingSpec).
+
+  Module Import conc := RoomHeatingConcrete RHS.
+
+  Definition two_pos: CRpos ('2) := positive_CRpos 2.
+
+  Definition room_flow_inv (rs : RoomState) : OpenRange -> OpenRange -> OpenRange :=
+    match rs with
+    | HeaterOn => flow.scale.inv two_pos (square_flow_conditions.one_axis.flow_range
+      _ flow.positive_linear.inv_correct flow.positive_linear.mono)
+    | HeaterOff
+    | NoHeater => decreasing_exponential_flow.inv milli
+    end.
+
+  Lemma room_flow_ok l : range_flow_inv_spec (room_flow l) (room_flow_inv l).
+  Proof with auto.
+    destruct l; crunch.
+  Qed.
+
+End RoomHeatingAbstract.

examples/room_heating/conc.v

@@ -3,6 +3,7 @@ Require  Coq.Program.Program.
 Require Import CoRN.reals.fast.CRln.
 
 Require Export hybrid.examples.room_heating.params.
+Require Import hybrid.tactics.
 Require Import hybrid.util.
 Require Import hybrid.c_util.
 Require Import hybrid.nat_util.
@@ -64,7 +65,7 @@ Module RoomHeatingConcrete (Import RHS : RoomHeatingSpec).
   Lemma exhaustiveRS_correct x : In x (exhaustiveRS n).
   Proof with auto.
     induction x.
-    left. ref.
+    crunch.
     simpl. destruct a; in_or_app_proof.
   Qed.
 
@@ -207,7 +208,10 @@ Module RoomHeatingConcrete (Import RHS : RoomHeatingSpec).
   Definition flow (l : DS) := vector_flow (Vmap room_flow l).
 
   Lemma invariant_stable s: Stable (invariant s).
-  Admitted.
+  Proof.
+    intros. apply check_n_Stable.
+    intros. destruct (ds s) [@ip]; crunch.
+  Qed.
 
   Definition concrete_system: concrete.System :=
     concrete.Build_System _ _ NoDup_locations

examples/thermostat/abs.v

@@ -3,6 +3,7 @@ Require Import geometry.
 Require Import monotonic_flow.
 Require Import hs_solver.
 Require Import interval_spec.
+Require Import tactics.
 Require decreasing_exponential_flow.
 Require abstract square_abstraction.
 Require EquivDec.
@@ -32,22 +33,16 @@ Definition temp_flow_inv (l: Location): OpenRange -> OpenRange -> OpenRange :=
   | Check => flow.scale.inv half_pos (dec_exp_flow.inv milli)
   end.
 
+Hint Resolve square_flow_conditions.one_axis.flow_range_covers.
+
 Lemma clock_rfis l: range_flow_inv_spec (clock_flow l) (clock_flow_inv l).
-Proof with auto.
-  intro.
-  unfold range_flow_inv_spec. intros.
-  apply square_flow_conditions.one_axis.flow_range_covers with p...
+Proof.
+  unfold clock_flow_inv; crunch.
 Qed.
 
 Lemma temp_rfis l: range_flow_inv_spec (temp_flow l) (temp_flow_inv l).
-Proof with auto.
-  destruct l; simpl temp_flow.
-      unfold temp_flow_inv.
-      apply flow.scale.inv_correct.
-      unfold range_flow_inv_spec. intros.
-      apply square_flow_conditions.one_axis.flow_range_covers with p...
-    apply dec_exp_flow.inv_correct.
-  apply flow.scale.inv_correct, dec_exp_flow.inv_correct.
+Proof. 
+  destruct l; crunch.
 Qed.
 
 (* Abstract regions: *)

flow.v

@@ -22,13 +22,14 @@ Record Flow (X: CSetoid): Type :=
   }.
 
 Definition mono (f: Flow CRasCSetoid): Type :=
-  sum (forall x, strongly_increasing (f x))
-    (forall x, strongly_decreasing (f x)).
+  ((forall x, strongly_increasing (f x)) + (forall x, strongly_decreasing (f x)))%type.
 
 Definition range_flow_inv_spec (f: Flow CRasCSetoid)
   (i: OpenRange -> OpenRange -> OpenRange): Prop :=
     forall a p, in_orange a p -> forall b t, in_orange b (f p t) -> in_orange (i a b) t.
 
+Hint Unfold range_flow_inv_spec.
+
 Obligation Tactic := idtac.
 
 Program Definition product_flow (X Y: CSetoid) (fx: Flow X) (fy: Flow Y):
@@ -149,7 +150,7 @@ Section contents.
 End contents.
 End scale.
 
-Hint Resolve scale.inc.
+Hint Resolve scale.inc scale.inv_correct.
 
 Module positive_linear.
 Section contents.