proposition: Lemma QSMutateSpec_UnConstr_refine' : forall qsSchema qs Ridx or MutatedTuples, @DropQSConstraints_AbsR qsSchema or qs -> refine {or' | QSMutateSpec or Ridx MutatedTuples or'} (attributeConstr <- {b | (forall tup, GetUnConstrRelation qs Ridx tup -> SatisfiesAttributeConstraints Ridx (indexedElement tup)) -> decides b (MutationPreservesAttributeConstraints MutatedTuples (SatisfiesAttributeConstraints Ridx))}; tupleConstr <- {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))}; crossConstr <- {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))}; crossConstr' <- {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'))}; match attributeConstr, tupleConstr, crossConstr, crossConstr' with | true, true, true, true => {or' | DropQSConstraints_AbsR or' (UpdateUnConstrRelation qs Ridx MutatedTuples)} | _, _, _, _ => ret or end).
proof: Proof. unfold DropQSConstraints_AbsR; intros; subst. setoid_rewrite QSMutateSpec_refine. repeat setoid_rewrite refineEquiv_bind_bind. rewrite !GetRelDropConstraints. f_equiv; unfold pointwise_relation; intros. f_equiv; unfold pointwise_relation; intros. f_equiv; unfold pointwise_relation; intros. { intros v Comp_v; subst; computes_to_inv; unfold decides, If_Then_Else in *; find_if_inside; intros; computes_to_econstructor; intros. - rewrite <- GetRelDropConstraints in *; eapply Comp_v; intros; eauto; eapply H; eauto; rewrite <- GetRelDropConstraints; eauto. - unfold not; intros; eapply Comp_v; intros. + eapply H; eauto; rewrite <- GetRelDropConstraints; eauto. + rewrite GetRelDropConstraints; eauto. } f_equiv; unfold pointwise_relation; intros. { intros v Comp_v; subst; computes_to_inv; unfold decides, If_Then_Else in *; find_if_inside; intros; computes_to_econstructor; intros. - rewrite <- GetRelDropConstraints in *; eapply Comp_v; intros; eauto. rewrite GetRelDropConstraints; eapply H; eauto. - unfold not; intros; eapply Comp_v; intros. + rewrite GetRelDropConstraints; eauto. + rewrite GetRelDropConstraints; eauto. } repeat find_if_inside; try reflexivity. intros v Comp_v; computes_to_inv; subst; computes_to_econstructor; simpl. rewrite <- GetRelDropConstraints; setoid_rewrite <- GetRelDropConstraints; subst; rewrite Comp_v; split; intros; unfold GetUnConstrRelation, DropQSConstraints, UpdateUnConstrRelation. rewrite ith_replace2_Index_neq; eauto using string_dec. rewrite ith_replace2_Index_eq; intuition. 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