proposition: Lemma CountingList_bupdate_Preserves_RepInv : bupdate_Preserves_RepInv CountingList_RepInv CountingList_ValidUpdate CountingListAsBag_bupdate.
proof: Proof. unfold bupdate_Preserves_RepInv, CountingList_RepInv, CountingListAsBag_bupdate. destruct container as [n l]; simpl; revert n; induction l; intros; simpl in *; eauto. destruct (search_term a); simpl. destruct n; simpl in *; [ discriminate | injection containerCorrect]; intros. pose proof (IHl n search_term update_term). destruct (CountingListPartition l search_term); simpl in *; eauto. apply H0 in H. assert (forall {A: Type} a (b: A) c, (length (a ++ b :: c) = S (length (a ++ c)))). induction a0; intros; auto; simpl; rewrite IHa0; reflexivity. rewrite H1; rewrite H; reflexivity. apply valid_update. destruct n; simpl in *; [ discriminate | injection containerCorrect]; intros. pose proof (IHl n search_term update_term). destruct (CountingListPartition l search_term); simpl in *; eauto. Qed.
imports: Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Coq.Arith.Arith Fiat.Common.List.ListFacts