proposition: Lemma refine_Join_Comp_Lists_filter_search_term_snd_dep {n} (ResultT : Type) : forall r_o (r_n : IndexedQueryStructure qs_schema BagIndexKeys) (_ : DelegateToBag_AbsR r_o r_n) (headings : Vector.t _ n) idx' (search_pattern : _ -> _) (resultComp : ilist2 (B:= @RawTuple) (_ :: headings) -> Comp (list ResultT)) filter_rest (cl : list (ilist2 (B:= @RawTuple) headings)), refine (l' <- (Join_Comp_Lists cl (fun _ => l <- CallBagEnumerate idx' r_n ; ret (snd l))); List_Query_In (filter (fun a : ilist2 (B:= @RawTuple) (_ :: headings) => BagMatchSearchTerm _ (search_pattern (ilist2_tl a)) (ilist2_hd a) && filter_rest a) l') resultComp) (l' <- (Join_Comp_Lists cl (fun tup => l <- CallBagFind idx' r_n (search_pattern tup); ret (snd l))); List_Query_In (filter filter_rest l') resultComp).
proof: Proof. intros; unfold CallBagMethod; simpl. etransitivity; [ | rewrite <- refine_Join_Comp_Lists; [reflexivity | intro; setoid_rewrite <- (@refine_BagFind_filter _ _ H idx' (BagMatchSearchTerm (ith3 BagIndexKeys idx') (search_pattern a)) (search_pattern a)); [finish honing | intro; reflexivity] ] ]. repeat setoid_rewrite (refineEquiv_bind_bind); repeat setoid_rewrite refineEquiv_bind_unit; simpl. match goal with |- refine (l' <- @Join_Comp_Lists ?n ?A ?f ?As ?a ?l ?c ; _) _ => pose proof (fun B C => @Join_Comp_Lists_apply_f n A B C f As a l c) as H''; setoid_rewrite H'' end. setoid_rewrite refineEquiv_unit_bind. etransitivity. 2: unfold List_Query_In; etransitivity. Focus 3. apply refine_under_bind. intros; set_evars. rewrite <- refineEquiv_bind_unit with (f := fun x => flatten_CompList (map resultComp x)) (x := filter filter_rest a). unfold H1; finish honing. Focus 2. simpl. rewrite <- refine_bind_bind. rewrite <- filter_and_join_ilist2_hd_dep with (f := fun tup => (BagMatchSearchTerm (ith3 BagIndexKeys idx') (search_pattern tup))) (filter_rest0 := filter_rest). finish honing. simplify with monad laws. rewrite refineEquiv_bind_bind. setoid_rewrite refineEquiv_bind_unit. f_equiv. 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