proposition: Lemma Join_Comp_Lists_eq qs_schema Index : forall idx n h f r_n l, refine (Join_Comp_Lists (n := n) l (fun a0 : ilist2 h => u <- @CallBagMethod qs_schema Index idx BagFind r_n (f a0); ret (snd u))) (u <- Join_Comp_Lists_prod r_n l (fun r_n (a0 : ilist2 h) => @CallBagFind qs_schema Index idx r_n (f a0)); ret (snd u)) .
proof: Proof. intros; induction l; unfold Join_Comp_Lists, Join_Comp_Lists_prod; simpl. - intros v CompV. computes_to_inv; subst. computes_to_econstructor. - setoid_rewrite IHl. repeat setoid_rewrite refineEquiv_bind_bind. Local Opaque CallBagMethod. simplify with monad laws. intros v Comp_v; computes_to_inv; subst. unfold CallBagFind in Comp_v'; computes_to_inv; subst; simpl. repeat computes_to_econstructor; eauto. assert (r_n = fst v0); subst; eauto. generalize v0 Comp_v; clear. induction l. + simpl; intros; computes_to_inv; subst. reflexivity. + simpl; intros; computes_to_inv; subst. apply IHl in Comp_v; simpl. unfold CallBagFind in Comp_v'; computes_to_inv; subst. simpl. apply CallBagFind_fst in Comp_v'; eauto. Qed.
imports: Coq.Bool.Bool Coq.Strings.String Coq.Strings.Ascii Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.Common.BoolFacts Fiat.Common.LogicFacts Fiat.Common.List.FlattenList Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.IterateBoundedIndex Fiat.Common.Tactics.CacheStringConstant Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.SearchTerms.ListInclusion Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Specification.SearchTerms.InRange Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements Fiat.QueryStructure.Automation.General.QueryAutomation Fiat.QueryStructure.Automation.General.InsertAutomation Fiat.QueryStructure.Automation.General.DeleteAutomation Fiat.QueryStructure.Automation.General.QueryStructureAutomation Fiat.QueryStructure.Automation.Constraints.TrivialConstraintAutomation Fiat.QueryStructure.Automation.Constraints.FunctionalDependencyAutomation Fiat.QueryStructure.Automation.Constraints.ForeignKeyAutomation Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagImplementation Fiat.QueryStructure.Implementation.ListImplementation Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.BagADT.Refinements Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Automation.SearchTerms.InclusionSearchTerms Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.SearchTerms.RangeSearchTerms Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Implementation.Operations Coq.Logic.Eqdep_dec Fiat.ADT.ComputationalADT Fiat.ADTNotation.BuildComputationalADT Fiat.ADTRefinement.GeneralBuildADTRefinements