proposition: Corollary refine_Join_Filtered_Comp_Lists_filter_tail : forall n heading headings (f : ilist2 (n := S n) (B := @RawTuple) (heading :: headings) -> bool) (ResultT : Type) (resultComp : ilist2 (B := @RawTuple) (heading :: headings) -> Comp (list ResultT)) (l2 : ilist2 (B := @RawTuple) headings -> Comp (list RawTuple)) (cond : ilist2 (B := @RawTuple) (heading :: headings) -> bool), forall l1 : list (ilist2 (B := @RawTuple) headings), refine (l' <- Join_Filtered_Comp_Lists l1 l2 cond; List_Query_In (filter f l') resultComp) (l' <- Join_Filtered_Comp_Lists l1 l2 (fun a => cond a && f a); List_Query_In l' resultComp).
proof: Proof. intros; pose proof (@refine_Join_Filtered_Comp_Lists_filter_tail_andb _ _ _ f (fun _ => true) _ resultComp l2 cond l1) as r. setoid_rewrite filter_true in r. intros v Comp_v. apply r in Comp_v. computes_to_inv; subst. rewrite filter_and, filter_true in Comp_v'. 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