proposition: Lemma refine_BagADT_QSDelete' {ResultT} : forall (r_o : UnConstrQueryStructure qs_schema) (r_n : IndexedQueryStructure qs_schema BagIndexKeys) idx DeletedTuples (k : _ -> Comp ResultT) (k' : _ -> Comp ResultT) (DT_Dec : DecideableEnsemble DeletedTuples) search_pattern, ExtensionalEq (@DecideableEnsembles.dec _ _ DT_Dec) (BagMatchSearchTerm (ith3 BagIndexKeys idx) search_pattern) -> DelegateToBag_AbsR r_o r_n -> (forall r_o r_n, DelegateToBag_AbsR r_o r_n -> refine (k r_o) (k' r_n)) -> refine (r_o' <- UpdateUnConstrRelationDeleteC r_o idx DeletedTuples; k r_o') (r_n' <- CallBagDelete idx r_n search_pattern; k' (fst r_n')).
proof: Proof. unfold refine; intros. unfold CallBagDelete, CallBagMethod in H2; simpl in H2; computes_to_inv; subst; simpl in *. unfold UpdateUnConstrRelationDeleteC; repeat computes_to_econstructor. eapply H1; eauto. unfold DelegateToBag_AbsR; intros. intros; destruct (fin_eq_dec idx idx0); subst. - rewrite get_update_unconstr_eq, get_update_indexed_eq. destruct (H0 idx0) as [l [ [ [bnd fresh_bnd] ? ] [ [bnd' fresh_bnd'] ? ] ] ]. pose proof (UnIndexedEnsembleListEquivalence_Delete DT_Dec H3). pose proof (UnIndexedEnsembleListEquivalence_Delete DT_Dec H4). eexists (filter (fun a : RawTuple => negb (DecideableEnsembles.dec a)) l); split; unfold EnsembleIndexedListEquivalence; split; eauto; try solve [eexists _; eauto using UnConstrFreshIdx_Delete]. eapply UnIndexedEnsembleListEquivalence_Same_set; eauto. split; unfold Included; intros; inversion H7; subst; econstructor; eauto; unfold Complement, Ensembles.In in *. + eapply Decides_false in H9; rewrite H in H9. congruence. + eapply Decides_false; rewrite <- H in H9; destruct (DecideableEnsembles.dec (indexedElement x)); congruence. - rewrite get_update_unconstr_neq, get_update_indexed_neq; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist2 Fiat.Common.i2list Fiat.Common.ilist3 Fiat.Common.i3list Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.String_as_OT Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements