proposition: Lemma KeyPreservingUpdateFAsUpdateTermOK {heading} : forall (indices indices' : list (@ProperAttribute heading)) (f : @RawTuple heading -> @RawTuple heading), (forall a, List.In a indices -> List.In a indices') -> (forall K tup, List.In K indices' -> GetAttributeRaw (f tup) (@Attribute _ K) = GetAttributeRaw tup (@Attribute _ K)) -> ProperAttributesToValidUpdate (@RawTuple heading -> @RawTuple heading) (fun upd tup => upd tup) indices f.
proof: Proof. induction indices; simpl; intuition. - unfold CountingList_ValidUpdate; auto. - destruct a as [attr [ [ [s | s] | s] | s ] ]; simpl in *. + unfold NTreeBag.IndexedBag_ValidUpdate; intuition. eapply (IHindices indices'); eauto. rewrite bupdate_transform_NestedTree, <- H1. erewrite (H0 {| Attribute := attr; ProperlyTyped := inleft (inleft in_left) |}); simpl; eauto. + unfold ZTreeBag.IndexedBag_ValidUpdate; intuition. eapply (IHindices indices'); eauto. rewrite bupdate_transform_NestedTree, <- H1. erewrite (H0 {| Attribute := attr; ProperlyTyped := inleft (inleft in_right) |}); simpl; eauto. + unfold NatTreeBag.IndexedBag_ValidUpdate; intuition. eapply (IHindices indices'); eauto. rewrite bupdate_transform_NestedTree, <- H1. erewrite (H0 {| Attribute := attr; ProperlyTyped := inleft (inright s) |}); simpl; eauto. + unfold StringTreeBag.IndexedBag_ValidUpdate; intuition. eapply (IHindices indices'); eauto. rewrite bupdate_transform_NestedTree, <- H1. erewrite (H0 {| Attribute := attr; ProperlyTyped := inright s |}); simpl; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Coq.Lists.List Coq.Program.Program Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.NArith.BinNat Coq.ZArith.ZArith_dec Coq.Arith.Arith Coq.FSets.FMapAVL Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.Common.String_as_OT Fiat.Common.List.ListFacts Fiat.Common.ilist2 Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.Delete Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements Fiat.QueryStructure.Implementation.Operations.List.ListQueryRefinements