proposition: Lemma Initialize_IndexedQueryStructureImpls_AbsR {qs_schema : RawQueryStructureSchema} : forall (Index : ilist3 (B := fun sch => SearchUpdateTerms (rawSchemaHeading sch)) (qschemaSchemas qs_schema)) (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)))), refine (r_o <- @Initialize_IndexedQueryStructure _ _ Index; {r_n | Build_IndexedQueryStructure_Impl_AbsR DelegateReps DelegateImpls ValidImpls r_o r_n}) (ret (Initialize_IndexedQueryStructureImpls' DelegateReps DelegateImpls)).
proof: Proof. destruct qs_schema. unfold Build_IndexedQueryStructure_Impl_AbsR, GetIndexedRelation. simpl; clear qschemaConstraints. induction qschemaSchemas; intros; pose proof (ilist3_invert _ Index) as H'; simpl in H'; subst. - simpl; simplify with monad laws. computes_to_econstructor; computes_to_inv; subst. eapply (Lookup_Iterate_Dep_Type); simpl. econstructor. - destruct H' as [idx' [Index' Index_eq] ]; subst. simpl; unfold CallBagConstructor; simpl; simplify with monad laws. pose proof (IHqschemaSchemas Index' (fun idx => DelegateReps (Fin.FS idx)) (fun idx => DelegateImpls (Fin.FS idx)) (fun idx => ValidImpls (Fin.FS idx)) _ (ReturnComputes _)). unfold refine; intros; computes_to_inv; subst. computes_to_econstructor; eauto. computes_to_econstructor. intro idx. pose proof (@refine_BagImplConstructor _ _ _ DelegateReps DelegateImpls ValidImpls idx BagEmpty). revert qschemaSchemas IHqschemaSchemas DelegateReps idx' Index' DelegateImpls ValidImpls v0 H H' H0. pattern n, idx; apply Fin.caseS; simpl; intros. + destruct (H0) as [r_o' [refines_r_o' AbsR_r_o'] ]. pose proof (refines_r_o' _ (ReturnComputes _)). unfold CallBagConstructor in *; simpl in *; computes_to_inv; subst. apply AbsR_r_o'. + 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