proposition: Lemma pre_from_elements_spec : forall A l (m : S.t A), NoDupA (X.eq@@1)%signature l -> (forall xv, InA (X.eq@@1)%signature xv l -> S.In (fst xv) m -> False) -> forall x v, S.find x (fold_left (fun acc xv => S.add (fst xv) (snd xv) acc) l m) = Some v <-> InA (X.eq * eq)%signature (x, v) l ∨ ¬InA (X.eq@@1)%signature (x, v) l ∧ S.find x m = Some v.
proof: Proof. intros A l. induction l as [| [y v'] l]; intros m Hl Hdiff x v; simpl. * do 2 rewrite InA_nil. tauto. * inversion_clear Hl. rewrite IHl; trivial; clear IHl. + split; intros [Hin | Hin]. - left. right. assumption. - { destruct (X.eq_dec x y) as [Heq | Heq]. * do 2 left. split; trivial. hnf; simpl. symmetry in Heq. eapply S.add_1, S.find_1 in Heq. destruct Hin as [_ Hin]. rewrite Heq in Hin. inversion Hin. reflexivity. * destruct Hin as [Hin Hm]. right. split. + intro Habs. inversion_clear Habs. - apply Heq. assumption. - contradiction. + apply S.find_2, S.add_3, S.find_1 in Hm; trivial. symmetry. assumption. } - { inversion_clear Hin. + destruct H1 as [H1 H2]; hnf in H1, H2; simpl in H1, H2. subst v'. right. split. - intro Habs. apply H. rewrite <- H1. revert Habs. apply InA_compat; trivial; refine _. - apply S.find_1, S.add_1. symmetry. assumption. + left. assumption. } - { destruct Hin as [Hin Hm]. right. split. + intro Habs. apply Hin. right. assumption. + apply S.find_1, S.add_2, S.find_2; trivial. intro Habs. apply Hin. left. symmetry. assumption. } + intros [z w] Hin [v'' Hadd]. simpl in *. destruct (X.eq_dec y z) as [Heq | Heq]. - assert (Hz : (X.eq @@1)%signature (y, v') (z, w)). { hnf. simpl. assumption. } rewrite Hz in H. contradiction. - apply S.add_3 in Hadd; trivial. apply (Hdiff (z, w)). right. assumption. exists v''. assumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface