proposition: Lemma refine_Join_Comp_Lists_filter_search_term_fst (ResultT : Type) : forall r_o (r_n : IndexedQueryStructure qs_schema BagIndexKeys) (_ : DelegateToBag_AbsR r_o r_n) idx heading cl (search_pattern : _) (resultComp : ilist2 (B:= @RawTuple) [heading ; _] -> Comp (list ResultT)) (cl_realizable : forall a, exists v, computes_to (cl a) v) filter_rest, refine (l <- CallBagEnumerate idx r_n ; l' <- Join_Comp_Lists (Build_single_Tuple_list (snd l)) cl; List_Query_In (filter (fun a : ilist2 (B:= @RawTuple) [_ ; _] => (BagMatchSearchTerm _ search_pattern (ilist2_hd (ilist2_tl a)) && filter_rest a)) l') resultComp) (l <- CallBagFind idx r_n search_pattern; l' <- Join_Comp_Lists (Build_single_Tuple_list (snd l)) cl; List_Query_In (filter filter_rest l') resultComp).
proof: Proof. intros. setoid_rewrite <- (@refine_BagFind_filter _ _ H idx (BagMatchSearchTerm (ith3 BagIndexKeys idx) search_pattern) search_pattern). intros; unfold CallBagFind, CallBagEnumerate, CallBagMethod; simpl. repeat setoid_rewrite (refineEquiv_bind_bind); repeat setoid_rewrite refineEquiv_bind_unit; simpl. f_equiv; unfold pointwise_relation; intros. let H := match goal with |- refine (l' <- Join_Comp_Lists ?l ?c; (@?f l')) _ => constr:(fun B C => Join_Comp_Lists_apply_f (B := B) (C := C) l c) end in setoid_rewrite H with (c' := fun l => List_Query_In l _). setoid_rewrite <- refineEquiv_unit_bind. setoid_rewrite (filter_and_join_ilist_tail (fun a0 : ilist2 (B:= @RawTuple) [_] =>_ (ilist2_hd a0)) (Build_single_Tuple_list a)); eauto. simplify with monad laws; f_equiv. unfold Build_single_Tuple_list; simpl; repeat rewrite ListFacts.filter_map; f_equiv. setoid_rewrite refineEquiv_bind_bind; setoid_rewrite refineEquiv_unit_bind; reflexivity. intro; 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