proposition: Lemma refine_SatisfiesCrossConstraints'_Constr : forall (qsSchema : QueryStructureSchema) (qs : QueryStructure qsSchema) (Ridx : Fin.t _) tup idx, refine (@Iterate_Decide_Comp _ (fun Ridx' => Ridx' <> Ridx -> forall tup', (GetRelation qs Ridx') tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (EnsembleInsert {| elementIndex := idx; indexedElement := tup |} (GetRelation qs Ridx)))) (@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)).
proof: Proof. intros. setoid_rewrite <- refine_Iterate_Decide_Comp. unfold SatisfiesCrossRelationConstraints. apply refine_Iterate_Decide_Comp_equiv; simpl; intros. simpl in *; destruct (fin_eq_dec Ridx idx0); subst. congruence. destruct (BuildQueryStructureConstraints qsSchema idx0 Ridx); eauto. simpl in *; destruct (fin_eq_dec Ridx idx0); subst; eauto. destruct (BuildQueryStructureConstraints qsSchema idx0 Ridx); eauto. Qed.
imports: Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.Operations.Query Coq.Lists.List Coq.Arith.Compare_dec Coq.Bool.Bool Coq.Strings.String Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.IterateBoundedIndex Fiat.Common.List.ListFacts Fiat.Common.LogicFacts Fiat.Common.DecideableEnsembles Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.Computation.Refinements.General Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Specification.Operations.Mutate