proposition: Lemma QSMutateSpec_UnConstr_refine_opt : forall qsSchema qs Ridx MutatedTuples or, @DropQSConstraints_AbsR qsSchema or qs -> refine (or' <- QSMutate or Ridx MutatedTuples; nr' <- {nr' | DropQSConstraints_AbsR (fst or') nr'}; ret (nr', snd or')) match (attrConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)), (tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)) with | Some aConstr, Some tConstr => attrConstr <- {b | (forall tup, GetUnConstrRelation qs Ridx tup -> aConstr (indexedElement tup)) -> decides b (MutationPreservesAttributeConstraints MutatedTuples aConstr) }; tupleConstr <- {b | (forall tup tup', elementIndex tup <> elementIndex tup' -> GetUnConstrRelation qs Ridx tup -> GetUnConstrRelation qs Ridx tup' -> tConstr (indexedElement tup) (indexedElement tup')) -> decides b (MutationPreservesTupleConstraints MutatedTuples tConstr) }; crossConstr <- (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))); crossConstr' <- (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 MutatedTuples (GetUnConstrRelation qs Ridx') 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))); 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 | Some aConstr, None => attrConstr <- {b | (forall tup, GetUnConstrRelation qs Ridx tup -> aConstr (indexedElement tup)) -> decides b (MutationPreservesAttributeConstraints MutatedTuples aConstr) }; crossConstr <- (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))); crossConstr' <- (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 MutatedTuples (GetUnConstrRelation qs Ridx') 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))); match attrConstr, crossConstr, crossConstr' with | 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 | None, Some tConstr => tupleConstr <- {b | (forall tup tup', elementIndex tup <> elementIndex tup' -> GetUnConstrRelation qs Ridx tup -> GetUnConstrRelation qs Ridx tup' -> tConstr (indexedElement tup) (indexedElement tup')) -> decides b (MutationPreservesTupleConstraints MutatedTuples tConstr) }; crossConstr <- (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))); crossConstr' <- (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 MutatedTuples (GetUnConstrRelation qs Ridx') 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))); match tupleConstr, crossConstr, crossConstr' with | 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 | None, None => crossConstr <- (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))); crossConstr' <- (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 MutatedTuples (GetUnConstrRelation qs Ridx') 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))); match crossConstr, crossConstr' with | 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 end.
proof: Proof. intros; rewrite QSMutateSpec_UnConstr_refine; eauto using refine_SatisfiesTupleConstraintsMutate, refine_SatisfiesAttributeConstraintsMutate, refine_SatisfiesCrossConstraintsMutate, refine_SatisfiesCrossConstraintsMutate'. - unfold SatisfiesTupleConstraints, SatisfiesAttributeConstraints. destruct (attrConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)). + destruct (tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)). reflexivity. simplify with monad laws; f_equiv. + simplify with monad laws; f_equiv. destruct (tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)). reflexivity. simplify with monad laws; f_equiv. 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