proposition: Lemma Implement_Bound_Bag_Call' A : forall qs_schema Index DelegateReps DelegateImpls ValidImpls r_o r_n ridx midx, @Build_IndexedQueryStructure_Impl_AbsR qs_schema Index DelegateReps DelegateImpls ValidImpls r_o r_n -> Lift_Method2P (fst (MethodDomCod (BagSig RawTuple (BagSearchTermType (ith3 Index ridx)) (BagUpdateTermType (ith3 Index ridx))) midx)) (snd (MethodDomCod (BagSig RawTuple (BagSearchTermType (ith3 Index ridx)) (BagUpdateTermType (ith3 Index ridx))) midx)) (fun cod m m' => forall (k : _ -> Comp A) k', (forall r_n' r_o' c, (AbsR (ValidImpls ridx)) r_o' r_n' -> refine (k (r_o', c)) (k' r_n' c)) -> refine (l <- m; k l) (k' (fst m') (snd m'))) (fun m m' => forall (k : _ -> Comp A) k', (forall r_n' r_o', (AbsR (ValidImpls ridx)) r_o' r_n' -> refine (k r_o') (k' r_n')) -> refine (l <- m; k l) (k' m')) (CallBagMethod (BagIndexKeys := Index) ridx midx r_o) (CallBagImplMethod DelegateReps DelegateImpls midx r_n).
proof: Proof. simpl; intros. generalize (@refine_BagImplMethods qs_schema Index DelegateReps DelegateImpls ValidImpls r_o r_n ridx H midx). simpl. eapply (fun P H => Lookup_Iterate_Dep_Type P H midx). simpl in *; intuition. - destruct (H0 t) as [r_o' [refines_r_o' AbsR_r_o'] ]. rewrite refines_r_o'; simplify with monad laws. eapply H1; eauto. - destruct (H0) as [r_o' [refines_r_o' AbsR_r_o'] ]. rewrite refines_r_o'; simplify with monad laws. eapply H1; eauto. - destruct (H0 t) as [r_o' [refines_r_o' AbsR_r_o'] ]. rewrite refines_r_o'; simplify with monad laws. eapply H1; eauto. - destruct (H0 t) as [r_o' [refines_r_o' AbsR_r_o'] ]. rewrite refines_r_o'; simplify with monad laws. eapply H1; eauto. - destruct (H0 t) as [r_o' [refines_r_o' AbsR_r_o'] ]. rewrite refines_r_o'; simplify with monad laws. eapply H1; eauto. - destruct (H0 t t0) as [r_o' [refines_r_o' AbsR_r_o'] ]. rewrite refines_r_o'; simplify with monad laws. eapply H1; 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