proposition: Lemma QSDeleteSpec_UnConstr_refine_opt : forall qsSchema qs Ridx DeletedTuples or, @DropQSConstraints_AbsR qsSchema or qs -> refine (or' <- (QSDelete or Ridx DeletedTuples); nr' <- {nr' | DropQSConstraints_AbsR (fst or') nr'}; ret (nr', snd or')) match (tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)) with | 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 (EnsembleDelete (GetRelation or Ridx) DeletedTuples) 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') (EnsembleDelete (GetRelation or Ridx) DeletedTuples) 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 with | true, true => deleted <- Pick (QSDeletedTuples qs Ridx DeletedTuples); ret (UpdateUnConstrRelation qs Ridx (EnsembleDelete (GetUnConstrRelation qs Ridx) DeletedTuples), deleted) | _, _ => ret (qs, []) end | 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') (EnsembleDelete (GetRelation or Ridx) DeletedTuples) 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 with | true => deleted <- Pick (QSDeletedTuples qs Ridx DeletedTuples); ret (UpdateUnConstrRelation qs Ridx (EnsembleDelete (GetUnConstrRelation qs Ridx) DeletedTuples), deleted) | _ => ret (qs, []) end end.
proof: Proof. unfold QSDelete. intros; rewrite QSMutateSpec_UnConstr_refine; eauto using QSDeleteSpec_UnConstr_refine_AttributeConstraints, refine_SatisfiesTupleConstraintsMutate, refine_SatisfiesCrossConstraintsMutate, QSDeleteSpec_UnConstr_refine_CrossConstraints'. simplify with monad laws. unfold SatisfiesTupleConstraints. case_eq (tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)); intros; [eapply refine_under_bind; intros | simplify with monad laws]. simpl; unfold DropQSConstraints_AbsR, QSDeletedTuples in *; subst. f_equiv; unfold pointwise_relation; intros; repeat find_if_inside; try simplify with monad laws; try reflexivity. rewrite GetRelDropConstraints, get_update_unconstr_eq; f_equiv. f_equiv; unfold pointwise_relation; intros; eauto. simpl; unfold DropQSConstraints_AbsR, QSDeletedTuples in *; subst. repeat find_if_inside; try simplify with monad laws; try reflexivity. rewrite GetRelDropConstraints, get_update_unconstr_eq; f_equiv. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Common.List.ListFacts 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.Common.Ensembles.IndexedEnsembles Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Delete 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.QueryStructure.Implementation.Operations.General.MutateRefinements Fiat.Common.Ensembles.EnsembleListEquivalence