proposition: Lemma refine_SatisfiesAttributeConstraintsMutate : forall qsSchema qs Ridx MutatedTuples, refine {b | (forall tup, GetUnConstrRelation qs Ridx tup -> SatisfiesAttributeConstraints Ridx (indexedElement tup)) -> decides b (MutationPreservesAttributeConstraints MutatedTuples (SatisfiesAttributeConstraints Ridx))} 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.
proof: Proof. intros; unfold MutationPreservesAttributeConstraints, SatisfiesAttributeConstraints. destruct (attrConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)); try reflexivity. intros v Comp_v; computes_to_econstructor; computes_to_inv; subst. simpl; tauto. 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