proposition: Lemma QSInsertSpec_UnConstr_refine_opt : forall qsSchema qs or (Ridx : Fin.t _) tup, @DropQSConstraints_AbsR qsSchema or qs -> refine (or' <- (idx <- Pick (freshIdx or Ridx); qs' <- Pick (QSInsertSpec or Ridx {| elementIndex := idx; indexedElement := tup |}); b <- Pick (SuccessfulInsertSpec or Ridx qs' {| elementIndex := idx; indexedElement := tup |}); ret (qs', b)); nr' <- {nr' | DropQSConstraints_AbsR (fst or') nr'}; ret (nr', snd or')) match (attrConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)), (tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)) with Some aConstr, Some tConstr => idx <- {idx | UnConstrFreshIdx (GetUnConstrRelation qs Ridx) idx} ; (schConstr_self <- {b | decides b (aConstr tup) }; schConstr <- {b | decides b (forall tup', GetUnConstrRelation qs Ridx tup' -> tConstr tup (indexedElement tup'))}; schConstr' <- {b | decides b (forall tup', GetUnConstrRelation 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 (GetUnConstrRelation 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', (GetUnConstrRelation qs Ridx') tup' -> CrossConstr (indexedElement tup') ( (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetUnConstrRelation qs Ridx)))) | None => None end)); match schConstr_self, schConstr, schConstr', qsConstr, qsConstr' with | true, true, true, true, true => ret (UpdateUnConstrRelation qs Ridx (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetUnConstrRelation qs Ridx)), true) | _, _, _, _, _ => ret (qs, false) end) | Some aConstr, None => idx <- {idx | UnConstrFreshIdx (GetUnConstrRelation 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 (GetUnConstrRelation 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', (GetUnConstrRelation qs Ridx') tup' -> CrossConstr (indexedElement tup') ( (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetUnConstrRelation qs Ridx)))) | None => None end)); match schConstr_self, qsConstr, qsConstr' with | true, true, true => ret (UpdateUnConstrRelation qs Ridx (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetUnConstrRelation qs Ridx)), true) | _, _, _ => ret (qs, false) end) | None, Some tConstr => idx <- {idx | UnConstrFreshIdx (GetUnConstrRelation qs Ridx) idx} ; (schConstr <- {b | decides b (forall tup', GetUnConstrRelation qs Ridx tup' -> tConstr tup (indexedElement tup'))}; schConstr' <- {b | decides b (forall tup', GetUnConstrRelation 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 (GetUnConstrRelation 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', (GetUnConstrRelation qs Ridx') tup' -> CrossConstr (indexedElement tup') ( (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetUnConstrRelation qs Ridx)))) | None => None end)); match schConstr, schConstr', qsConstr, qsConstr' with | true, true, true, true => ret (UpdateUnConstrRelation qs Ridx (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetUnConstrRelation qs Ridx)), true) | _, _, _, _ => ret (qs, false) end) | None, None => idx <- {idx | UnConstrFreshIdx (GetUnConstrRelation qs Ridx) idx} ; (qsConstr <- (@Iterate_Decide_Comp_opt _ (fun Ridx' => match (BuildQueryStructureConstraints qsSchema Ridx Ridx') with | Some CrossConstr => Some (CrossConstr tup (GetUnConstrRelation 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', (GetUnConstrRelation qs Ridx') tup' -> CrossConstr (indexedElement tup') ( (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetUnConstrRelation qs Ridx)))) | None => None end)); match qsConstr, qsConstr' with | true, true => ret (UpdateUnConstrRelation qs Ridx (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetUnConstrRelation qs Ridx)), true) | _, _ => ret (qs, false) end) end.
proof: Proof. unfold QSInsert. intros; rewrite QSInsertSpec_UnConstr_refine; eauto using refine_SatisfiesAttributeConstraints_self, refine_SatisfiesTupleConstraints, refine_SatisfiesTupleConstraints', refine_SatisfiesCrossConstraints; [ | intros; eapply refine_SatisfiesCrossConstraints']. destruct (attrConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)); destruct (tupleConstraints (GetNRelSchema (qschemaSchemas qsSchema) Ridx)). - reflexivity. - f_equiv; unfold pointwise_relation; intros. repeat setoid_rewrite refineEquiv_bind_bind. repeat setoid_rewrite refineEquiv_bind_unit; f_equiv. - f_equiv; unfold pointwise_relation; intros. repeat setoid_rewrite refineEquiv_bind_bind. repeat setoid_rewrite refineEquiv_bind_unit; f_equiv. - f_equiv; unfold pointwise_relation; intros. repeat setoid_rewrite refineEquiv_bind_bind. repeat setoid_rewrite refineEquiv_bind_unit; f_equiv. 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