Make examples/thermostat/safe compile with current Coq/CoRN/CoLoR.

SConstruct

@@ -2,9 +2,10 @@ import os, glob, string
 libs = os.environ["COQLIBS"]
 coqtop = os.environ["COQTOP"]
 corn_dir = libs + '/CoRN'
-color_dir = libs + '/color/color/trunk/color'
+color_dir = libs + '/color'
+mathclasses_dir = corn_dir + '/math-classes/src'
 
-Rs = [(corn_dir, 'CoRN'), (color_dir, 'CoLoR'), ('.', 'hybrid')]
+Rs = [(corn_dir, 'CoRN'), (mathclasses_dir, 'MathClasses'), (color_dir, 'CoLoR'), ('.', 'hybrid')]
 Rs = string.join(map(lambda (x,y): '-R "' + x + '" ' + y, Rs))
 
 coqc = coqtop + '/bin/coqc -noglob ' + Rs
@@ -14,7 +15,8 @@ def make_abs(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:])
+  return map(make_abs, os.popen("coqdep -I . " + Rs + " -w " + str(node) + " 2> /dev/null").read().strip().split(':')[1].strip().split(' ')[1:])
+    # todo: this is a hack. use CoRN's approach
 
 env = DefaultEnvironment(ENV = os.environ)
 env.Append(BUILDERS = {'Coq' : Builder(action = coqc + ' $SOURCE', suffix = '.vo', src_suffix = '.v')})

abstract.v

@@ -1,3 +1,5 @@
+Set Automatic Coercions Import.
+
 Require Import List Bool.
 Require Import util list_util stability containers.
 Require Import CSetoids.
@@ -22,7 +24,7 @@ Section contents.
     ; regions: ExhaustiveList Region
     ; NoDup_regions: NoDup regions
     ; in_region: Container (concrete.Point chs) Region
-    ; in_region_mor: Morphism (@cs_eq _ ==> eq ==> iff) in_region
+    ; in_region_mor: Proper (@cs_eq _ ==> eq ==> iff) in_region
     ; regions_cover: forall l p, c.invariant (l, p) -> DN (sig (in_region p))
     }.
 
@@ -63,7 +65,7 @@ Section contents.
 
     Let in_region p r := in_region ap p (fst r) /\ in_region ap' p (snd r).
 
-    Let in_region_mor: Morphism (@cs_eq _ ==> eq ==> iff) in_region.
+    Let in_region_mor: Proper (@cs_eq _ ==> eq ==> iff) in_region.
     Proof. unfold in_region. intros x x' e r r' e'. rewrite e, e'. split; auto. Qed.
 
     Program Definition regions_cover_prod l p : concrete.invariant (l, p) -> DN (sig (in_region p)) :=
@@ -113,9 +115,16 @@ Section contents.
           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.
+    Lemma in_region_aux_morph : Proper (@st_eq _ ==> eq ==> iff) (@in_region_aux aps).
+    Proof with auto.
+      repeat intro.
+      subst.
+      induction aps. firstorder.
+      split; intros [H0 H1]; split.
+            apply (in_region_mor a x y H (refl_equal _))...
+          apply IHl...
+        apply (in_region_mor a x y H (refl_equal _))...
+      apply IHl...
     Qed.
 
     Obligation Tactic := program_simpl; auto with typeclass_instances.
@@ -183,10 +192,11 @@ Section contents.
       @overestimate (exists u, In u (proj1_sig astates) /\ reachable u) overestimate.
 
     Next Obligation. Proof with eauto.
-      intros H0 [x [Px r]].
+      intros [x [Px r]].
       apply (@safe x)...
       repeat intro.
-      apply (overestimation_false _ H0)...
+      apply (@overestimation_false (exists u, In u (proj1_sig astates) /\ reachable u) _ H0)...
+        (* todo: ugly *)
       destruct astates.
       pose proof (c ())...
     Qed.
@@ -233,7 +243,7 @@ Section contents.
       DN (exists is, overestimation_bool (initial_dec ahs is) = true /\
         exists s', s ∈ s' /\ end_with trans (negb b) is s').
   Proof with eauto; auto 20.
-    intros i s H b H0.
+    intros H b H0.
     induction H0 as [| b i (l, p) H0 IH [l' p']].
       destruct s as [l cp].
       apply (DN_fmap (regions_cover ap l cp (concrete.invariant_initial chs _ H))).

abstract_as_graph.v

@@ -25,6 +25,7 @@ Section using_duplication.
 
   Lemma NoDup_edges v: NoDup (edges v).
   Proof with auto; try congruence.
+    revert v.
     intros [k [l r]].
     apply NoDup_map...
     unfold nexts.
@@ -38,7 +39,8 @@ Section using_duplication.
 
   Lemma edges_match_transitions y b x: In y (nexts (b, x)) <-> abstract.trans ahs b x y.
   Proof with auto.
-    intros [l' r'] b [l r]. simpl.
+    destruct y as [l' r'].
+    destruct x as [l r]. simpl.
     split; destruct b...
   Qed.
 
@@ -127,28 +129,38 @@ Section using_duplication.
   Program Let reachable_verts := digraph.reachables g NoDup_init_verts.
     (* Having this as a separate definition is critical for efficiency. *)
 
-  Program Let state_reachable: decider (abstract.reachable ahs) :=
-    fun s => @equivalent_decision (exists b, In (b, s) (`reachable_verts)) _ _ decide.
-
   Hint Resolve in_filter.
 
-  Next Obligation. Proof with eauto.
+  Definition state_reachable: decider (abstract.reachable ahs).
+  Proof with auto.
+   intro s.
+   simpl.
+   apply (@equivalent_decision (exists b, In (b, s) (`reachable_verts))).
     split.
-      intros [x H].
-      destruct reachable_verts.
-      apply <- respect.
-      exists x.
-      apply -> i...
+     intros [x H].
+     destruct reachable_verts.
+     apply <- respect.
+     exists x.
+     apply -> i...
     intro.
     apply respect in H.
     destruct H.
     destruct H.
     exists x.
-    destruct reachable_verts.
+    destruct @reachable_verts.
     simpl proj1_sig.
     apply <- i.
     unfold digraph.reachable...
-  Qed.
+    eauto.
+   apply (@decide_exists bool _ _).
+   intros.
+   apply (@In_decision _ _ _).
+   (* todo: this last goal is just instance resolution but it appears to diverge *)
+  Defined.
+
+(*  Program Let state_reachable: decider (abstract.reachable ahs) :=
+    fun s => @equivalent_decision (exists b, In (b, s) (`reachable_verts)) _ _ decide.
+*)
 
   Definition some_reachable := abstract.some_reachable_2 (decider_to_overestimator _ state_reachable).
 

abstract_cont_trans_over.v

@@ -1,3 +1,5 @@
+Set Automatic Coercions Import.
+
 Require Import List.
 Require Import c_util util list_util stability containers.
 Require Import CSetoids CRreal.
@@ -61,7 +63,7 @@ Section contents.
 
   Definition redundant (l: c.Location chs) (r r': abstract.Region ap) (H: r <> r'): Prop :=
     forall p, p ∈ r ->
-      forall t, '0 <= t -> concrete.flow chs l p t ∈ r' ->
+      forall t, 0 <= t -> concrete.flow chs l p t ∈ r' ->
         concrete.flow chs l p t ∈ r.
 
   Variable under_redundant: underestimator redundant.
@@ -71,7 +73,7 @@ Section contents.
    inequality is integrated in the optionality: *)
 
   Definition hints (l: c.Location chs) (r r': abstract.Region ap):
-    option (forall p, p ∈ r -> forall t, '0 <= t -> concrete.flow chs l p t ∈ r' -> concrete.flow chs l p t ∈ r) :=
+    option (forall p, p ∈ r -> forall t, 0 <= t -> concrete.flow chs l p t ∈ r' -> concrete.flow chs l p t ∈ r) :=
     match r == r' with
     | left _ => None
     | right E => under_redundant l E
@@ -83,7 +85,7 @@ Section contents.
   Hint Unfold abstract.cont_trans.
 
   Next Obligation. Proof with eauto 20.
-    intros l r r' H [x [x0 [H0 [H1 [H2 H3]]]]].
+    intros [x [x0 [H0 [H1 [H2 H3]]]]].
     apply andb_false_elim in H.
     destruct H.
       apply overestimation_false in e...
@@ -125,7 +127,7 @@ Section contents.
 
   Definition strong_redundant l (r r': a.Region ap) (H: r <> r'): Prop :=
     forall p: c.Point chs, p ∈ r ->
-      forall t: Time, concrete.flow chs l p t ∈ r' -> t <= '0.
+      forall t: Time, concrete.flow chs l p t ∈ r' -> t <= 0.
 
   (* Whereas Hint merely says that the destination point lies in the source region,
    StrongHint says that the flow duration is nonpositive. Since flow durations
@@ -139,7 +141,7 @@ Section contents.
   Lemma weaken_hint l r r' (H: r <> r'): strong_redundant l H -> redundant l H.
   Proof with eauto.
     repeat intro.
-    assert (t [=] '0). apply (CRle_def t ('0))...
+    assert (t [=] 0). apply (CRle_def t 0)...
     rewrite H4, flow_zero...
   Qed.
 

bnat.v

@@ -35,6 +35,7 @@ Section alt_rect.
 End alt_rect.
 
 Lemma bnat_cases n (x: bnat (S n)): { p | x = bS p } + { x = bO n }.
+  revert n x.
   apply bnat_Srect; [right | left; exists b]; reflexivity.
 Defined.