proposition: Lemma InsertForeignKeysCheck {qsSchema} : forall (qs : UnConstrQueryStructure qsSchema) (Ridx Ridx' :Fin.t _) (attr : Attributes _) (attr' : Attributes _) (tupmap : Domain _ attr' -> Domain _ attr) tup (ForeignKey_P_P : (forall tup' : IndexedRawTuple, GetUnConstrRelation qs Ridx tup' -> ForeignKey_P attr attr' tupmap (indexedElement tup') (GetUnConstrRelation qs Ridx'))), Ridx <> Ridx' -> refine {b' | decides b' (forall tup', (GetUnConstrRelation qs Ridx) tup' -> ForeignKey_P attr attr' tupmap (indexedElement tup') (EnsembleInsert tup (GetUnConstrRelation qs Ridx')))} (ret true).
proof: Proof. intros; apply refine_pick_val; simpl; intros. unfold ForeignKey_P in *. destruct (ForeignKey_P_P _ H0) as [tup'' [In_tup'' ?] ]; exists tup''; unfold EnsembleInsert; intuition. Qed.
imports: Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.Operations.Query Coq.Lists.List Coq.Arith.Compare_dec Coq.Bool.Bool Coq.Strings.String Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.IterateBoundedIndex Fiat.Common.List.ListFacts Fiat.Common.LogicFacts Fiat.Common.DecideableEnsembles Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.Computation.Refinements.General Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Specification.Operations.Mutate