proposition: Lemma swap_joins : forall {A B} s1 s2, Permutation (@Join_Lists A B s1 s2) (map swap_pair (Join_Lists s2 s1)).
proof: Proof. induction s1; simpl; intros. - rewrite join_nil_r; trivial. - rewrite IHs1; unfold Join_Lists. replace (map (fun b : B => (a, b)) s2) with (map swap_pair (map (fun b : B => (b, a)) s2)) by (induction s2; unfold swap_pair in *; simpl; try rewrite IHs2; firstorder). rewrite <- map_app; f_equiv; simpl. induction s2; simpl; trivial. constructor; rewrite <- IHs2. rewrite !app_assoc. apply Permutation_app_tail, Permutation_app_comm. 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