proposition: Lemma refine_Join_Query_In_Enumerate' {n} headings (ResultT : Type) : forall r_o (r_n : IndexedQueryStructure qs_schema BagIndexKeys), DelegateToBag_AbsR r_o r_n -> forall (idx : Fin.t _) (resultComp : ilist2 (n := n) (B:= @RawTuple) headings -> RawTuple -> Comp (list ResultT)) l, refine (List_Query_In l (fun tup : ilist2 (B := @RawTuple) headings => UnConstrQuery_In r_o idx (resultComp tup))) (l' <- (Join_Comp_Lists l (fun _ => l <- (CallBagEnumerate idx r_n); ret (snd l))); List_Query_In l' (fun tup_pair => (resultComp (ilist2_tl tup_pair) (ilist2_hd tup_pair)))).
proof: Proof. intros. unfold List_Query_In; induction l; unfold Join_Comp_Lists; simpl. - intros v Comp_v; computes_to_inv; subst; eauto. - setoid_rewrite IHl; rewrite refine_Query_In_Enumerate; eauto. unfold List_Query_In. setoid_rewrite refineEquiv_bind_bind at 1. setoid_rewrite refineEquiv_bind_bind at 2. intros v Comp_v; computes_to_inv. subst. rewrite map_app, map_map in Comp_v'; simpl in *. computes_to_econstructor; eauto. apply flatten_CompList_app_inv' in Comp_v'; destruct_ex; intuition. subst; repeat (computes_to_econstructor; eauto). unfold Build_single_Tuple_list in *. rewrite !map_app, !map_map, app_nil_r; simpl; eauto. 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