proposition: Lemma Check_Attr_Depend_dec' : forall (h : RawHeading) (attrlist attrlist' : list (Attributes h)) (attr_eq_dec : List_Query_eq (map (Domain h) attrlist)) (attr_eq_dec' : List_Query_eq (map (Domain h) attrlist')) (tup : RawTuple) (l : list RawTuple), Check_Attr_Depend _ _ attr_eq_dec attr_eq_dec' tup l = false -> ~ (forall tup' : RawTuple, List.In tup' l -> tupleAgree tup tup' attrlist' -> tupleAgree tup tup' attrlist).
proof: Proof. unfold Check_Attr_Depend; intros. eapply Check_List_Prop_dec' with (P := fun tup' : RawTuple => ~ tupleAgree tup tup' attrlist' \/ tupleAgree tup tup' attrlist) in H; eauto. destruct_ex; intuition; eauto. intros; destruct (Tuple_Agree_dec _ _ attr_eq_dec' tup a); auto; [ apply (proj1 (Tuple_Agree_eq_dec _ _ _ _ _ )) in t; rewrite t | apply (proj1 (Tuple_Agree_eq_dec' _ _ _ _ _ )) in n; rewrite n]; simpl; intuition. right; eapply Tuple_Agree_eq_dec; eauto. exfalso; match goal with | [ H : _ |- _ ] => apply H; eapply Tuple_Agree_eq_dec; eauto end. eapply Tuple_Agree_eq_dec; eauto. left; eapply Tuple_Agree_eq_dec'; eauto. 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 Coq.Bool.Bool Fiat.Common.ilist2 Fiat.Computation Fiat.ADT Fiat.ADTRefinement Fiat.ADTNotation Fiat.QueryStructure.Specification.Representation.QueryStructureSchema Fiat.QueryStructure.Specification.Operations.Query Fiat.QueryStructure.Specification.Operations.Insert Fiat.QueryStructure.Specification.Representation.QueryStructure Fiat.ADTRefinement.BuildADTRefinements Fiat.Common.DecideableEnsembles Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.QueryStructureRefinements Fiat.QueryStructure.Implementation.Constraints.ConstraintChecksRefinements