proposition: Lemma binsert_correct_DB db_schema qs index (bag_plus : BagPlusProof (@RawTuple _)) : forall (store: BagTypePlus bag_plus), GetUnConstrRelation qs index ≃ store -> forall tuple bound (ValidBound : UnConstrFreshIdx (GetUnConstrRelation qs index) bound), EnsembleIndexedListEquivalence (GetUnConstrRelation (@UpdateUnConstrRelation db_schema qs index (EnsembleInsert {| elementIndex := bound; indexedElement := tuple |} (GetUnConstrRelation qs index))) index) (benumerate (binsert (Bag := BagPlus bag_plus) store tuple)).
proof: Proof. intros * store_eqv; destruct store_eqv as (store_eqv, store_WF). unfold EnsembleIndexedTreeEquivalence_AbsR, UnConstrFreshIdx, EnsembleBagEquivalence, EnsembleIndexedListEquivalence, UnIndexedEnsembleListEquivalence, EnsembleListEquivalence in *. setoid_rewrite get_update_unconstr_eq. setoid_rewrite in_ensemble_insert_iff. setoid_rewrite NoDup_modulo_permutation. split; intros. unfold UnConstrFreshIdx; exists (S bound); intros; intuition; subst; simpl. unfold EnsembleInsert in *; intuition; subst; simpl; omega. destruct store_eqv as (indices & [ l' (map & equiv & nodup ) ]); eauto. destruct (permutation_map_cons indexedElement (binsert_enumerate tuple store store_WF) {| elementIndex := bound; indexedElement := tuple |} l' eq_refl map) as [ l'0 (map' & perm) ]. exists l'0. split; [ assumption | split ]. setoid_rewrite perm; setoid_rewrite equiv; simpl; intuition eauto. eexists (bound :: _); split; try apply perm; eauto. constructor; eauto. unfold not; intros. match goal with | [ H : List.In _ _ |- _ ] => rewrite in_map_iff in H; destruct_ex; intuition; subst end. match goal with | [ H : List.In _ _, ValidBound : forall element : IndexedElement, _ |- _ ] => apply equiv in H2; apply ValidBound in H2; destruct x; simpl in *; omega end. setoid_rewrite perm; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Coq.Lists.List Coq.Program.Program Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.NArith.BinNat Coq.ZArith.ZArith_dec Coq.Arith.Arith Coq.FSets.FMapAVL Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements Fiat.QueryStructure.Implementation.Operations.List.ListQueryRefinements