proposition: Lemma FiniteTables_AbsR_Insert' {qs_schema : RawQueryStructureSchema} : forall (r_o r_n r_n' : UnConstrQueryStructure qs_schema) (idx : Fin.t (numRawQSschemaSchemas qs_schema)) (tup : IndexedElement), computes_to (UpdateUnConstrRelationInsertC r_n idx tup) r_n' -> UnConstrFreshIdx (GetUnConstrRelation r_n idx) (elementIndex tup) -> FiniteTables_AbsR r_o r_n -> FiniteTables_AbsR r_n' r_n'.
proof: Proof. unfold UpdateUnConstrRelationInsertC; intros; computes_to_inv; subst. unfold FiniteTables_AbsR; intuition. destruct (fin_eq_dec idx idx0); subst. - unfold GetUnConstrRelation, UpdateUnConstrRelation. rewrite ilist2.ith_replace2_Index_eq. unfold FiniteTables_AbsR in H1; intuition subst. destruct (H2 idx0) as [l ?]; eexists (cons (indexedElement tup) l). eauto using UnIndexedEnsembleListEquivalence_Insert. - unfold GetUnConstrRelation, UpdateUnConstrRelation. rewrite ilist2.ith_replace2_Index_neq; eauto. unfold FiniteTables_AbsR in H1; intuition subst. eapply H2. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Coq.Sorting.Permutation Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Tactics.CacheStringConstant Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Operations.Empty Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Specification.Operations.Update Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements Fiat.QueryStructure.Implementation.Operations.General.QueryStructureRefinements Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Automation.General.QueryAutomation Fiat.QueryStructure.Automation.General.InsertAutomation Fiat.QueryStructure.Automation.General.DeleteAutomation