proposition: Lemma refine_BagImplConstructor {n} {schemas : Vector.t RawSchema n} (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 (ridx : Fin.t _) cidx, Lift_Constructor2P (ConstructorDom (BagSig RawTuple (BagSearchTermType (ith3 Index ridx)) (BagUpdateTermType (ith3 Index ridx))) cidx) (fun c c' => exists r_o' , refine c (ret r_o') /\ AbsR (ValidImpls ridx) r_o' c') (@CallBagConstructor _ (ith3 Index ridx) cidx) (CallBagImplConstructor DelegateReps DelegateImpls cidx).
proof: Proof. intros. generalize (ADTRefinementPreservesConstructors (ValidImpls ridx) cidx). eapply (fun P H => Lookup_Iterate_Dep_Type P H cidx). simpl; split; intuition. unfold refine in *. specialize (H _ (ReturnComputes _)); computes_to_inv; subst. eexists; unfold CallBagImplConstructor in *; simpl in *. split; simpl. - intros v' Comp_v; computes_to_inv; subst. unfold CallBagConstructor; simpl; computes_to_econstructor. - eapply H'. 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