proposition: Lemma denot_while: forall b c s, denot (WHILE b c) s = if beval b s then bind (denot c s) (denot (WHILE b c)) else Some s.
proof: Proof. intros. rewrite <- denot_seq. set (c' := c ;; WHILE b c). destruct (denot_charact c' s) as (i & LIM). apply denot_unique with (S i). intros. destruct j as [ | j]. lia. cbn. destruct (beval b s). apply (LIM (S j)). lia. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)