proposition: Lemma refine_uniqueness_check_into_query' : forall {schm : RawQueryStructureSchema} idx tup attr (c : UnConstrQueryStructure schm), Query_eq (Domain (GetNRelSchemaHeading (qschemaSchemas schm) idx) attr) -> refine {b | decides b (forall tup' : @IndexedRawTuple _, GetUnConstrRelation c idx tup' -> UniqueAttribute' attr tup (indexedElement tup'))} (c <- (Count For (UnConstrQuery_In c idx (fun tup' => Where (GetAttributeRaw tup attr = GetAttributeRaw tup' attr) Return tup'))); (ret (Nat.eqb c 0))).
proof: Proof. intros. setoid_replace (forall tup', GetUnConstrRelation c idx tup' -> UniqueAttribute' attr tup (indexedElement tup')) with (forall tup', ~ (GetUnConstrRelation c idx tup' /\ GetAttributeRaw tup attr = GetAttributeRaw (indexedElement tup') attr)) by (unfold UniqueAttribute'; intuition eauto). setoid_rewrite refine_decide_negation. rewrite (@refine_constraint_check_into_query _ _ (fun tup' => GetAttributeRaw tup attr = GetAttributeRaw tup' attr)) by eauto with typeclass_instances. 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