proposition: Lemma refine_Join_Join_Filtered_Comp_Lists_filter_tail_andb : forall n heading1 heading2 headings (f g : ilist2 (n := S n) (B := @RawTuple) (heading1 :: headings) -> bool) (l2 : ilist2 (B := @RawTuple) headings -> Comp (list RawTuple)) (l2' : ilist2 (B := @RawTuple) (heading1 :: headings) -> Comp (list RawTuple)) (cond1 : ilist2 (B := @RawTuple) (heading1 :: headings) -> bool) (cond2 : ilist2 (B := @RawTuple) (heading2 :: heading1 :: headings) -> bool), forall l1 : list (ilist2 (B := @RawTuple) headings), refine (l <- Join_Filtered_Comp_Lists l1 l2 cond1; Join_Filtered_Comp_Lists (filter (fun a => f a && g a) l) l2' cond2) (l <- Join_Filtered_Comp_Lists l1 l2 (fun a => cond1 a && f a); Join_Filtered_Comp_Lists (filter g l) l2' cond2).
proof: Proof. intros; revert l2 l2'. unfold Join_Filtered_Comp_Lists, Join_Comp_Lists; induction l1; simpl; intros; simplify with monad laws. - repeat setoid_rewrite refineEquiv_bind_unit; simpl; reflexivity. - repeat setoid_rewrite refineEquiv_bind_bind. repeat setoid_rewrite refineEquiv_bind_unit. repeat setoid_rewrite <- filter_and. repeat (f_equiv; intro). setoid_rewrite andb_assoc. 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