proposition: Lemma measure_map_le: forall m1 m2, (forall x, V.measure (get x (Top_except m1)) <= V.measure (get x (Top_except m2)))%nat -> (measure_map m1 <= measure_map m2)%nat.
proof: Proof. intros m0. pattern m0. unfold measure_map at 1; apply IMProp.fold_rec. - intros m EMPTY m2 LE. lia. - intros x v1 n m' m'' MAP NOTIN ADD REC m2 LE. set (m2' := IdentMap.remove x m2). assert (LE': forall x, (V.measure (get x (Top_except m')) <= V.measure (get x (Top_except m2')))%nat). { intros y. generalize (LE y). unfold get, m2'. rewrite ADD, IMFact.add_o, IMFact.remove_o. destruct (AbstrInterp.IdentMap.E.eq_dec x y). + subst y. apply IMFact.not_find_in_iff in NOTIN. rewrite NOTIN. rewrite ! V.measure_top. lia. + auto. } apply REC in LE'. rewrite (measure_map_remove m2 x). fold m2'. specialize (LE x). unfold get at 1 in LE. rewrite ADD, IMFact.add_eq_o in LE by auto. lia. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)