proposition: Lemma QSMutateSpec_refine_subgoals ResultT : forall qsSchema (qs : QueryStructure qsSchema) qs' Ridx default success refined_schConstr_self refined_schConstr refined_qsConstr refined_qsConstr' MutatedTuples (k : _ -> Comp ResultT), DropQSConstraints_AbsR qs qs' -> refine match attrConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx) with | Some Constr => {b | (forall tup, GetUnConstrRelation qs' Ridx tup -> SatisfiesAttributeConstraints Ridx (indexedElement tup)) -> decides b (MutationPreservesAttributeConstraints MutatedTuples (SatisfiesAttributeConstraints Ridx)) } | None => ret true end refined_schConstr_self -> refine match tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx) with | Some Constr => {b | (forall tup tup', elementIndex tup <> elementIndex tup' -> GetUnConstrRelation qs' Ridx tup -> GetUnConstrRelation qs' Ridx tup' -> Constr (indexedElement tup) (indexedElement tup')) -> decides b (MutationPreservesTupleConstraints MutatedTuples Constr) } | None => ret true end refined_schConstr -> refine (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) )) refined_qsConstr -> refine (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) )) refined_qsConstr' -> (forall qs'' qs''' mutated, DropQSConstraints_AbsR qs'' qs''' -> (forall Ridx', Ridx <> Ridx' -> GetRelation qs Ridx' = GetRelation qs'' Ridx') -> (forall t, GetRelation qs'' Ridx t <-> MutatedTuples t) -> UnIndexedEnsembleListEquivalence (Intersection _ (GetRelation qs Ridx) (Complement _ (GetUnConstrRelation (UpdateUnConstrRelation qs' Ridx MutatedTuples) Ridx))) mutated -> refine (k (qs'', mutated)) (success qs''' mutated)) -> refine (k (qs, [ ])) default -> refine (qs' <- QSMutate qs Ridx MutatedTuples; k qs') (schConstr_self <- refined_schConstr_self; schConstr <- refined_schConstr; qsConstr <- refined_qsConstr; qsConstr' <- refined_qsConstr'; match schConstr_self, schConstr, qsConstr, qsConstr' with | true, true, true, true => mutated <- Pick (UnIndexedEnsembleListEquivalence (Intersection _ (GetRelation qs Ridx) (Complement _ (GetUnConstrRelation (UpdateUnConstrRelation qs' Ridx MutatedTuples) Ridx)))); qs'' <- UpdateUnConstrRelationMutateC qs' Ridx MutatedTuples; success qs'' mutated | _, _, _, _ => default end).
proof: Proof. intros; rewrite QSMutateSpec_refine_subgoals'; eauto; f_equiv. rewrite refine_SatisfiesAttributeConstraintsMutate; eauto. rewrite refine_SatisfiesTupleConstraintsMutate; eauto. rewrite refine_SatisfiesCrossConstraintsMutate; eauto. rewrite refine_SatisfiesCrossConstraintsMutate'; eauto. 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