proposition: Lemma refine_constraint_check_into_query'' : forall heading R P' P (P_dec : DecideableEnsemble P), Same_set _ (fun tup => P (indexedElement tup)) P' -> refine (Pick (fun (b : bool) => decides b (exists tup2: @IndexedRawTuple heading, (R tup2 /\ P' tup2)))) (Bind (Count (For (QueryResultComp R (fun tup => Where (P tup) Return tup)))) (fun count => ret (negb (Nat.eqb count 0)))).
proof: Proof. Local Transparent Count. unfold refine, Count, UnConstrQuery_In; intros * excl * P_iff_P' pick_comp ** . computes_to_inv; subst. computes_to_constructor. destruct (Datatypes.length v0) eqn:eq_length; destruct v0 as [ | head tail ]; simpl in *; try discriminate; simpl. pose proof (For_computes_to_nil _ R H). rewrite not_exists_forall; intro a; rewrite not_and_implication; intros. unfold not; intros; eapply H0; eauto; apply P_iff_P'; eauto. apply For_computes_to_In with (x := head) in H; try solve [intuition]. destruct H as ( p & [ x0 ( in_ens & _eq ) ] ); subst. eexists; split; eauto; apply P_iff_P'; eauto. apply decidable_excl; assumption. 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