proposition: Lemma QSMutateSpec_UnConstr_refine : forall qsSchema qs Ridx MutatedTuples or refined_attrConstr refined_tupleConstr refined_crossConstr refined_crossConstr', @DropQSConstraints_AbsR qsSchema or qs -> refine {b | (forall tup, GetUnConstrRelation qs Ridx tup -> SatisfiesAttributeConstraints Ridx (indexedElement tup)) -> decides b (MutationPreservesAttributeConstraints MutatedTuples (SatisfiesAttributeConstraints Ridx))} refined_attrConstr -> refine {b | (forall tup tup', elementIndex tup <> elementIndex tup' -> GetUnConstrRelation qs Ridx tup -> GetUnConstrRelation qs Ridx tup' -> SatisfiesTupleConstraints Ridx (indexedElement tup) (indexedElement tup')) -> decides b (MutationPreservesTupleConstraints MutatedTuples (SatisfiesTupleConstraints Ridx))} refined_tupleConstr -> refine {b | (forall Ridx', Ridx' <> Ridx -> forall tup', (GetUnConstrRelation qs Ridx') tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (GetUnConstrRelation qs Ridx)) -> decides b (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints (GetUnConstrRelation qs Ridx') MutatedTuples (SatisfiesCrossRelationConstraints Ridx' Ridx))} refined_crossConstr -> refine {b | (forall Ridx', Ridx' <> Ridx -> forall tup', (GetUnConstrRelation qs Ridx tup') -> SatisfiesCrossRelationConstraints Ridx Ridx' (indexedElement tup') (GetUnConstrRelation qs Ridx')) -> decides b (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints MutatedTuples (GetUnConstrRelation qs Ridx') (SatisfiesCrossRelationConstraints Ridx Ridx'))} refined_crossConstr' -> refine (or' <- QSMutate or Ridx MutatedTuples; nr' <- {nr' | DropQSConstraints_AbsR (fst or') nr'}; ret (nr', snd or')) (attrConstr <- refined_attrConstr; tupleConstr <- refined_tupleConstr; crossConstr <- refined_crossConstr; crossConstr' <- refined_crossConstr'; match attrConstr, tupleConstr, crossConstr, crossConstr' with | true, true, true, true => mutated <- Pick (UnIndexedEnsembleListEquivalence (Intersection _ (GetRelation or Ridx) (Complement _ (GetUnConstrRelation (UpdateUnConstrRelation qs Ridx MutatedTuples) Ridx)))); ret (UpdateUnConstrRelation qs Ridx MutatedTuples, mutated) | _, _, _, _ => ret (DropQSConstraints or, []) end).
proof: Proof. intros; unfold QSMutate; simplify with monad laws. setoid_rewrite (@QSMutateSpec_UnConstr_refine' _ qs Ridx); eauto. setoid_rewrite <- H0; setoid_rewrite <- H1. setoid_rewrite <- H2; setoid_rewrite <- H3. simplify with monad laws; repeat (eapply refine_under_bind; intros; eauto); eauto. repeat find_if_inside; try solve [simplify with monad laws; refine pick val _; [ simplify with monad laws; refine pick val (DropQSConstraints or); try simplify with monad laws | eauto using ComplementIntersectionIndexedList]; reflexivity ]. computes_to_inv; simpl in *. unfold DropQSConstraints_AbsR in *; subst. repeat rewrite (fun Ridx => GetRelDropConstraints or Ridx) in *. refine pick val (Mutate_Valid or H4 H5 (refine_Iterate_MutationPreservesCrossConstraints (refl_equal _) H7) (refine_Iterate_MutationPreservesCrossConstraints' (refl_equal _) H6)); [ simplify with monad laws | unfold Mutate_Valid, DropQSConstraints, UpdateRelation, UpdateUnConstrRelation; simpl; repeat rewrite imap_replace2_Index by eauto using string_dec; simpl; try reflexivity]. f_equiv. - unfold GetRelation, GetUnConstrRelation, Mutate_Valid, UpdateRelation, DropQSConstraints, UpdateUnConstrRelation; simpl; repeat rewrite ith_replace2_Index_eq; reflexivity. - unfold pointwise_relation; intros. refine pick val _; [ simplify with monad laws; reflexivity | unfold GetRelation, GetUnConstrRelation, Mutate_Valid, UpdateRelation, DropQSConstraints, UpdateUnConstrRelation; simpl; rewrite imap_replace2_Index by eauto using string_dec; try reflexivity ]. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.ilist2 Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.Schema Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Mutate Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements Fiat.Common.IterateBoundedIndex Fiat.Common.DecideableEnsembles Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.Ensembles.EnsembleListEquivalence