proposition: Lemma QSInsertSpec_refine_opt : forall qsSchema (qs : QueryStructure qsSchema) Ridx tup, refine (QSInsert qs Ridx tup) match (attrConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)), (tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)) with Some aConstr, Some tConstr => idx <- {idx | UnConstrFreshIdx (GetRelation qs Ridx) idx} ; (schConstr_self <- {b | decides b (aConstr tup) }; schConstr <- {b | decides b (forall tup', GetRelation qs Ridx tup' -> tConstr tup (indexedElement tup'))}; schConstr' <- {b | decides b (forall tup', GetRelation qs Ridx tup' -> tConstr (indexedElement tup') tup)}; qsConstr <- (@Iterate_Decide_Comp_opt _ (fun Ridx' => match (BuildQueryStructureConstraints qsSchema Ridx Ridx') with | Some CrossConstr => Some (CrossConstr tup (GetRelation qs Ridx')) | None => None end)); qsConstr' <- (@Iterate_Decide_Comp_opt _ (fun Ridx' => If (fin_eq_dec Ridx Ridx') Then None Else match (BuildQueryStructureConstraints qsSchema Ridx' Ridx) with | Some CrossConstr => Some ( forall tup', (GetRelation qs Ridx') tup' -> CrossConstr (indexedElement tup') ( (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetRelation qs Ridx)))) | None => None end)); match schConstr_self, schConstr, schConstr', qsConstr, qsConstr' with | true, true, true, true, true => qs' <- {qs' | (forall Ridx', Ridx <> Ridx' -> GetRelation qs Ridx' = GetRelation qs' Ridx') /\ forall t, GetRelation qs' Ridx t <-> (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetRelation qs Ridx) t)}; ret (qs', true) | _, _, _, _, _ => ret (qs, false) end) | Some aConstr, None => idx <- {idx | UnConstrFreshIdx (GetRelation qs Ridx) idx} ; (schConstr_self <- {b | decides b (aConstr tup) }; qsConstr <- (@Iterate_Decide_Comp_opt _ (fun Ridx' => match (BuildQueryStructureConstraints qsSchema Ridx Ridx') with | Some CrossConstr => Some (CrossConstr tup (GetRelation qs Ridx')) | None => None end)); qsConstr' <- (@Iterate_Decide_Comp_opt _ (fun Ridx' => If (fin_eq_dec Ridx Ridx') Then None Else match (BuildQueryStructureConstraints qsSchema Ridx' Ridx) with | Some CrossConstr => Some ( forall tup', (GetRelation qs Ridx') tup' -> CrossConstr (indexedElement tup') ( (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetRelation qs Ridx)))) | None => None end)); match schConstr_self, qsConstr, qsConstr' with | true, true, true => qs' <- {qs' | (forall Ridx', Ridx <> Ridx' -> GetRelation qs Ridx' = GetRelation qs' Ridx') /\ forall t, GetRelation qs' Ridx t <-> (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetRelation qs Ridx) t)}; ret (qs', true) | _, _, _ => ret (qs, false) end) | None, Some tConstr => idx <- {idx | UnConstrFreshIdx (GetRelation qs Ridx) idx} ; (schConstr <- {b | decides b (forall tup', GetRelation qs Ridx tup' -> tConstr tup (indexedElement tup'))}; schConstr' <- {b | decides b (forall tup', GetRelation qs Ridx tup' -> tConstr (indexedElement tup') tup)}; qsConstr <- (@Iterate_Decide_Comp_opt _ (fun Ridx' => match (BuildQueryStructureConstraints qsSchema Ridx Ridx') with | Some CrossConstr => Some (CrossConstr tup (GetRelation qs Ridx')) | None => None end)); qsConstr' <- (@Iterate_Decide_Comp_opt _ (fun Ridx' => If (fin_eq_dec Ridx Ridx') Then None Else match (BuildQueryStructureConstraints qsSchema Ridx' Ridx) with | Some CrossConstr => Some ( forall tup', (GetRelation qs Ridx') tup' -> CrossConstr (indexedElement tup') ( (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetRelation qs Ridx)))) | None => None end)); match schConstr, schConstr', qsConstr, qsConstr' with | true, true, true, true => qs' <- {qs' | (forall Ridx', Ridx <> Ridx' -> GetRelation qs Ridx' = GetRelation qs' Ridx') /\ forall t, GetRelation qs' Ridx t <-> (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetRelation qs Ridx) t)}; ret (qs', true) | _, _, _, _ => ret (qs, false) end) | None, None => idx <- {idx | UnConstrFreshIdx (GetRelation qs Ridx) idx} ; (qsConstr <- (@Iterate_Decide_Comp_opt _ (fun Ridx' => match (BuildQueryStructureConstraints qsSchema Ridx Ridx') with | Some CrossConstr => Some (CrossConstr tup (GetRelation qs Ridx')) | None => None end)); qsConstr' <- (@Iterate_Decide_Comp_opt _ (fun Ridx' => If (fin_eq_dec Ridx Ridx') Then None Else match (BuildQueryStructureConstraints qsSchema Ridx' Ridx) with | Some CrossConstr => Some ( forall tup', (GetRelation qs Ridx') tup' -> CrossConstr (indexedElement tup') ( (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetRelation qs Ridx)))) | None => None end)); match qsConstr, qsConstr' with | true, true => qs' <- {qs' | (forall Ridx', Ridx <> Ridx' -> GetRelation qs Ridx' = GetRelation qs' Ridx') /\ forall t, GetRelation qs' Ridx t <-> (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetRelation qs Ridx) t)}; ret (qs', true) | _, _ => ret (qs, false) end) end.
proof: Proof. unfold QSInsert. intros; simpl. unfold If_Then_Else. setoid_rewrite QSInsertSpec_refine with (default := ret qs). simplify with monad laws. setoid_rewrite refine_SatisfiesAttributeConstraints_self; simpl. match goal with |- context [attrConstraints ?R] => destruct (attrConstraints R) end. setoid_rewrite refine_SatisfiesTupleConstraints_Constr; simpl. setoid_rewrite refine_SatisfiesTupleConstraints_Constr'; simpl. match goal with |- context [tupleConstraints ?R] => destruct (tupleConstraints R) end. setoid_rewrite refine_SatisfiesCrossConstraints_Constr; simpl. rewrite freshIdx_UnConstrFreshIdx_Equiv. repeat (eapply refine_under_bind; intros). eapply refine_under_bind_both. unfold SatisfiesCrossRelationConstraints; simpl. setoid_rewrite refine_Iterate_Decide_Comp_equiv. eapply refine_Iterate_Decide_Comp. - simpl; intros; simpl in *. destruct (fin_eq_dec Ridx idx); simpl in *; substs; eauto. + congruence. + destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto. - simpl; intros. intro; apply H4. simpl in *; destruct (fin_eq_dec Ridx idx); simpl in *; substs; eauto. + destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto. - intros. repeat setoid_rewrite refine_If_Then_Else_Bind. unfold If_Then_Else. repeat find_if_inside; unfold SuccessfulInsertSpec; try (simplify with monad laws; eapply refine_SuccessfulInsert; eauto). + apply refine_under_bind; intros. refine pick val true; simpl. simplify with monad laws; reflexivity. intros; computes_to_inv; intuition; eapply H7; eauto. - simpl; simplify with monad laws. setoid_rewrite refine_SatisfiesCrossConstraints_Constr; simpl. rewrite freshIdx_UnConstrFreshIdx_Equiv. repeat (eapply refine_under_bind; intros). eapply refine_under_bind_both. unfold SatisfiesCrossRelationConstraints; simpl. setoid_rewrite refine_Iterate_Decide_Comp_equiv. eapply refine_Iterate_Decide_Comp. + simpl; intros; simpl in *. destruct (fin_eq_dec Ridx idx); simpl in *; substs; eauto. * congruence. * destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto. + simpl; intros. intro; apply H2. simpl in *; destruct (fin_eq_dec Ridx idx); simpl in *; substs; eauto. * destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto. + intros. repeat setoid_rewrite refine_If_Then_Else_Bind. unfold If_Then_Else. repeat find_if_inside; unfold SuccessfulInsertSpec; try (simplify with monad laws; eapply refine_SuccessfulInsert; eauto). * apply refine_under_bind; intros. refine pick val true; simpl. simplify with monad laws; reflexivity. intros; computes_to_inv; intuition; eapply H5; eauto. - simplify with monad laws. setoid_rewrite refine_SatisfiesTupleConstraints_Constr; simpl. setoid_rewrite refine_SatisfiesTupleConstraints_Constr'; simpl. match goal with |- context [tupleConstraints ?R] => destruct (tupleConstraints R) end. setoid_rewrite refine_SatisfiesCrossConstraints_Constr; simpl. rewrite freshIdx_UnConstrFreshIdx_Equiv. repeat (eapply refine_under_bind; intros). eapply refine_under_bind_both. unfold SatisfiesCrossRelationConstraints; simpl. setoid_rewrite refine_Iterate_Decide_Comp_equiv. eapply refine_Iterate_Decide_Comp. + simpl; intros; simpl in *. destruct (fin_eq_dec Ridx idx); simpl in *; substs; eauto. * congruence. * destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto. + simpl; intros. intro; apply H3. simpl in *; destruct (fin_eq_dec Ridx idx); simpl in *; substs; eauto. * destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto. + intros. repeat setoid_rewrite refine_If_Then_Else_Bind. unfold If_Then_Else. repeat find_if_inside; unfold SuccessfulInsertSpec; try (simplify with monad laws; eapply refine_SuccessfulInsert; eauto). * apply refine_under_bind; intros. refine pick val true; simpl. simplify with monad laws; reflexivity. intros; computes_to_inv; intuition; eapply H6; eauto. + simpl; simplify with monad laws. setoid_rewrite refine_SatisfiesCrossConstraints_Constr; simpl. rewrite freshIdx_UnConstrFreshIdx_Equiv. repeat (eapply refine_under_bind; intros). eapply refine_under_bind_both. unfold SatisfiesCrossRelationConstraints; simpl. setoid_rewrite refine_Iterate_Decide_Comp_equiv. eapply refine_Iterate_Decide_Comp. * simpl; intros; simpl in *. destruct (fin_eq_dec Ridx idx); simpl in *; substs; eauto. congruence. destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto. * simpl; intros. intro; apply H1. simpl in *; destruct (fin_eq_dec Ridx idx); simpl in *; substs; eauto. destruct (BuildQueryStructureConstraints qsSchema idx Ridx); eauto. * intros. repeat setoid_rewrite refine_If_Then_Else_Bind. unfold If_Then_Else. repeat find_if_inside; unfold SuccessfulInsertSpec; try (simplify with monad laws; eapply refine_SuccessfulInsert; eauto). apply refine_under_bind; intros. refine pick val true; simpl. simplify with monad laws; reflexivity. intros; computes_to_inv; intuition; eapply H4; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.IterateBoundedIndex Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements