proposition: Lemma QSMutateSpec_refine : forall (qsSchema : QueryStructureSchema) (qs : QueryStructure qsSchema) Ridx (MutatedTuples : IndexedEnsemble ), refine (Pick (QSMutateSpec qs Ridx MutatedTuples)) (attributeConstr <- {b | (forall tup, GetRelation qs Ridx tup -> SatisfiesAttributeConstraints Ridx (indexedElement tup)) -> decides b (MutationPreservesAttributeConstraints MutatedTuples (SatisfiesAttributeConstraints Ridx))}; tupleConstr <- {b | (forall tup tup', elementIndex tup <> elementIndex tup' -> GetRelation qs Ridx tup -> GetRelation qs Ridx tup' -> SatisfiesTupleConstraints Ridx (indexedElement tup) (indexedElement tup')) -> decides b (MutationPreservesTupleConstraints MutatedTuples (SatisfiesTupleConstraints Ridx))}; crossConstr <- {b | (forall Ridx', Ridx' <> Ridx -> forall tup', (GetRelation qs Ridx') tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (GetRelation qs Ridx)) -> decides b (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints (GetRelation qs Ridx') MutatedTuples (SatisfiesCrossRelationConstraints Ridx' Ridx))}; crossConstr' <- {b | (forall Ridx', Ridx' <> Ridx -> forall tup', (GetRelation qs Ridx) tup' -> SatisfiesCrossRelationConstraints Ridx Ridx' (indexedElement tup') (GetRelation qs Ridx')) -> decides b (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints MutatedTuples (GetRelation qs Ridx') (SatisfiesCrossRelationConstraints Ridx Ridx'))}; match attributeConstr, tupleConstr, crossConstr, crossConstr' with | true, true, true, true => {qs' | (forall Ridx', Ridx <> Ridx' -> GetRelation qs Ridx' = GetRelation qs' Ridx') /\ forall t, GetRelation qs' Ridx t <-> MutatedTuples t } | _, _, _, _ => ret qs end).
proof: Proof. intros qsSchema qs Ridx MutatedTuples v Comp_v. computes_to_inv. assert (decides v0 (MutationPreservesAttributeConstraints MutatedTuples (SatisfiesAttributeConstraints Ridx))) as H0' by (apply Comp_v; intros; unfold SatisfiesAttributeConstraints, QSGetNRelSchema, GetNRelSchema; pose proof (rawAttrconstr ((ith2 (rawRels qs) Ridx))) as H'; destruct (attrConstraints (Vector.nth (qschemaSchemas qsSchema) Ridx)); [apply H' | ]; eauto); clear Comp_v. assert (decides v1 (MutationPreservesTupleConstraints MutatedTuples (SatisfiesTupleConstraints Ridx))) as H1' by (apply Comp_v'; unfold SatisfiesTupleConstraints, QSGetNRelSchema, GetNRelSchema; pose proof (rawTupleconstr ((ith2 (rawRels qs) Ridx))) as H'; destruct (tupleConstraints (Vector.nth (qschemaSchemas qsSchema) Ridx)); [apply H' | ]; eauto); clear Comp_v'. assert (decides v2 (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints (GetRelation qs Ridx') MutatedTuples (SatisfiesCrossRelationConstraints Ridx' Ridx))) as H2' by (apply Comp_v''; intros; pose proof (crossConstr qs Ridx' Ridx); unfold SatisfiesCrossRelationConstraints; simpl; destruct (BuildQueryStructureConstraints qsSchema Ridx' Ridx); eauto); clear Comp_v''. assert (decides v3 (forall Ridx', Ridx' <> Ridx -> MutationPreservesCrossConstraints MutatedTuples (GetRelation qs Ridx') (SatisfiesCrossRelationConstraints Ridx Ridx'))) as H3' by (apply Comp_v'''; intros; pose proof (crossConstr qs Ridx Ridx'); unfold SatisfiesCrossRelationConstraints; simpl; destruct (BuildQueryStructureConstraints qsSchema Ridx Ridx'); eauto); clear Comp_v'''. destruct v0; destruct v1; destruct v2; destruct v3; try solve [computes_to_econstructor; computes_to_inv; subst; unfold QSMutateSpec; simpl in *; right; subst; intuition]. computes_to_inv; subst; computes_to_econstructor; unfold QSMutateSpec; simpl in *; left; intuition eauto. - rewrite <- H; eauto. - rewrite <- H; eauto. - unfold Same_set, Included, In; eauto; intuition; eapply H0; eauto. - rewrite H; 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