proposition: Lemma QSDeleteSpec_refine_subgoals ResultT : forall qsSchema (qs : QueryStructure qsSchema) qs' Ridx default success refined_schConstr refined_qsConstr (DeletedTuples : Ensemble RawTuple) (k : _ -> Comp ResultT), DropQSConstraints_AbsR qs qs' -> 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 (EnsembleDelete (GetUnConstrRelation qs' Ridx) DeletedTuples) 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') (EnsembleDelete (GetUnConstrRelation qs' 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) )) 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 <-> EnsembleDelete (GetRelation qs Ridx) DeletedTuples t) -> QSDeletedTuples qs' Ridx DeletedTuples mutated -> refine (k (qs'', mutated)) (success qs''' mutated)) -> refine (k (qs, [ ])) default -> refine (qs' <- QSDelete qs Ridx DeletedTuples; k qs') ( schConstr <- refined_schConstr; qsConstr <- refined_qsConstr; match schConstr, qsConstr with | true, true => mutated <- Pick (QSDeletedTuples qs' Ridx DeletedTuples); qs'' <- UpdateUnConstrRelationDeleteC qs' Ridx DeletedTuples; success qs'' mutated | _, _ => default end).
proof: Proof. intros. unfold QSDelete. rewrite QSMutateSpec_refine_subgoals' with (refined_schConstr_self := ret true) (refined_qsConstr' := ret true); try first [eassumption | reflexivity ]. simplify with monad laws. repeat (f_equiv; unfold pointwise_relation; intros). rewrite <- H0, <- (GetRelDropConstraints qs Ridx), <- H. rewrite refine_SatisfiesTupleConstraintsMutate; eauto. destruct (tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)); f_equiv. rewrite refine_SatisfiesCrossConstraintsMutate; eauto. rewrite <- (GetRelDropConstraints qs Ridx). rewrite <- H1, H; f_equiv. repeat find_if_inside. unfold QSDeletedTuples. f_equiv. rewrite <- (GetRelDropConstraints qs Ridx). unfold GetUnConstrRelation, UpdateUnConstrRelation. rewrite ilist2.ith_replace2_Index_eq, <- H; reflexivity. unfold UpdateUnConstrRelationDeleteC, UpdateUnConstrRelationMutateC; rewrite <- H, GetRelDropConstraints; reflexivity. reflexivity. reflexivity. eauto using QSDeleteSpec_UnConstr_refine_AttributeConstraints. eauto using QSDeleteSpec_UnConstr_refine_CrossConstraints'. intros; eapply H2; eauto. unfold QSDeletedTuples. unfold GetUnConstrRelation, UpdateUnConstrRelation in H7. rewrite ilist2.ith_replace2_Index_eq in H7. rewrite <- GetRelDropConstraints, H in H7; eauto. 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