proposition: Lemma refine_Join_List_Query_In {QueryT ResultT} qsSchema qs R l' l resultComp : EnsembleIndexedListEquivalence (GetUnConstrRelation qs R) l -> refine (List_Query_In (QueryT := QueryT) l' (fun b => @UnConstrQuery_In ResultT qsSchema qs R (resultComp b))) (List_Query_In (Join_Lists l' l) (fun b => (resultComp (fst b) (snd b)))).
proof: Proof. intros; unfold QueryResultComp, List_Query_In. rewrite refine_flatten_CompList_func. 2: unfold pointwise_relation; intros; apply refine_List_Query_In; eassumption. unfold List_Query_In, flatten_CompList. induction l'; simpl. reflexivity. setoid_rewrite IHl'; clear IHl'. unfold Join_Lists; simpl; auto. simpl; rewrite map_app. rewrite map_map. repeat rewrite fold_right_app. simpl. assert (resultComp a = fun x : RawTuple => resultComp a x) as eta by (apply functional_extensionality; auto); rewrite <- eta. induction (map (resultComp a) l); simpl; simplify with monad laws. - reflexivity. - setoid_rewrite <- IHl0. repeat setoid_rewrite refineEquiv_bind_bind. setoid_rewrite refineEquiv_bind_unit. setoid_rewrite app_assoc; reflexivity. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.GeneralBuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.SetEq Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListMorphisms Fiat.Common.List.FlattenList Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.Common.List.ListFacts