proposition: Lemma filter_and_join_ilist_tail {n} {A} {a} {As : Vector.t A n} (f' : A -> Type) : forall (f : (ilist2 (B := f') As) -> bool) (s1 : list (ilist2 (B := f') As)) (s2 : ilist2 (B := f') As -> Comp (list (f' a))) filter_rest, (forall a, List.In a s1 -> exists v, computes_to (s2 a) v) -> refineEquiv (l <- (Join_Comp_Lists s1 s2); ret (filter (fun x : ilist2 (B := f') (Vector.cons _ a _ As) => f (ilist2_tl x) && filter_rest x) l)) (l <- Join_Comp_Lists (filter f s1) s2; ret (filter filter_rest l)).
proof: Proof. split; induction s1; unfold Join_Comp_Lists in *; simpl in *; intros; eauto. - simplify with monad laws; simpl; intros v Comp_v; computes_to_inv; subst; repeat econstructor. - simplify with monad laws; intros v. case_eq (f a0); simpl; intros a0_eq Comp_v. + computes_to_inv; subst; computes_to_econstructor; eauto. pose (IHs1 (fun a In_a => H _ (or_intror In_a)) _ (BindComputes _ (fun x => ret (filter filter_rest x)) _ _ Comp_v'0 (ReturnComputes _))) ; computes_to_inv; subst. computes_to_econstructor; eauto. rewrite !filter_app, !filter_map, c'; simpl. rewrite a0_eq, filter_and, filter_true; eauto. + pose (IHs1 (fun a In_a => H _ (or_intror In_a)) _ Comp_v); computes_to_inv; subst. destruct (H a0); eauto. repeat (computes_to_econstructor; eauto). rewrite filter_app, filter_map; simpl; intros; rewrite a0_eq, filter_false, c'; simpl; computes_to_econstructor. - intros v Comp_v; computes_to_inv; subst; eauto. - intros v Comp_v; computes_to_inv; subst. pose proof (IHs1 (fun a In_a => H _ (or_intror In_a)) _ (BindComputes _ (fun x => ret (_ x)) _ _ Comp_v'0 (ReturnComputes _))). computes_to_inv. case_eq (f a0); intros a0_eq; simpl. + repeat (computes_to_econstructor; eauto). rewrite !filter_app, !filter_map, H0', filter_and; simpl. rewrite a0_eq, filter_and, filter_true; eauto. + repeat (computes_to_econstructor; eauto). rewrite !filter_app, !filter_map, !filter_and, H0'; simpl. rewrite a0_eq, filter_false, <- filter_and; 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