proposition: Lemma refine_SatisfiesCrossConstraintsMutate : forall qsSchema qs Ridx MutatedTuples, 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))} (Iterate_Decide_Comp_opt_Pre _ (fun Ridx' => if fin_eq_dec Ridx Ridx' then None else match BuildQueryStructureConstraints qsSchema Ridx' Ridx with | Some CrossConstr => Some ( (MutationPreservesCrossConstraints (GetUnConstrRelation qs Ridx') MutatedTuples CrossConstr)) | None => None end) (@Iterate_Ensemble_BoundedIndex_filter _ (fun Ridx' => forall tup', (GetUnConstrRelation qs Ridx') tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (GetUnConstrRelation qs Ridx)) (fun idx => if (fin_eq_dec Ridx idx) then false else true) )).
proof: Proof. intros; simpl. unfold MutationPreservesCrossConstraints. setoid_rewrite <- refine_Iterate_Decide_Comp_Pre. setoid_rewrite Iterate_Decide_Comp_BoundedIndex_Pre. eapply refine_Iterate_Decide_Comp_equiv_Pre; eauto using string_dec. - unfold SatisfiesCrossRelationConstraints; intros. destruct (fin_eq_dec Ridx idx); [congruence | destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto]. - unfold not; intros; eapply H. unfold SatisfiesCrossRelationConstraints in *. destruct (fin_eq_dec Ridx idx); [ eauto | destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto]. - setoid_rewrite <- Iterate_Ensemble_filter_neq; eauto using string_dec. 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