proposition: Lemma QSInsertSpec_UnConstr_refine : forall qsSchema qs Ridx tup or refined_schConstr_self refined_schConstr refined_schConstr' refined_qsConstr refined_qsConstr', refine {b | decides b (SatisfiesAttributeConstraints Ridx tup)} refined_schConstr_self -> refine {b | decides b (forall tup' : @IndexedElement (@RawTuple (@GetNRelSchemaHeading (numRawQSschemaSchemas (QueryStructureSchemaRaw qsSchema)) (qschemaSchemas (QueryStructureSchemaRaw qsSchema)) _)), GetUnConstrRelation qs Ridx tup' -> SatisfiesTupleConstraints Ridx tup (indexedElement tup'))} refined_schConstr -> refine {b | decides b (forall tup', GetUnConstrRelation qs Ridx tup' -> SatisfiesTupleConstraints Ridx (indexedElement tup') tup)} refined_schConstr' -> refine (@Iterate_Decide_Comp _ (fun Ridx' => SatisfiesCrossRelationConstraints Ridx Ridx' tup (GetUnConstrRelation qs Ridx'))) refined_qsConstr -> (forall idx, refine (@Iterate_Decide_Comp _ (fun Ridx' => Ridx' <> Ridx -> forall tup', (GetUnConstrRelation qs Ridx') tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetUnConstrRelation qs Ridx)))) (refined_qsConstr' idx)) -> @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')) (idx <- {idx | UnConstrFreshIdx (GetUnConstrRelation qs Ridx) idx}; (schConstr_self <- refined_schConstr_self; schConstr <- refined_schConstr; schConstr' <- refined_schConstr'; qsConstr <- refined_qsConstr ; qsConstr' <- (refined_qsConstr' idx); 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)).
proof: Proof. intros. simplify with monad laws. unfold freshIdx. rewrite <- GetRelDropConstraints. unfold DropQSConstraints_AbsR in *; subst. rewrite freshIdx2UnConstr. apply refine_bind_pick; intros. setoid_rewrite <- H; setoid_rewrite <- H0; setoid_rewrite <- H1; setoid_rewrite <- H2; setoid_rewrite <- (H3 a). setoid_rewrite <- (QSInsertSpec_UnConstr_refine' _ {| elementIndex := a; indexedElement := tup |}). repeat setoid_rewrite refineEquiv_bind_bind. setoid_rewrite refineEquiv_bind_unit; simpl. unfold DropQSConstraints_AbsR in *; subst. f_equiv; intros. unfold UnConstrFreshIdx, not in *; intros. apply H4 in H5; simpl in *; omega. reflexivity. 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