proposition: Lemma refine_Join_Join_Filtered_Comp_Lists_filter_hd_andb : forall n heading1 heading2 headings (f : ilist2 (n := n) (B := @RawTuple) headings -> bool) (g : ilist2 (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 a : ilist2 (B := @RawTuple) headings, exists v : list RawTuple, refine (l2 a) (ret v)) -> forall l1 : list (ilist2 (B := @RawTuple) headings), refine (l <- Join_Filtered_Comp_Lists l1 l2 cond1; Join_Filtered_Comp_Lists (filter (fun a : ilist2 (B := @RawTuple) (_ :: _) => f (ilist2_tl a) && g a) l) l2' cond2) (l <- Join_Filtered_Comp_Lists (filter f l1) l2 cond1; Join_Filtered_Comp_Lists (filter g l) l2' cond2).
proof: Proof. intros; revert l2 l2' cond1 cond2 H. unfold Join_Filtered_Comp_Lists, Join_Comp_Lists; induction l1; simpl; intros; simplify with monad laws. - repeat setoid_rewrite refineEquiv_bind_unit; simpl; 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, !map_app, !map_map in Comp_v'. apply FlattenCompList.flatten_CompList_app_inv' in Comp_v'. destruct_ex; split_and; subst. assert (computes_to (l <- l <- FlattenCompList.flatten_CompList (map (fun l' : ilist2 (B := @RawTuple) headings => l <- l2 l'; ret (map (fun fa : RawTuple => icons2 fa l') l)) (filter f l1)); ret (filter cond1 l); l0 <- FlattenCompList.flatten_CompList (map (fun l' : ilist2 (B := @RawTuple) (heading1 :: headings) => l0 <- l2' l'; ret (map (fun fa : RawTuple => icons2 fa l') l0)) (filter g l)); ret (filter cond2 l0)) (filter cond2 x0)) as H' by (repeat computes_to_econstructor; eauto). pose (IHl1 l2 l2' cond1 cond2 H _ H'); computes_to_inv; subst. computes_to_econstructor; eauto. computes_to_econstructor. 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. rewrite !filter_app, <- c''; eauto. + destruct (H a); eauto. computes_to_inv; subst; computes_to_econstructor; eauto. assert (computes_to (l <- l <- FlattenCompList.flatten_CompList (map (fun l' : ilist2 (B := @RawTuple) headings => l <- l2 l'; ret (map (fun fa : RawTuple => icons2 fa l') l)) (filter f l1)); ret (filter cond1 l); l0 <- FlattenCompList.flatten_CompList (map (fun l' : ilist2 (B := @RawTuple) (heading1 :: headings) => l0 <- l2' l'; ret (map (fun fa : RawTuple => icons2 fa l') l0)) (filter g l)); ret (filter cond2 l0)) (filter cond2 v1)) as H' by (repeat econstructor; eauto). pose (IHl1 l2 l2' cond1 cond2 H _ H'); computes_to_inv; subst. computes_to_econstructor; eauto. computes_to_econstructor. repeat rewrite filter_app, filter_map. repeat rewrite map_app, map_map; simpl. rewrite a_eq, filter_false; simpl; eauto. rewrite <- c''; 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