proposition: Lemma refine_BagFindBagCount {ResultT} : forall qs_schema BagIndexKeys idx r_o r_n search_term P (f : _ -> ResultT) (P_dec : DecideableEnsemble P), @DelegateToBag_AbsR qs_schema BagIndexKeys r_o r_n -> ExtensionalEq DecideableEnsembles.dec (BagMatchSearchTerm (ith3 BagIndexKeys idx) search_term) -> refine (Count For (UnConstrQuery_In r_o idx (fun tup => Where (P tup) Return (f tup)))) (r_n' <- CallBagCount idx r_n search_term; ret (snd r_n')).
proof: Proof. intros. rewrite refine_Count, refine_BagFindBag_single; eauto. rewrite !refine_bind_bind. unfold CallBagFind, CallBagCount; autorewrite with monad laws. f_equiv; intro. simpl. rewrite !map_length; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist2 Fiat.Common.i2list Fiat.Common.ilist3 Fiat.Common.i3list Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.String_as_OT Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements