proposition: Lemma chooseAction : forall trueLevel sensor r, Min sensor <= trueLevel <= Max sensor -> refine (p <- (act <- {act : action | match act with | Nothing => True | Fill => trueLevel + maxFill < tankMax | Empty => trueLevel - maxEmpty >= 0 end}; trueLevel' <- {trueLevel' : Z | minFill <= FillRate r <= maxFill -> minEmpty <= EmptyRate r <= maxEmpty -> match act with | Nothing => trueLevel' = trueLevel | Fill => trueLevel' = trueLevel + FillRate r | Empty => trueLevel' = trueLevel - EmptyRate r end}; ret (trueLevel', act)); sensor' <- {sensor' : interval | Min sensor' <= fst p <= Max sensor'}; ret (sensor', snd p)) (if (Min sensor <? TargetLevel r) && (Max sensor + maxFill <? tankMax) then ret (Interval (Min sensor + minFill) (Max sensor + maxFill), Fill) else if (Max sensor >? TargetLevel r) && (Min sensor - maxEmpty >=? 0) then ret (Interval (Min sensor - maxEmpty) (Max sensor - minEmpty), Empty) else ret (sensor, Nothing)).
proof: Proof. intros. assert ((minFill <= FillRate r <= maxFill /\ minEmpty <= EmptyRate r <= maxEmpty) \/ ~(minFill <= FillRate r <= maxFill /\ minEmpty <= EmptyRate r <= maxEmpty)) by (destruct (Z_le_gt_dec minFill (FillRate r)), (Z_le_gt_dec (FillRate r) maxFill), (Z_le_gt_dec minEmpty (EmptyRate r)), (Z_le_gt_dec (EmptyRate r) maxEmpty); omega). intuition; implement1; (simplify with monad laws; do 2 intro; repeat computes_to_inv; subst; simpl in *; solve [ econstructor; split; repeat match goal with | [ |- Ensembles.In _ _ _ ] => econstructor; split end; repeat implement; generalize fillBounds, emptyBounds; omega | econstructor; split; repeat match goal with | [ |- Ensembles.In _ _ _ ] => econstructor; split end; try match goal with | [ |- Ensembles.In _ _ {| Min := ?min; Max := _ |} ] => instantiate (1 := min) end; repeat implement; generalize fillBounds, emptyBounds; omega ]). Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Ics