proposition: Lemma ble_false: forall s1 s2, s2 <> Bot -> ble s1 s2 = false -> exists x, V.ble (get x s1) (get x s2) = false.
proof: Proof. unfold ble; intros. destruct s1 as [ | m1]. discriminate. destruct s2 as [ | m2]. congruence. - set (p := fun (x: IdentMap.key) v => V.ble (get x (Top_except m1)) v) in *. set (m' := IMProp.filter (fun x v => negb (p x v)) m2). destruct (IdentMap.elements m') as [ | [x1 v1] l1] eqn:ELT. + assert (IMProp.for_all p m2 = true). { apply IMProp.for_all_iff. repeat (hnf; intros). congruence. intros. destruct (p k e) eqn:P; auto. assert (M: IdentMap.MapsTo k e m'). { apply IMProp.filter_iff. repeat (hnf; intros). congruence. rewrite P; auto. } apply IdentMap.elements_1 in M. rewrite ELT in M. inversion M. } congruence. + assert (M: IdentMap.MapsTo x1 v1 m'). { apply IdentMap.elements_2. rewrite ELT. constructor. hnf; auto. } apply IMProp.filter_iff in M. destruct M as [M N]. apply negb_true_iff in N. exists x1. unfold get at 2. erewrite IdentMap.find_1 by eauto. exact N. repeat (hnf; intros). congruence. Qed.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)