proposition: Lemma chooseAction : forall trueLevel sensor targetLevel, Z.abs (sensor - trueLevel) <= sensorAccuracy -> refine (p <- (act <- {act : action | match act with | Nothing => True | Fill => trueLevel + fillRate < tankMax | Empty => trueLevel - emptyRate >= 0 end}; ret (match act with | Nothing => trueLevel | Fill => trueLevel + fillRate | Empty => trueLevel - emptyRate end, act)); sensor' <- {n : Z | Z.abs (n - fst p) <= sensorAccuracy}; ret (sensor', snd p)) (if (sensor <? targetLevel) && (sensor + sensorAccuracy + fillRate <? tankMax) then ret (sensor + fillRate, Fill) else if (sensor >? targetLevel) && (sensor - sensorAccuracy - emptyRate >=? 0) then ret (sensor - emptyRate, Empty) else ret (sensor, Nothing)).
proof: Proof. implement. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Ics