proposition: Lemma refine_Join_Comp_Lists_filter_tail_cond : forall n heading headings (f : ilist2 (n := n) (B := @RawTuple) (headings) -> bool) (filter_rest : ilist2 (B := @RawTuple) (heading :: headings) -> bool) (ResultT : Type) (resultComp : _ -> Comp (list ResultT)) (l1 : list (ilist2 (B := @RawTuple) headings)) (l2 : ilist2 (B := @RawTuple) headings -> Comp (list (@RawTuple heading))), (forall a : ilist2 (B := @RawTuple) headings, List.In a l1 -> exists v : list (@RawTuple heading), refine (l2 a) (ret v)) -> refine (l' <- Join_Comp_Lists l1 l2; List_Query_In (filter (fun (a : ilist2 (B := @RawTuple) (heading :: headings)) => f (ilist2_tl a) && (filter_rest a)) l') resultComp) (l' <- Join_Comp_Lists (filter f l1) l2; List_Query_In (filter filter_rest l') resultComp).
proof: Proof. unfold Join_Comp_Lists; induction l1; simpl; intros; simplify with monad laws. - setoid_rewrite refineEquiv_bind_unit; reflexivity. - case_eq (f a); simpl; intros a_eq v Comp_v. + computes_to_inv; subst; computes_to_econstructor; eauto. rewrite filter_app, filter_map in Comp_v'. unfold List_Query_In in Comp_v'. rewrite map_app, map_map in Comp_v'. apply flatten_CompList_app_inv' in Comp_v'. destruct_ex; split_and. pose (IHl1 l2 (fun a In_a => H _ (or_intror In_a)) _ (BindComputes _ _ _ _ Comp_v'0 H3)); computes_to_inv; subst. computes_to_econstructor; eauto. unfold List_Query_In. repeat rewrite filter_app, filter_map. repeat rewrite map_app, map_map; simpl. rewrite filter_and, a_eq, filter_true. eapply FlattenCompList.flatten_CompList_app; eauto. + destruct (H a); eauto. computes_to_inv; subst; computes_to_econstructor; eauto. pose (IHl1 l2 (fun a In_a => H _ (or_intror In_a)) _ (BindComputes _ _ _ _ Comp_v Comp_v')); computes_to_inv; subst. computes_to_econstructor; eauto. unfold List_Query_In. repeat rewrite filter_app, filter_map. repeat rewrite map_app, map_map; simpl. rewrite filter_and, a_eq, filter_false; simpl; eauto. Qed.
imports: Coq.Arith.Arith Coq.ZArith.ZArith Coq.NArith.NArith Coq.ZArith.ZArith Coq.Strings.String Coq.Lists.List Coq.Sorting.Permutation Coq.Bool.Bool Coq.Sets.Ensembles Coq.Logic.FunctionalExtensionality Fiat.ADTNotation Fiat.Common Fiat.Common.ilist2 Fiat.Common.List.ListFacts Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Computation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure