proposition: Lemma refine_SuccessfulInsert : forall qsSchema (qs : QueryStructure qsSchema) Ridx tup b, computes_to {idx | UnConstrFreshIdx (GetRelation qs Ridx) idx} b -> refine (b <- {result : bool | decides result (forall t : IndexedElement, GetRelation qs Ridx t <-> EnsembleInsert {| elementIndex := b; indexedElement := tup |} (GetRelation qs Ridx) t)}; ret (qs, b)) (ret (qs, false)).
proof: Proof. intros; computes_to_inv. unfold UnConstrFreshIdx in *. refine pick val false; simpl. - simplify with monad laws; reflexivity. - intro. unfold EnsembleInsert in H0. assert (GetRelation qs Ridx {| elementIndex := b; indexedElement := tup |}). eapply H0; intuition. apply H in H1; simpl in *; intuition. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.IterateBoundedIndex Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements