Use stability and double negation arguments in c_util to remove uses …

…of trichotomy axiom, which thermostat safety now no longer depends upon.

Ignore-this: f14444df04fdd8e334d08d22d79d322c

darcs-hash:20090701143257-bab43-fb475725f17581e182324fc508496f0b1504a953.gz

c_util.v

@@ -1,4 +1,4 @@
-Require Import util.
+Require Import util stability.
 Require Export CRsign.
 Require Export CRln.
 Require Import CRexp.
@@ -991,7 +991,9 @@ Section function_properties.
   Proof with auto.
     unfold strongly_increasing.
     intros.
-    destruct (CR_lt_eq_dec x x').
+    apply (CRle_stable x x').
+    apply (DN_fmap (CR_trichotomy x x')); intro.
+    destruct H0.
       rewrite s.
       apply CRle_refl.
     destruct s.
@@ -1025,7 +1027,9 @@ Section function_properties.
   Proof with auto.
     unfold strongly_increasing.
     intros.
-    destruct (CR_lt_eq_dec x x').
+    apply (CRle_stable x' x).
+    apply (DN_fmap (CR_trichotomy x x')). intro.
+    destruct H0.
       rewrite s.
       apply CRle_refl.
     destruct s.
@@ -1040,7 +1044,9 @@ Section function_properties.
     strongly_increasing -> forall x x', x <= x' -> f x <= f x'.
   Proof with auto.
     intros.
-    destruct (CR_lt_eq_dec x x').
+    apply (CRle_stable (f x) (f x')).
+    apply (DN_fmap (CR_trichotomy x x')). intro.
+    destruct H0.
       rewrite (f_wd s).
       apply CRle_refl.
     destruct s.
@@ -1054,7 +1060,9 @@ Section function_properties.
     strongly_decreasing -> forall x x', x <= x' -> f x' <= f x.
   Proof with auto.
     intros.
-    destruct (CR_lt_eq_dec x x').
+    apply (CRle_stable (f x') (f x)).
+    apply (DN_fmap (CR_trichotomy x x')). intro.
+    destruct H0.
       rewrite (f_wd s).
       apply CRle_refl.
     destruct s.
@@ -1074,7 +1082,9 @@ Section function_properties.
     intros.
     split.
       intros.
-      destruct (CR_lt_eq_dec x x')...
+      apply (CReq_stable x x').
+      apply (DN_fmap (CR_trichotomy x x')). intro.
+      destruct H0...
       elimtype False.
       destruct s; destruct X.
             set (s _ _ c).

stability.v

@@ -62,6 +62,24 @@ Proof. unfold CRle. auto. Qed.
 
 Hint Resolve CRle_stable.
 
+Lemma CReq_stable (x y: CR): Stable (x == y)%CR.
+  intros.
+  constructor.
+  intro.
+  apply <- (CRle_def x y).
+  split.
+    apply (CRle_stable x y).
+    apply (DN_fmap H).
+    intro.
+    rewrite H0.
+    apply CRle_refl.
+  apply (CRle_stable y x).
+  apply (DN_fmap H).
+  intro.
+  rewrite H0.
+  apply CRle_refl.
+Qed. (* Todo: This is a ridiculous proof. Make a sane one! *)
+
 Lemma stable_conjunction (A B: Prop): Stable A -> Stable B -> Stable (A /\ B).
 Proof. firstorder. Qed.
 
@@ -100,7 +118,7 @@ Lemma CRle_lt_dec x y: DN ((x <= y) + (y < x)).
   apply CRle_refl.
 Qed.
 
-Lemma CR_trichotomy x y: DN ((x == y) + (x < y) + (y < x)).
+Lemma CR_trichotomy x y: DN ((x == y) + ((x < y) + (y < x))).
 Proof with auto.
   intros.
   apply (DN_bind (CRle_dec x y)).