proposition: Corollary refine_QSEmptySpec_Initialize_IndexedQueryStructure : refine {nr' | DelegateToBag_AbsR (imap2 rawRel (Build_EmptyRelations (qschemaSchemas qs_schema))) nr'} (@Initialize_IndexedQueryStructure _ (qschemaSchemas qs_schema) BagIndexKeys).
proof: Proof. intros v Comp_v. computes_to_econstructor. unfold IndexedQueryStructure, DelegateToBag_AbsR, GetIndexedRelation. unfold GetUnConstrRelation. unfold DropQSConstraints, QSEmptySpec. intros; simpl; rewrite <- ith_imap2, ith_Bounded_BuildEmptyRelations, i2th_Bounded_Initialize_IndexedQueryStructure; eauto. intros; eexists List.nil; split; intros; simpl; try rewrite <- ith_imap2, ith_Bounded_BuildEmptyRelations. - split; simpl; intros. + exists 0; unfold UnConstrFreshIdx; intros; intuition. + eexists List.nil; intuition eauto. * inversion H. * inversion H. * econstructor. - split; simpl; intros. + exists 0; unfold UnConstrFreshIdx; intros; intuition. + eexists List.nil; intuition eauto. * inversion H. * inversion H. * econstructor. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist2 Fiat.Common.i2list Fiat.Common.ilist3 Fiat.Common.i3list Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.String_as_OT Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements