proposition: Lemma denot_while_min: forall b c F, (forall s, F s = if beval b s then bind (denot c s) F else Some s) -> (forall s, denot (WHILE b c) s <<= F s).
proof: Proof. intros b c F EQ. assert (REC: forall n s, cinterp n (WHILE b c) s <<= F s). { induction n as [ | n]; intros; cbn. - auto with lessdef. - rewrite EQ. destruct (beval b s); auto with lessdef. apply bind_mono; auto with lessdef. destruct (denot_eq c s n) as [E|E]; rewrite E; auto using lessdef_refl with lessdef. } intros. destruct (denot_charact (WHILE b c) s) as (i & LIM). rewrite <- (LIM i) by lia. apply REC. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)