proposition: Lemma DeleteForeignKeysCheck {qsSchema} : forall (qs : UnConstrQueryStructure qsSchema) (Ridx Ridx' :Fin.t _) (DeletedTuples : Ensemble (RawTuple )) (Delete_dec : DecideableEnsemble DeletedTuples) (attr : Attributes _) (attr' : Attributes _) (tupmap : Domain _ attr -> Domain _ attr') (AgreeDelete : forall tup tup', tupleAgree tup tup' [attr] -> DeletedTuples tup -> DeletedTuples tup') (attr_eq_dec : Query_eq (Domain _ attr)) (P : Prop) (ForeignKey_P_P : P -> (forall tup' : IndexedRawTuple, GetUnConstrRelation qs Ridx' tup' -> ForeignKey_P attr' attr tupmap (indexedElement tup') (GetUnConstrRelation qs Ridx))) (tup_map_inj : forall a a', tupmap a = tupmap a' -> a = a'), refine {b' | P -> decides b' (MutationPreservesCrossConstraints (GetUnConstrRelation qs Ridx') (EnsembleDelete (GetUnConstrRelation qs Ridx) DeletedTuples) (ForeignKey_P attr' attr tupmap))} (x <- Count (For (UnConstrQuery_In qs Ridx' (fun tup' => UnConstrQuery_In qs Ridx (fun tup => Where (DeletedTuples tup) Where (tupmap (GetAttributeRaw tup attr) = GetAttributeRaw tup' attr') Return ())))); ret (match x with 0 => true | S _ => false end)).
proof: Proof. simpl; unfold ForeignKey_P; intros. intros v Comp_v. computes_to_inv; destruct_ex; split_and. unfold Count in *; computes_to_inv. destruct v0; simpl in *; subst; computes_to_inv; subst; computes_to_constructor; simpl; unfold not; unfold MutationPreservesCrossConstraints; intros. - destruct (ForeignKey_P_P H _ H0) as [tup2 [In_tup2 Agree_tup2] ]. eexists; intuition eauto. unfold EnsembleDelete; constructor; unfold In; intros; eauto. unfold Complement, Ensembles.In, not; intros. unfold Query_For in *; computes_to_inv. rewrite Permutation_nil in Comp_v; symmetry in Comp_v'0; eauto. apply (fun x => In_UnConstrQuery_In' _ _ _ _ () _ H0 x Comp_v). intros results' H3; apply (fun x => In_UnConstrQuery_In' _ _ _ _ () _ In_tup2 x H3). intros results'0 H5. unfold Query_Where in H5; computes_to_inv; simpl in *; intuition. computes_to_inv; split_and. simpl in H4. unfold QSGetNRelSchema, GetNRelSchema in Agree_tup2; simpl in *. rewrite Agree_tup2 in H4; pose proof (H4 (refl_equal _)) as H'; computes_to_inv; simpl in *; subst; simpl; eauto. apply Return_inv in H'; subst; simpl; intuition. rewrite Comp_v'; destruct v1; try discriminate; reflexivity. - unfold Query_For in *; computes_to_inv. eapply In_UnConstrQuery_In with (a := tt) in Comp_v; destruct_ex; intuition. pose proof (H3 _ H2); pose proof (H0 _ H2); destruct_ex; intuition. eapply In_UnConstrQuery_In with (a := tt) in H1; destruct_ex; intuition. unfold EnsembleDelete in *; inversion H5; subst; unfold Ensembles.In, Complement, In in *. unfold Query_Where in H1; computes_to_inv; intuition. case_eq (@dec _ _ Delete_dec (indexedElement x3)); intros. + apply Delete_dec in H1; pose proof (H13 H1) as H'. computes_to_inv; split_and. unfold indexedTuple in *. destruct (A_eq_dec (GetAttributeRaw (indexedElement x3) attr) (GetAttributeRaw (indexedElement x1) attr)). * rewrite e in *; setoid_rewrite <- H9 in H15; subst; pose proof (H15 (refl_equal _)) as e'; computes_to_inv; simpl in *; subst. apply H12; eapply AgreeDelete; eauto. unfold tupleAgree; simpl; intros attr'' In_attr''; destruct In_attr''; [rewrite H17 in *; eauto | intuition ]. * rewrite H16 in H11; simpl in *; eauto. intros; unfold QSGetNRelSchema, GetNRelSchema in *; simpl in *; setoid_rewrite <- H17 in H9; eauto. + rewrite H14 in H11; simpl in *; eauto. intros H'; apply dec_decides_P in H'; congruence. + eapply Permutation_in; symmetry in Comp_v'; simpl; eauto. destruct v1; simpl in *; [ discriminate | destruct u; eauto]. 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