proposition: Lemma refine_functional_dependency_check_into_query : forall {schm : RawQueryStructureSchema} {tbl} (ref : @RawTuple (@GetNRelSchemaHeading _ (qschemaSchemas schm) tbl)) args1 args2 (c : UnConstrQueryStructure schm), DecideableEnsemble (fun x : RawTuple => tupleAgree_computational ref x args1 /\ ~ tupleAgree_computational ref x args2) -> ((forall tup' : IndexedRawTuple, GetUnConstrRelation c tbl tup' -> FunctionalDependency_P args2 args1 ref (indexedElement tup')) <-> (forall tup', ~ (GetUnConstrRelation c tbl tup' /\ tupleAgree ref (indexedElement tup') args1 /\ ~ tupleAgree ref (indexedElement tup') args2))) -> refine (Pick (fun (b : bool) => decides b (forall tup', GetUnConstrRelation c tbl tup' -> FunctionalDependency_P args2 args1 ref (indexedElement tup')))) (Bind (Count For (UnConstrQuery_In c tbl (fun tup => Where (tupleAgree_computational ref tup args1 /\ ~ tupleAgree_computational ref tup args2) Return tup))) (fun count => ret (Nat.eqb count 0))).
proof: Proof. intros * is_dec ** . setoid_replace (forall tup', GetUnConstrRelation c tbl tup' -> tupleAgree ref (indexedElement tup') args1 -> tupleAgree ref (indexedElement tup') args2) with (forall tup', ~ (GetUnConstrRelation c tbl tup' /\ tupleAgree ref (indexedElement tup') args1 /\ ~ tupleAgree ref (indexedElement tup') args2)); eauto. setoid_rewrite refine_decide_negation. setoid_rewrite (tupleAgree_equivalence ref). setoid_rewrite (@refine_constraint_check_into_query _ _ (fun x => tupleAgree_computational ref x args1 /\ ~ tupleAgree_computational ref x args2)); try assumption. Opaque Query_For Count. simplify with monad laws. setoid_rewrite negb_involutive. reflexivity. 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