proposition: Lemma refine_unused_key_check : 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) (rel : Ensemble IndexedRawTuple) (l : list RawTuple), EnsembleIndexedListEquivalence rel l -> refine {b | decides b (forall tup' : IndexedRawTuple, rel tup' -> tupleAgree tup (indexedElement tup') attrlist' -> tupleAgree tup (indexedElement tup') attrlist)} (ret (Check_Attr_Depend _ _ attr_eq_dec attr_eq_dec' tup l)).
proof: Proof. intros. unfold refine; intros; computes_to_inv; subst; computes_to_econstructor. case_eq (Check_Attr_Depend _ _ attr_eq_dec attr_eq_dec' tup l); simpl; intros. eapply Check_Attr_Depend_dec; try apply H; eauto. destruct H as [l' [fresh_l' [l'_eq [equiv_l_l' _] ] ] ]; subst. eapply in_map; eapply equiv_l_l'; eapply H1. unfold not; intros. eapply (Check_Attr_Depend_dec' attr_eq_dec attr_eq_dec'); eauto. destruct H as [l' [fresh_l' [l'_eq [equiv_l_l' _] ] ] ]; subst. intros. apply (in_map_iff indexedRawTuple) in H; destruct_ex; intuition; subst. intros; eapply H1; eauto. eapply equiv_l_l'; 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