proposition: Lemma refine_BagFindBag_single {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 (For (UnConstrQuery_In r_o idx (fun tup => Where (P tup) Return (f tup)))) (r_n' <- CallBagFind qs_schema BagIndexKeys idx r_n search_term; ret (map f (snd r_n'))).
proof: Proof. intros. rewrite refine_For. etransitivity. apply refine_under_bind_both. etransitivity. apply refine_Filtered_Query_In_Enumerate; eauto. apply refine_under_bind; intros. match goal with | [H : @DelegateToBag_AbsR ?qs_schema ?indexes ?r_o ?r_n |- refine (List_Query_In ?b (fun b' : ?QueryT => Where (@?P b') (@?resultComp b'))) _ ] => etransitivity; [ let H' := eval simpl in (@refine_List_Query_In_Where QueryT _ b P resultComp) in pose proof H' | ] end. eapply (H2 {| DecideableEnsembles.dec := fun tup => DecideableEnsembles.dec (prim_fst tup) |}). simpl. finish honing. intros; finish honing. simpl. etransitivity. apply refine_under_bind_both. apply (fun heading => @refine_Join_Filtered_Comp_Lists_filter_tail _ heading [ ]%vector); intros. intros; finish honing. simpl. setoid_rewrite Join_Filtered_Comp_Lists_ExtensionalEq_filters; [ | unfold ExtensionalEq in *; intros [? ?]; simpl; rewrite H0; instantiate (1 := fun tup => BagMatchSearchTerm (ith3 BagIndexKeys idx) search_term (ilist2_hd tup) && true); simpl; rewrite andb_true_r; eauto ]. rewrite (@refine_Join_Comp_Lists_To_Find _ _ 0 _ _ H [ ]%vector). simplify with monad laws. unfold Join_Comp_Lists; simpl. unfold CallBagFind, CallBagCount; autorewrite with monad laws. f_equiv; intro. simpl. rewrite app_nil_r. rewrite (List_Query_In_Return _ (map (fun fa : RawTuple => icons2 fa inil2) a) (fun tup => f (prim_fst tup))). simplify with monad laws. refine pick val _. reflexivity. simpl. rewrite Permutation_map. 2: reflexivity. rewrite map_map; simpl. induction a; simpl; eauto. Unshelve. simpl. intro; rewrite dec_decides_P; 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