proposition: Corollary filter_join_ilist2_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))), (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') (a :: As) => f (ilist2_tl x)) l)) (Join_Comp_Lists (filter f s1) s2).
proof: Proof. intros; pose proof (filter_and_join_ilist_tail f s1 s2 (fun _ => true)). setoid_rewrite filter_and in H0; setoid_rewrite filter_true in H0. setoid_rewrite H0; eauto; setoid_rewrite refineEquiv_unit_bind; reflexivity. 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