proposition: Lemma refine_Join_Comp_Lists_To_Find {n} : forall r_o (r_n : IndexedQueryStructure qs_schema BagIndexKeys), DelegateToBag_AbsR r_o r_n -> forall {headings} (l1 : list (ilist2 (n := n) (B:= @RawTuple) headings)) (idx : Fin.t _) search_pattern, refine (Join_Filtered_Comp_Lists l1 (fun _ => l <- CallBagEnumerate idx r_n ; ret (snd l)) (fun a => BagMatchSearchTerm (ith3 BagIndexKeys idx) search_pattern (ilist2_hd a) && true)) (Join_Comp_Lists l1 (fun _ => l <- CallBagFind idx r_n search_pattern; ret (snd l))) .
proof: Proof. unfold Join_Filtered_Comp_Lists, Join_Comp_Lists; intros; simpl. induction l1. - simpl; simplify with monad laws; reflexivity. - Local Transparent CallBagMethod. simpl. setoid_rewrite refineEquiv_bind_bind. setoid_rewrite refineEquiv_bind_bind. etransitivity; [ | apply refine_bind; [ eapply (@refine_BagFind_filter _ _ H idx (BagMatchSearchTerm (ith3 BagIndexKeys idx) search_pattern) search_pattern); unfold ExtensionalEq; intuition | unfold pointwise_relation; intros; finish honing] ]. setoid_rewrite refineEquiv_bind_bind. setoid_rewrite refineEquiv_bind_bind at 1. setoid_rewrite refineEquiv_bind_bind at 1. setoid_rewrite refineEquiv_bind_bind at 1. repeat setoid_rewrite refineEquiv_bind_unit; simpl; f_equiv; intro. intros v Comp_v. computes_to_inv; subst. generalize (IHl1 _ Comp_v); intros; computes_to_inv. computes_to_econstructor; subst; eauto. rewrite filter_app, ListFacts.filter_map. simpl. erewrite filter_by_equiv; eauto. unfold ExtensionalEq; intros; rewrite andb_true_r; auto. 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