proposition: Lemma measure_widen_lt: forall m1 m2, ble (Top_except m2) (Top_except m1) = false -> (measure_map (IdentMap.map2 widen_aux m1 m2) < measure_map m1)%nat.
proof: Proof. intros. apply ble_false in H. 2: congruence. destruct H as (x & BL). apply measure_map_lt. - intros y. unfold get. rewrite IMFact.map2_1bis by auto. unfold widen_aux. destruct (IdentMap.find y m1) as [ v1 |]. destruct (IdentMap.find y m2) as [ v2 |]. apply V.widen_2. rewrite V.measure_top; lia. rewrite V.measure_top; lia. - exists x. unfold get in *. rewrite IMFact.map2_1bis by auto. unfold widen_aux. destruct (IdentMap.find x m1) as [ v1 |]. destruct (IdentMap.find x m2) as [ v2 |]. apply V.widen_3 in BL; auto. apply V.widen_3 in BL; rewrite V.measure_top; lia. assert (T: forall z, V.ble z V.top = true). { intros. apply V.ble_2. red; intros. apply V.top_1. } rewrite T in BL. congruence. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)