proposition: Lemma Join_Comp_Lists_Impl'' qs_schema (n' := numRawQSschemaSchemas qs_schema ) (schemas := qschemaSchemas qs_schema) n (Index : ilist3 schemas) (DelegateReps : Fin.t n' -> Type) (DelegateImpls : forall idx : Fin.t n', ComputationalADT.pcADT (Build_IndexedQueryStructure_Impl_Sigs Index idx) (DelegateReps idx)) ValidImpls heading (idx : Fin.t n') : forall (r_n : IndexedQueryStructure qs_schema Index) l f' r_n', Build_IndexedQueryStructure_Impl_AbsR DelegateReps DelegateImpls ValidImpls r_n r_n' -> exists r_n'', computes_to (@Join_Comp_Lists_prod n _ _ (@RawTuple) heading _ r_n l (fun r_n b' => br <- CallBagMethod idx BagFind r_n (f' b'); ret (UpdateIndexedRelation qs_schema Index r_n idx (fst br), snd br))) (r_n'', snd (Join_Comp_Lists_prod' (As := heading) r_n' l (fun r_n b' => let br := @CallBagImplMethod _ _ Index DelegateReps DelegateImpls _ BagFind r_n (f' b') in (Update_Build_IndexedQueryStructure_Impl_cRep qs_schema Index DelegateReps r_n idx (fst br), snd br)))) /\ Build_IndexedQueryStructure_Impl_AbsR DelegateReps DelegateImpls ValidImpls r_n'' (fst (Join_Comp_Lists_prod' (As := heading) r_n' l (fun r_n b' => let br := @CallBagImplMethod _ _ Index DelegateReps DelegateImpls _ BagFind r_n (f' b') in (Update_Build_IndexedQueryStructure_Impl_cRep qs_schema Index DelegateReps r_n idx (fst br), snd br)))).
proof: Proof. induction l; unfold Join_Comp_Lists_prod, Join_Comp_Lists_prod'; simpl; intros. - eexists; simpl; intuition eauto. - destruct (IHl f' r_n' H) as [r_n'' [? ?] ]. destruct (@refine_BagImplMethods _ _ DelegateReps DelegateImpls ValidImpls _ _ idx H1 BagFind (f' a)) as [v' [ref AbsR] ]. pose proof (ref _ (ReturnComputes _)). eexists; intuition eauto. computes_to_econstructor; eauto. computes_to_econstructor; eauto. simpl. eapply ReturnComputes_eq; f_equal. progress f_equal. unfold Join_Comp_Lists_prod'. Admitted. Lemma Join_Comp_Lists_Impl' {B} qs_schema (n' := numRawQSschemaSchemas qs_schema ) (schemas := qschemaSchemas qs_schema) n (Index : ilist3 schemas) (DelegateReps : Fin.t n' -> Type) (DelegateImpls : forall idx : Fin.t n', ComputationalADT.pcADT (Build_IndexedQueryStructure_Impl_Sigs Index idx) (DelegateReps idx)) ValidImpls heading (idx : Fin.t n') : forall (r_n : IndexedQueryStructure qs_schema Index) l f' (f'' : _ -> B) r_n', Build_IndexedQueryStructure_Impl_AbsR DelegateReps DelegateImpls ValidImpls r_n r_n' -> refine (x <- @Join_Comp_Lists_prod n _ _ (@RawTuple) heading _ r_n l (fun r_n b' => br <- CallBagMethod idx BagFind r_n (f' b'); ret (UpdateIndexedRelation qs_schema Index r_n idx (fst br), snd br)); r_n'0 <- {r_n0 | Build_IndexedQueryStructure_Impl_AbsR DelegateReps DelegateImpls ValidImpls (fst x) r_n0}; ret (r_n'0, f'' (snd x))) (let res := (Join_Comp_Lists_prod' (As := heading) r_n' l (fun r_n b' => let br := @CallBagImplMethod _ _ Index DelegateReps DelegateImpls _ BagFind r_n (f' b') in (Update_Build_IndexedQueryStructure_Impl_cRep qs_schema Index DelegateReps r_n idx (fst br), snd br))) in ret (fst res, f'' (snd res) )). Proof. intros * AbsR v Comp_v. computes_to_inv; subst. destruct (@Join_Comp_Lists_Impl'' qs_schema n Index DelegateReps DelegateImpls ValidImpls heading idx r_n l f' r_n' AbsR) as [r_n'' [? AbsR_r_n''] ]. computes_to_econstructor; 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