proposition: Lemma QSInsertSpec_refine_subgoals_short_circuit ResultT : forall qsSchema (qs : QueryStructure qsSchema) qs' Ridx tup default success refined_schConstr_self refined_schConstr refined_schConstr' refined_qsConstr refined_qsConstr' (k : _ -> Comp ResultT), DropQSConstraints_AbsR qs qs' -> refine {b | decides b (SatisfiesAttributeConstraints Ridx tup)} refined_schConstr_self -> refine {b | decides b (forall tup', GetUnConstrRelation qs' Ridx tup' -> SatisfiesTupleConstraints Ridx tup (indexedElement tup'))} refined_schConstr -> (forall b', decides b' (forall tup', GetUnConstrRelation qs' Ridx tup' -> SatisfiesTupleConstraints Ridx tup (indexedElement tup')) -> refine {b | decides b (forall tup', GetUnConstrRelation qs' Ridx tup' -> SatisfiesTupleConstraints Ridx (indexedElement tup') tup)} (refined_schConstr' b')) -> refine (@Iterate_Decide_Comp.Iterate_Decide_Comp_opt _ (fun Ridx' => match (BuildQueryStructureConstraints qsSchema Ridx Ridx') with | Some CrossConstr => Some (CrossConstr tup (GetUnConstrRelation qs' Ridx')) | None => None end)) refined_qsConstr -> (forall idx, UnConstrFreshIdx (GetUnConstrRelation qs' Ridx) idx -> refine (@Iterate_Decide_Comp.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)) (refined_qsConstr' idx)) -> (forall idx qs' qs'', DropQSConstraints_AbsR qs' qs'' -> UnConstrFreshIdx (GetRelation qs Ridx) idx -> (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)) -> refine (k (qs', true)) (success qs'')) -> refine (k (qs, false)) default -> refine (qs' <- QSInsert qs Ridx tup; k qs') (idx <- {idx | UnConstrFreshIdx (GetUnConstrRelation qs' Ridx) idx} ; schConstr_self <- refined_schConstr_self; If schConstr_self Then schConstr <- refined_schConstr; If schConstr Then schConstr' <- refined_schConstr' schConstr; If schConstr' Then qsConstr <- refined_qsConstr; If qsConstr Then qsConstr' <- refined_qsConstr' idx; If qsConstr' Then qs'' <- UpdateUnConstrRelationInsertC qs' Ridx {| elementIndex := idx; indexedElement := tup |}; success qs'' Else default Else default Else default Else default Else default ).
proof: Proof. intros; unfold QSInsert. simplify with monad laws. setoid_rewrite QSInsertSpec_refine_short_circuit with (default := ret qs). rewrite freshIdx_UnConstrFreshIdx_Equiv. simplify with monad laws. rewrite <- !H, (GetRelDropConstraints qs). apply refine_under_bind_both; [reflexivity | intros]. apply refine_under_bind_both; [eassumption | intros]. rewrite refine_If_Then_Else_Bind. eapply refine_if; intros; subst; simpl; try simplify with monad laws. apply refine_under_bind_both; [eauto | intros]. rewrite <- H1; simpl. rewrite <- (GetRelDropConstraints qs), H; reflexivity. rewrite refine_If_Then_Else_Bind. eapply refine_if; intros; subst; simpl; try simplify with monad laws. apply refine_under_bind_both; [eauto | intros]. rewrite <- H2; simpl. rewrite <- (GetRelDropConstraints qs), H; reflexivity. computes_to_inv; simpl in *; eauto. rewrite <- !GetRelDropConstraints in H9; rewrite !H in H9. eauto. rewrite refine_If_Then_Else_Bind. eapply refine_if; intros; subst; simpl; try simplify with monad laws. apply refine_under_bind_both; [eauto | intros]. rewrite <- H3; simpl. etransitivity. apply refine_SatisfiesCrossConstraints_Constr. f_equiv. apply functional_extensionality; intro. destruct (BuildQueryStructureConstraints qsSchema Ridx x). rewrite <- (GetRelDropConstraints qs), H; reflexivity. reflexivity. rewrite refine_If_Then_Else_Bind. eapply refine_if; intros; subst; simpl; try simplify with monad laws. apply refine_under_bind_both; [eauto | intros]. rewrite <- H4; simpl. etransitivity. apply refine_SatisfiesCrossConstraints'_Constr. f_equiv. apply functional_extensionality; intro. simpl. find_if_inside; eauto. destruct (BuildQueryStructureConstraints qsSchema x Ridx). rewrite <- (GetRelDropConstraints qs), H. rewrite <- (GetRelDropConstraints qs), H. reflexivity. reflexivity. computes_to_inv; simpl in *; subst. rewrite <- H, (GetRelDropConstraints qs); eauto. rewrite refine_If_Then_Else_Bind. eapply refine_if. simpl in *; intros; subst; simpl; computes_to_inv; simpl in *. assert (forall tup' : IndexedElement, GetRelation qs Ridx tup' -> SatisfiesTupleConstraints (qsSchema := qsSchema) Ridx (indexedElement {| elementIndex := a; indexedElement := tup |}) (indexedElement tup')) as H9' by (intros; apply H9; try rewrite <- H, GetRelDropConstraints; eassumption). assert (forall Ridx' : Fin.t (numRawQSschemaSchemas qsSchema), Ridx' <> Ridx -> forall tup' : IndexedElement, GetRelation qs Ridx' tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (EnsembleInsert {| elementIndex := a; indexedElement := tup |} (GetRelation qs Ridx))) as H12' by (apply Iterate_Decide_Comp_BoundedIndex in H12; computes_to_inv; subst; simpl in *; apply H12). assert (forall tup' : IndexedElement, GetRelation qs Ridx tup' -> SatisfiesTupleConstraints (qsSchema := qsSchema) Ridx (indexedElement tup') (indexedElement {| elementIndex := a; indexedElement := tup |})) as H10' by (intros; apply H10; try rewrite <- H, GetRelDropConstraints; eassumption). assert (forall Ridx' : Fin.t (numRawQSschemaSchemas qsSchema), SatisfiesCrossRelationConstraints (qsSchema := qsSchema) Ridx Ridx' (indexedElement {| elementIndex := a; indexedElement := tup |}) (GetRelation qs Ridx')) as H11'. (apply Iterate_Decide_Comp_BoundedIndex in H11; computes_to_inv; subst; simpl in *; apply H11). refine pick val (Insert_Valid qs {| elementIndex := a; indexedElement := tup |} H9' H10' H8 H11' H12'). simplify with monad laws. refine pick val true. unfold UpdateUnConstrRelationInsertC. simplify with monad laws. setoid_rewrite refineEquiv_bind_unit. eapply H5. rewrite H. unfold DropQSConstraints_AbsR, DropQSConstraints, Insert_Valid; simpl. unfold UpdateRelation. rewrite ilist2.imap_replace2_Index; try reflexivity. simpl. unfold UpdateUnConstrRelation; simpl. rewrite <- H. rewrite GetRelDropConstraints; reflexivity. apply H7. intros. intros; unfold Insert_Valid, GetRelation, UpdateRelation; simpl. simpl. rewrite ilist2.ith_replace2_Index_neq; simpl; eauto. intros; unfold Insert_Valid, GetRelation, UpdateRelation; simpl. rewrite ilist2.ith_replace2_Index_eq; simpl; reflexivity. unfold SuccessfulInsertSpec; simpl. unfold Insert_Valid, GetRelation, UpdateRelation; simpl. rewrite ilist2.ith_replace2_Index_eq; simpl; reflexivity. split; intros. unfold Insert_Valid, GetRelation, UpdateRelation; simpl. rewrite ilist2.ith_replace2_Index_neq; simpl; eauto. rewrite <- GetRelDropConstraints. unfold Insert_Valid, GetRelation, UpdateRelation; simpl. unfold DropQSConstraints, GetUnConstrRelation; simpl. rewrite ilist2.imap_replace2_Index; simpl. rewrite ilist2.ith_replace2_Index_eq; simpl; reflexivity. intros; subst; computes_to_inv; simpl. simplify with monad laws. refine pick val _; try simplify with monad laws; eauto. unfold SuccessfulInsertSpec. computes_to_inv; simpl in *; subst. intro. pose proof (proj2 (H13 _) (or_introl (eq_refl _))). apply H7 in H14; simpl in H14; omega. refine pick val _; try simplify with monad laws; eauto. unfold SuccessfulInsertSpec. computes_to_inv; simpl in *; subst. intro. pose proof (proj2 (H12 _) (or_introl (eq_refl _))). apply H7 in H13; simpl in H13; omega. refine pick val _; try simplify with monad laws; eauto. unfold SuccessfulInsertSpec. computes_to_inv; simpl in *; subst. intro. pose proof (proj2 (H11 _) (or_introl (eq_refl _))). apply H7 in H12; simpl in H12; omega. refine pick val _; try simplify with monad laws; eauto. unfold SuccessfulInsertSpec. computes_to_inv; simpl in *; subst. intro. pose proof (proj2 (H10 _) (or_introl (eq_refl _))). apply H7 in H11; simpl in H11; omega. refine pick val _; try simplify with monad laws; eauto. unfold SuccessfulInsertSpec. computes_to_inv; simpl in *; subst. intro. pose proof (proj2 (H9 _) (or_introl (eq_refl _))). apply H7 in H10; simpl in H10; omega. 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