proposition: Lemma fold_left_add2_Eq {B C} : forall f f' k (v : C) l st, let f' := (fun (acc : @StringMap.t C) (el : B) => StringMap.add (f el) (f' el) acc) in ~ StringMap.In k (fold_left f' l (StringMap.empty _)) -> StringMap.Equal (fold_left f' l ([k |> v]::st)) ([k |> v]:: (fold_left f' l st)).
proof: Proof. induction l; simpl; intros. - reflexivity. - rewrite <- IHl. + rewrite StringMap_fold_left_Eq. reflexivity. unfold StringMap.Equal; simpl. intros; rewrite !add_o; repeat find_if_inside; eauto; subst. destruct H. remember (StringMap.empty C); clear. remember (f' a). clear; revert t c; induction l; simpl; intros. eexists; apply StringMap.add_1; eauto. destruct (string_dec (f a0) (f a)); subst; simpl. rewrite e; eapply IHl. destruct (IHl ([f a0 |> f' a0]::t) c). eexists x. setoid_rewrite find_mapsto_iff. setoid_rewrite StringMap_fold_left_Eq. setoid_rewrite <- find_mapsto_iff. eapply H. unfold StringMap.Equal; intros; rewrite !add_o; repeat find_if_inside; try congruence. + intro; apply H. remember (StringMap.empty C). revert H0; generalize a t; clear; induction l; simpl; intros. * destruct (string_dec k (f a)); subst. eexists (f' a); apply StringMap.add_1; eauto. destruct H0. eexists x; apply StringMap.add_2; eauto. * eapply (IHl a0) in H0. eapply StringMap_In_Permutation. 2: apply H0. clear; intros; destruct H. apply add_mapsto_iff in H; intuition; subst. destruct (string_dec (f a) (f a0)); subst. eexists (f' a). apply StringMap.add_1; eauto. eexists (f' a0). apply StringMap.add_2; eauto. apply StringMap.add_1; eauto. apply add_mapsto_iff in H1; intuition; subst. eexists (f' a). apply StringMap.add_1; eauto. eexists x. apply StringMap.add_2; eauto. apply StringMap.add_2; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.ADT.Core Bedrock.Platform.Facade.DFModule Fiat.ADTNotation Bedrock.Platform.Facade.CompileUnit2 Fiat.Common.i3list Fiat.Common.ilist3 CertifiedExtraction.Core CertifiedExtraction.FacadeUtils CertifiedExtraction.StringMapUtils CertifiedExtraction.Extraction.Internal CertifiedExtraction.Extraction.Extraction