proposition: Lemma FMap_fold_add_MapsTo_In : forall (Value : Type) (l : list (MKeys.key)) (k : MKeys.key) (v : Value) (bag' : MKeys.t Value) z, ~ InA E.eq k (map fst (MKeys.elements bag')) -> (MKeys.MapsTo k v (fold_left (fun (a : MKeys.t Value) (p : MKeys.key) => MKeys.add p z a) l bag') <-> (InA E.eq k l /\ v = z)) .
proof: Proof. setoid_rewrite MoreMKeysFacts.BasicFacts.elements_mapsto_iff. induction l; simpl; split; intros; intuition. - exfalso; apply H. eapply (inA_map (f := fst)) in H0; eauto using RelationPairs.fst_compat with typeclass_instances. - exfalso; apply H. eapply (inA_map (f := fst)) in H0; eauto using RelationPairs.fst_compat with typeclass_instances. - inversion H1. - destruct (E.eq_dec k a). + eauto. + eapply IHl in H0; intuition. * apply H. let H1 := match goal with H1 : InA _ _ _ |- _ => constr:(H1) end in apply inA_map' with (eqA := @MKeys.eq_key_elt _) in H1; eauto using RelationPairs.fst_compat with typeclass_instances. destruct_ex; intuition. let H3 := match goal with H3 : E.eq _ _ |- _ => constr:(H3) end in rewrite H3. destruct x. let H2 := match goal with H2 : InA _ _ _ |- _ => constr:(H2) end in rewrite <- MoreMKeysFacts.BasicFacts.elements_mapsto_iff in H2. eapply inA_map with (eqA := @MKeys.eq_key_elt _); eauto using RelationPairs.fst_compat with typeclass_instances. let H2 := match goal with H2 : InA _ _ _ |- _ => constr:(H2) end in rewrite <- MoreMKeysFacts.BasicFacts.elements_mapsto_iff. let H2 := match goal with H2 : MKeys.MapsTo _ _ _ |- _ => constr:(H2) end in rewrite MoreMKeysFacts.BasicFacts.add_mapsto_iff in H2; intuition; subst. let H2 := match goal with H2 : MKeys.E.eq _ _ |- _ => constr:(H2) end in simpl in H3; rewrite H2 in n; intuition. - destruct (E.eq_dec k a). rewrite <- MoreMKeysFacts.BasicFacts.elements_mapsto_iff in H0. rewrite e in H0. assert (MKeys.MapsTo a z (MKeys.add a z bag')). apply MKeys.add_1; eauto. remember (MKeys.add a z bag') as bag''; clear Heqbag''. revert bag'' H1 H0; clear; induction l; simpl; intros. + eapply MoreMKeysFacts.BasicFacts.MapsTo_fun; eauto. + eapply (IHl (MKeys.add a0 z bag'')); eauto. eapply MoreMKeysFacts.BasicFacts.add_mapsto_iff; intuition. destruct (E.eq_dec a0 a); intuition. + eapply IHl with (bag' := MKeys.add a z bag'); eauto. intros. apply inA_map' with (eqA := @MKeys.eq_key_elt _) in H1; eauto using RelationPairs.fst_compat with typeclass_instances. destruct_ex; intuition. destruct x; rewrite <- MoreMKeysFacts.BasicFacts.elements_mapsto_iff in H2. rewrite MoreMKeysFacts.BasicFacts.add_mapsto_iff in H2; intuition; subst. simpl in *; rewrite H3 in n; intuition. apply H. rewrite MoreMKeysFacts.BasicFacts.elements_mapsto_iff in H4. eapply inA_map with (f := fst) in H4. simpl in *; rewrite H3; eauto. eauto using RelationPairs.fst_compat with typeclass_instances. - inversion H1; subst. + rewrite H3. rewrite <- MoreMKeysFacts.BasicFacts.elements_mapsto_iff. assert (MKeys.MapsTo a z (MKeys.add a z bag')). apply MKeys.add_1; eauto. remember (MKeys.add a z bag') as bag''; clear Heqbag''. revert bag'' H0; clear; induction l; simpl; intros; eauto. eapply IHl; eauto. destruct (E.eq_dec a a0). rewrite MoreMKeysFacts.BasicFacts.add_mapsto_iff; intuition. rewrite MoreMKeysFacts.BasicFacts.add_mapsto_iff; intuition. + destruct (E.eq_dec k a). * rewrite e. assert (MKeys.MapsTo a z (MKeys.add a z bag')). apply MKeys.add_1; eauto. remember (MKeys.add a z bag') as bag''; clear Heqbag''. generalize a bag'' H0; clear; induction l; simpl; intros. rewrite <- MoreMKeysFacts.BasicFacts.elements_mapsto_iff; eauto. eapply IHl; eauto. destruct (MKeys.E.eq_dec a0 a); intuition. * eapply IHl; eauto. intro. apply inA_map' with (eqA := @MKeys.eq_key_elt _) in H0; eauto using RelationPairs.fst_compat with typeclass_instances. destruct_ex; intuition. destruct x. rewrite <- MoreMKeysFacts.BasicFacts.elements_mapsto_iff in H2. apply H. rewrite MoreMKeysFacts.BasicFacts.add_mapsto_iff in H2; intuition. subst; simpl in *. rewrite H4, H2 in n; intuition. simpl in *. rewrite MoreMKeysFacts.BasicFacts.elements_mapsto_iff in H5. rewrite H4. eapply inA_map with (f := fst) in H5; simpl in *; eauto using RelationPairs.fst_compat with typeclass_instances. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.Arith.Peano_dec Coq.Structures.OrdersEx Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListInclusion