proposition: Lemma refine_For_In_Insert : forall ResultT MySchema R or a tup bod, (forall tup, GetUnConstrRelation or R tup -> RawTupleIndex tup <> a) -> refine (Query_For (@UnConstrQuery_In ResultT MySchema (UpdateUnConstrRelation or R (EnsembleInsert {| elementIndex := a; indexedElement := tup |} (GetUnConstrRelation or R))) R bod)) (newResults <- bod tup; origResults <- (Query_For (@UnConstrQuery_In ResultT MySchema or R bod)); {l | Permutation.Permutation (newResults ++ origResults) l}).
proof: Proof. intros; rewrite refine_For. unfold UnConstrQuery_In, GetUnConstrRelation at 1, UpdateUnConstrRelation. rewrite ith_replace2_Index_eq. unfold QueryResultComp; simplify with monad laws. rewrite Ensemble_List_Equivalence_Insert. - setoid_rewrite refineEquiv_bind_bind. setoid_rewrite refineEquiv_bind_unit; simpl. simplify with monad laws. Transparent Query_For. unfold Query_For. repeat setoid_rewrite refineEquiv_bind_bind; simpl. unfold refine; intros; computes_to_inv. repeat computes_to_econstructor; eauto. rewrite Permutation.Permutation_app_head; eauto. - simpl; unfold In, not; intros; destruct_ex; intuition. eapply H; eauto. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Common.ilist2 Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Operations.Empty Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Specification.Operations.Update Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements