proposition: Lemma refine_BagImplMethods {qs_schema : RawQueryStructureSchema} (schemas := qschemaSchemas qs_schema) (Index : ilist3 (B := fun sch => SearchUpdateTerms (rawSchemaHeading sch)) schemas) (DelegateReps : Fin.t _ -> Type) (DelegateImpls : forall idx, ComputationalADT.pcADT (Build_IndexedQueryStructure_Impl_Sigs Index idx) (DelegateReps idx)) (ValidImpls : forall idx, refineADT (Build_IndexedQueryStructure_Impl_Specs Index idx) (ComputationalADT.LiftcADT (existT _ _ (DelegateImpls idx)))) : forall (r_o : IndexedQueryStructure qs_schema Index) (r_n : Build_IndexedQueryStructure_Impl_cRep Index DelegateReps) ridx, Build_IndexedQueryStructure_Impl_AbsR DelegateReps DelegateImpls ValidImpls r_o r_n -> forall midx, 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' => exists r_o', refine m (ret (r_o', snd m')) /\ AbsR (ValidImpls ridx) r_o' (fst m')) (fun m m' => exists r_o', refine m (ret r_o') /\ AbsR (ValidImpls ridx) r_o' m') (CallBagMethod ridx midx r_o) (CallBagImplMethod DelegateReps DelegateImpls midx r_n) .
proof: Proof. intros. generalize (ADTRefinementPreservesMethods (ValidImpls ridx) midx (GetIndexedRelation r_o ridx) (GetIndexedQueryStructureRelation r_n ridx) (H ridx)). eapply (fun P H => Lookup_Iterate_Dep_Type P H midx); simpl in *; intuition. - specialize (H0 t _ (ReturnComputes _)); computes_to_inv; subst; unfold CallBagImplMethod, CallBagMethod in *; simpl in *. unfold cMethods, callMethod in *; simpl in *; rewrite <- H0''; simpl. eexists; split; eauto. intros v Comp_v; computes_to_inv; subst. repeat computes_to_econstructor; eauto. - specialize (H0 _ (ReturnComputes _)); computes_to_inv; subst; unfold CallBagImplMethod, CallBagMethod in *; simpl in *. unfold cMethods, callMethod in *; simpl in *; rewrite <- H0''; simpl. eexists; split; eauto. intros v Comp_v; computes_to_inv; subst. repeat computes_to_econstructor; eauto. - specialize (H0 t _ (ReturnComputes _)); computes_to_inv; subst; unfold CallBagImplMethod, CallBagMethod in *; simpl in *. unfold cMethods in H0'; simpl in *. eexists; split; eauto. intros v Comp_v; computes_to_inv; subst. repeat computes_to_econstructor; eauto. - specialize (H0 t _ (ReturnComputes _)); computes_to_inv; subst; unfold CallBagImplMethod, CallBagMethod in *; simpl in *. unfold cMethods, callMethod in *; simpl in *; rewrite <- H0''; simpl. eexists; split; eauto. intros v Comp_v; computes_to_inv; subst. repeat computes_to_econstructor; eauto. - specialize (H0 t _ (ReturnComputes _)); computes_to_inv; subst; unfold CallBagImplMethod, CallBagMethod in *; simpl in *. unfold cMethods, callMethod in *; simpl in *; rewrite <- H0''; simpl. eexists; split; eauto. intros v Comp_v; computes_to_inv; subst. repeat computes_to_econstructor; eauto. - specialize (H0 t t0 _ (ReturnComputes _)); computes_to_inv; subst; unfold CallBagImplMethod, CallBagMethod in *; simpl in *. unfold cMethods, callMethod in *; simpl in *; rewrite <- H0''; simpl. eexists; split; eauto. intros v Comp_v; computes_to_inv; subst. repeat 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