proposition: Lemma insert_finite_helper: forall (qs_schema : RawQueryStructureSchema) (r_n: { r_n: UnConstrQueryStructure qs_schema & AllFinite r_n }) qidx tup, UnConstrFreshIdx (GetUnConstrRelation (projT1 r_n) qidx) (elementIndex tup) -> AllFinite (UpdateUnConstrRelation (projT1 r_n) qidx (EnsembleInsert tup (GetUnConstrRelation (projT1 r_n) qidx))).
proof: Proof. red; intros qsc r_n idx tup Hfresh idx'. destruct (Fin.eqb idx idx') eqn:idxeq. - apply Fin.eqb_eq in idxeq. subst idx'. destruct r_n as [r Hfin]. destruct (Hfin idx) as [l1 Hl1]. destruct Hl1 as [l2 [Hmap [Hin Hdup]]]. exists ((indexedElement tup) :: l1). cbn. rewrite get_update_unconstr_eq. red. exists (tup :: l2). split. simpl. rewrite <- Hmap. reflexivity. split. split; intros H; unfold EnsembleInsert, In in *; destruct H; simpl; [ left; symmetry; assumption | right; apply (Hin x); apply H | left; symmetry; assumption | right; apply (Hin x); apply H]. simpl. apply NoDup_cons. red in Hfresh. simpl in Hfresh. assert (Hlist: forall (x: nat) l, (forall x', List.In x' l -> lt x' x) -> ~List.In x l). { intros x l Hx'. intro Hx. apply (Hx' x) in Hx. apply lt_irrefl in Hx. inversion Hx. } apply Hlist. apply forall_In_map. intros elem Helem. apply Hfresh. apply (Hin elem). assumption. assumption. - assert (Hidxeq: idx <> idx'). { intro. apply Fin.eqb_eq in H. congruence. } destruct r_n as [r Hfin]. destruct (Hfin idx') as [l1 Hl1]. exists l1. cbn. rewrite get_update_unconstr_neq. assumption. assumption. Qed.
imports: Coq.Lists.List 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.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.List.ListFacts Fiat.Narcissus.Examples.Guard.Core 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 Fiat.Narcissus.Examples.Guard.Core Fiat.Narcissus.Examples.Guard.DropFields