proposition: Lemma QSInsertSpec_refine' : forall qsSchema (qs : QueryStructure qsSchema) Ridx tup default, refine (Pick (QSInsertSpec qs Ridx tup)) (schConstr_self <- {b | decides b (SatisfiesAttributeConstraints Ridx (indexedElement tup))}; schConstr <- {b | decides b (forall tup', GetRelation qs Ridx tup' -> SatisfiesTupleConstraints Ridx (indexedElement tup) (indexedElement tup'))}; schConstr' <- {b | decides b (forall tup', GetRelation qs Ridx tup' -> SatisfiesTupleConstraints Ridx (indexedElement tup') (indexedElement tup))}; qsConstr <- {b | decides b (forall Ridx', SatisfiesCrossRelationConstraints Ridx Ridx' (indexedElement tup) (GetRelation qs Ridx'))}; qsConstr' <- {b | decides b (forall Ridx', Ridx' <> Ridx -> forall tup', (GetRelation qs Ridx') tup' -> SatisfiesCrossRelationConstraints Ridx' Ridx (indexedElement tup') (EnsembleInsert tup (GetRelation qs Ridx)))}; match schConstr_self, schConstr, schConstr', qsConstr, qsConstr' with | true, true, true, true, true => {qs' | (forall Ridx', Ridx <> Ridx' -> GetRelation qs Ridx' = GetRelation qs' Ridx') /\ forall t, GetRelation qs' Ridx t <-> (EnsembleInsert tup (GetRelation qs Ridx) t) } | _, _ , _, _, _ => default end).
proof: Proof. intros qsSchema qs Ridx tup default v Comp_v; computes_to_inv; destruct v0; [ destruct v1; [ destruct v2; [ destruct v3; [ destruct v4; [ repeat (computes_to_inv; destruct_ex; split_and); simpl in *; computes_to_econstructor; unfold QSInsertSpec; eauto | ] | ] | ] | ] | ]; cbv delta [decides] beta in *; simpl in *; repeat (computes_to_inv; destruct_ex); eauto; computes_to_econstructor; unfold QSInsertSpec; intros; solve [exfalso; intuition]. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Fiat.Computation Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.ADTRefinement.BuildADTRefinements Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.IterateBoundedIndex Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements