proposition: Lemma Trie_add_Preserves_TreeOK : forall trie item st1 st2, eqlistA X.eq (projection item) (st2 ++ st1) -> TrieOK trie st2 -> TrieOK (Trie_add trie st1 item) st2.
proof: Proof. intros trie item st1; eapply Trie_add_ind; intros; subst. - econstructor; inversion H0; subst; eauto. + eapply binsert_RepInv; eauto. + intros; rewrite binsert_enumerate in H5 by eauto. simpl in *; intuition; subst. rewrite H, app_nil_r; reflexivity. - econstructor; inversion H1; subst; simpl; eauto. intros; destruct (X.eq_dec k key0). apply find_1 in H6; eauto. pose proof (add_1 subtries (Trie_add subtrie st' item0) (X.eq_sym e)) as H7; apply find_1 in H7; eauto. rewrite H6 in H7; injections; intros; subst. eapply H; eauto. rewrite <- app_assoc. rewrite H0. apply eqlistA_app; repeat first [econstructor; eauto | try reflexivity ]; try typeclasses eauto; try (symmetry; assumption). apply H5. apply MapsTo_1 with (x := key0). symmetry; eauto. apply find_2; eassumption. apply H5. eapply add_3 in H6; eauto; intuition. - econstructor; inversion H1; subst; simpl; eauto. + intros; destruct (X.eq_dec k key0). apply find_1 in H6; eauto. pose proof (add_1 subtries (Trie_add TrieBag_bempty st' item0) (X.eq_sym e)) as H7; apply find_1 in H7; eauto. rewrite H6 in H7; injections; intros; subst. eapply H; eauto. rewrite <- app_assoc. rewrite H0. apply eqlistA_app; repeat first [econstructor; eauto | try reflexivity ]; try typeclasses eauto; try (symmetry; assumption). unfold TrieBagRepInv; intros; econstructor; simpl in *. apply bempty_RepInv. econstructor. intros; exfalso; eapply benumerate_empty; eauto. intros; exfalso; eapply empty_1; eauto. apply H5. eapply add_3 in H6; eauto; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsProperties Coq.FSets.FMapInterface Coq.FSets.FMapFacts Coq.FSets.FMapAVL Coq.ZArith.ZArith Fiat.Common Fiat.Common.List.ListFacts Fiat.Common.List.FlattenList Fiat.Common.SetEqProperties Fiat.Common.FMapExtensions Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Specification.SearchTerms.ListPrefix