Prove non-strictly increasing

common/union_unary.mlw

+module Union
+  use int.Int
+  use bool.Bool
+  use option.Option
+  use interval.Bound
+  use real.RealInfix
+
+  use union.Union
+  import Make
+
+   type unary = {
+    uq: Q.t -> Q.t;
+    ghost ur: real -> real;
+    (* uq_left: Q.t -> (Bound.t,Q.t); *)
+    (* uq_right: Q.t -> (Bound.t,Q.t); *)
+    (* ghost ur_left: real -> Bound.t; *)
+    (* ghost ur_right: real -> Bound.t; *)
+   }
+   invariant { forall v:Q.t. (ur v) = (uq v) }
+   by {
+      ur  = (fun r -> r);
+      uq = (fun q -> q);
+      (* uq = (fun q -> Strict,q,Strict); *)
+      (* ur_left = (fun _ -> Strict); *)
+      (* ur_right = (fun _ -> Strict); *)
+   }
+
+   (** unary non-strict increasing *)
+   predicate nsi1 (op:unary) =
+       (forall v v' [op.ur v,op.ur v']. v  <. v' -> (op.ur v) <=. (op.ur v'))
+
+  lemma nsi1_cmp: forall op[nsi1 op]. nsi1 op ->
+      (forall v v' b. cmp v b v' -> cmp (op.ur v) Large (op.ur v'))
+
+   let rec op_nsi1_sin start (ghost rstart:real) if_ op (l:t'') : t''
+     requires { ordered' l }
+     requires { nsi1 op }
+     requires { lt_bound' rstart l }
+     requires { op.ur rstart = start } 
+     ensures { ordered' result }
+     ensures { forall q. q <. start -> (lt_bound' q result) }
+     ensures { forall q. (mem_if if_ q l) -> rstart <=. q -> mem_if False (op.ur q) result }
+     ensures { mem_if False start result }
+     variant { length' l }
+    =
+      match l with
+      | Sin q l' ->
+         let qop = (op.uq q) in
+         if Q.(start = qop)
+         then op_nsi1_sin start rstart if_ op l'
+         else if if_
+         then begin
+           End start Large (op_nsi1_wait if_ op l')
+         end
+         else Sin start (op_nsi1_sin qop (Q.real q) if_ op l')
+      | End q bv l' ->
+(*        assert { forall p. cmp q bv p = cmp (op.ur q) Large (op.ur p) };*)
+        let qop = (op.uq q) in
+        if Q.(start = qop) then op_nsi1_sin start rstart (notb if_) op l'
+        else if if_ then
+          End start Large (op_nsi1_inter qop (Q.real q) op l')
+        else
+          Sin start (op_nsi1_sin qop (Q.real q) (notb if_) op l')
+      | Inf -> if if_ then End start Large Inf else Sin start Inf 
+      end
+  with op_nsi1_inter stop (ghost rstop:real) op (l:t'') : t''
+     requires { ordered' l }
+     requires { nsi1 op }
+     requires { lt_bound' rstop l }
+     requires { op.ur rstop = stop }
+     ensures { ordered' result }
+     ensures { forall q. q <. stop -> (lt_bound' q result) }
+     ensures { forall q. (mem_if False q l) -> mem_if True (op.ur q) result }
+     ensures { forall q. q <=. stop -> mem_if True q result }
+     variant { length' l }
+    =
+      match l with
+      | Sin q l' ->
+         let qop = (op.uq q) in
+         if Q.(stop = qop)
+         then op_nsi1_inter stop (Q.real q) op l'
+         else
+            End stop Strict (op_nsi1_sin qop (Q.real q) False op l')
+      | End q bv l' ->
+(*        assert { forall p. cmp q bv p = cmp (op.ur q) Large (op.ur p) };*)
+        let qop = (op.uq q) in
+        if Q.(stop = qop) then op_nsi1_wait True op l'
+        else
+          End stop Strict (op_nsi1_sin qop (Q.real q) True op l')
+      | Inf -> End stop Strict Inf
+      end
+  with op_nsi1_wait if_ op (l:t'') : t''
+     requires { ordered' l }
+     requires { nsi1 op }
+     ensures { ordered' result }
+     ensures { forall q q'. (lt_bound' q l) -> q' <. op.ur q -> (lt_bound' q' result) }
+     ensures { forall q. (mem_if if_ q l) -> mem_if if_ (op.ur q) result }
+     variant { length' l }
+    =
+      match l with
+      | Sin q l' ->
+         let qop = (op.uq q) in
+         if if_ then op_nsi1_wait if_ op l'
+         else op_nsi1_sin qop (Q.real q) False op l'
+      | End q bv l' ->
+        (*assert { forall p. cmp q bv p = cmp (op.ur q) Large (op.ur p) };*)
+        let qop = (op.uq q) in
+         if if_ then op_nsi1_inter qop (Q.real q) op l'
+         else op_nsi1_sin qop (Q.real q) True op l'
+      | Inf -> Inf
+      end
+
+
+
+  let op_nsi1_cst (op:unary) l
+    requires { nsi1 op }
+    ensures {
+       forall q. (mem q l.a) -> mem (op.ur q) result.a
+     }
+   =
+     match l.a with
+     | On l ->
+       { a = On (op_nsi1_wait True op l) }
+     | Off l ->
+        let v = not_bottom' False l in
+        let l = (op_nsi1_wait False op l) in
+        assert { mem_if False (op.ur v) l };
+       { a = Off l }
+    end
+
+   (** unary stricly decreasing *)
+   predicate sd1 (op:unary) =
+       (forall v v' [op.ur v,op.ur v']. v <. v' -> op.ur v' <. op.ur v)
+
+   predicate first_bound' (x:real) (l:t'') =
+     match l with
+     | Sin q _ -> x = q
+     | End q _ _ -> x = q
+     | Inf -> true
+     end
+
+   let rec ghost smaller_first_bound (x:real) (y:real) (m:t'')
+      requires { x <. y }
+      requires { first_bound' y m }
+      requires { ordered' m }
+      ensures { lt_bound' x m }
+      variant { m } =
+      match m with
+      | Sin q m ->
+        smaller_lt_bound x (Q.real q) m
+      | End q _ m ->
+        smaller_lt_bound x (Q.real q) m
+      | Inf -> ()
+      end
+
+
+
+   let rec op_sd1_cst' op (l:t'') (acc:t'') if_ (ghost curr:real) (ghost orig: t) : t
+     requires { sd1 op }
+     requires { ordered' l }
+     requires { ordered' acc }
+     requires { lt_bound' curr l }
+     requires { first_bound' (op.ur curr) acc }
+     requires  { forall q. (mem q orig.a) -> (if curr <. q then mem_if if_ q l else mem_if if_ (op.ur q) acc) }
+ (*    ensures { forall q. (lt_bound' q l) -> (lt_bound' (op q) result) }
+     ensures { forall q. (mem_if if_ q l) -> mem_if if_ (op q) result }   *)
+     ensures  { forall q. (mem q orig.a) -> mem (op.ur q) result.a }
+     variant { length' l }
+    =
+      match l with
+      | Sin q l' ->
+        smaller_first_bound pure {op.ur q} pure {op.ur curr} acc;
+       op_sd1_cst' op l' (Sin (op.uq q) acc) if_ (Q.real q) orig
+      | End q bv l' ->
+        assert { forall p. cmp q bv p = cmp (op.ur p) bv (op.ur q) };
+        smaller_first_bound pure {op.ur q} pure {op.ur curr} acc;
+        op_sd1_cst' op l' (End (op.uq q) (inv_bound bv) acc) (notb if_) (Q.real q) orig
+      | Inf -> if if_ then { a = On acc } else begin
+         let v = not_bottom orig in
+         assert { mem_if False (op.ur v) acc };
+         { a = Off acc }
+         end
+      end
+
+  let op_sd1_cst op l
+    requires { sd1 op }
+    ensures {
+       forall q. (mem q l.a) -> mem (op.ur q) result.a
+     }
+   =
+     match l.a with
+     | On l' ->
+        let ghost curr = match l' with
+        | Sin q _ | End q _ _ -> let ghost r = (Q.real q) -. 1. in smaller_first_bound r (Q.real q) l'; r
+        | Inf -> 0.
+        end
+        in
+       op_sd1_cst' op l' Inf True curr l
+     | Off l' ->
+        let ghost curr = match l' with
+        | Sin q _ | End q _ _ -> let ghost r = (Q.real q) -. 1. in smaller_first_bound r (Q.real q) l'; r
+        | Inf -> 0.
+        end
+        in
+        op_sd1_cst' op l' Inf False curr l
+    end
+
+    let neg l
+       ensures { forall q. (mem q l.a) -> mem (-. q) result.a }
+     =
+       let negq (x:Q.t) ensures { result = -. x } = Q.(Q.of_int 0 - x) in
+       op_sd1_cst {ur = (fun x -> -.x); uq = negq } l
+(*
+    let mult_cst c l
+       ensures { forall q. (mem q l.a) -> mem (c *. q) result.a }
+     =
+       let fq (x:Q.t) ensures { result = c *. x } = Q.(c * x) in
+       let ghost function fr (x:real) = (Q.real c) *. x in
+       let op = { uq = fq; ur = fr } in
+       match Q.compare (Q.of_int 0) c with
+       | Ord.Eq -> singleton (Q.of_int 0)
+       | Ord.Lt -> op_si1_cst op l
+       | Ord.Gt -> op_sd1_cst op l
+       end
+  *)     
+end