proposition: Lemma filter_and_join_ilist2_hd_dep {n} {A} {a} {As : Vector.t A n} (f' : A -> Type) : forall (f : ilist2 (B := f') As -> f' a -> bool) (s1 : list (ilist2 (B := f') As)) (s2 : _ -> Comp (list (f' a))) filter_rest, refineEquiv (l <- (Join_Comp_Lists s1 s2); ret (filter (fun x : ilist2 (B := f') (a :: As) => f (ilist2_tl x) (ilist2_hd x) && filter_rest x) l)) (l <- Join_Comp_Lists s1 (fun a => l <- s2 a; ret (filter (f a) l)); ret (filter filter_rest l)).
proof: Proof. split; induction s1; unfold Join_Comp_Lists in *; simpl in *; intros; eauto. - simplify with monad laws; rewrite refineEquiv_bind_unit; reflexivity. - simplify with monad laws; intros v Comp_v; computes_to_inv; subst; computes_to_econstructor; eauto. pose (IHs1 _ (BindComputes _ (fun x => ret (_ x)) _ _ Comp_v'0 (ReturnComputes _))). computes_to_inv; subst. repeat (computes_to_econstructor; eauto). repeat rewrite filter_app, ListFacts.filter_map; simpl; eauto. rewrite <- filter_and, c'; eauto. - intros v Comp_v; computes_to_inv; subst; eauto. - simplify with monad laws; intros v Comp_v; computes_to_inv; subst; computes_to_econstructor; eauto. pose proof (IHs1 _ (BindComputes _ (fun x => ret (_ x)) _ _ Comp_v'0 (ReturnComputes _))). computes_to_inv; subst. repeat (computes_to_econstructor; eauto). rewrite filter_app, ListFacts.filter_map; simpl; eauto. repeat rewrite filter_app, ListFacts.filter_map; simpl; eauto. rewrite <- filter_and, H'; 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