proposition: Lemma refine_BagADT_QSDelete_snd : forall r_o (r_n : IndexedQueryStructure qs_schema BagIndexKeys), DelegateToBag_AbsR r_o r_n -> forall (idx :Fin.t _) (DT : Ensemble RawTuple) (DT_Dec : DecideableEnsemble DT) search_pattern, ExtensionalEq (@DecideableEnsembles.dec _ _ DT_Dec) (BagMatchSearchTerm (ith3 BagIndexKeys idx) search_pattern) -> refine {r_n' | DelegateToBag_AbsR (UpdateUnConstrRelation r_o idx (EnsembleDelete (GetUnConstrRelation r_o idx) DT)) r_n'} (l <- (CallBagDelete idx r_n search_pattern); ret (fst l)).
proof: Proof. intros. computes_to_constructor; computes_to_inv. unfold CallBagDelete, CallBagMethod in *; simpl in *; computes_to_inv; subst. simpl. unfold DelegateToBag_AbsR; intros. - destruct (fin_eq_dec idx idx0); subst. + rewrite get_update_unconstr_eq, get_update_indexed_eq. unfold DelegateToBag_AbsR in H. destruct (H idx0) as [l [ [ [bnd fresh_bnd] [l' [l'_eq [l_eqv NoDup_l'] ] ] ] [ [bnd' fresh_bnd'] [l'' [l''_eq [l''_eqv NoDup_l''] ] ] ] ] ]. exists (filter (fun a => negb (DecideableEnsembles.dec a)) l); repeat split. * exists bnd; unfold EnsembleDelete, UnConstrFreshIdx; intros. inversion H2; subst; eauto. * unfold UnIndexedEnsembleListEquivalence; exists (filter (fun a => negb (DecideableEnsembles.dec (indexedElement a))) l'); split; eauto. rewrite <- l'_eq; rewrite ListFacts.filter_map; reflexivity. intuition. apply filter_In; split. eapply l_eqv; inversion H2; eauto. inversion H2; subst; rewrite (proj2 (Decides_false _ _)); eauto. rewrite filter_In in H2; intuition; constructor; [ apply l_eqv; eauto | case_eq (DecideableEnsembles.dec (indexedElement x)); intros H'; rewrite H' in H4; try discriminate; eapply Decides_false in H'; eauto ]. eapply NoDup_filter_map with (f := fun a => negb (DecideableEnsembles.dec a)); eauto. * exists bnd'; unfold EnsembleDelete, UnConstrFreshIdx; intros. inversion H2; subst; eauto. * unfold UnIndexedEnsembleListEquivalence; exists (filter (fun a => negb (DecideableEnsembles.dec (indexedElement a))) l''); split; eauto. rewrite <- l''_eq; rewrite ListFacts.filter_map; reflexivity. intuition. apply filter_In; split. eapply l''_eqv; inversion H2; eauto. inversion H2; subst; rewrite (proj2 (Decides_false _ _)); eauto. unfold Complement, Ensembles.In in *. intro; apply H4. rewrite <- H0. apply dec_decides_P; eauto. rewrite filter_In in H2; intuition; constructor; [ apply l''_eqv; eauto | case_eq (DecideableEnsembles.dec (indexedElement x)); intros H'; rewrite H' in H4; try discriminate; eapply Decides_false in H'; eauto ]. unfold Complement, Ensembles.In; rewrite <- H0; eapply Decides_false in H'; rewrite H'; congruence. eapply NoDup_filter_map with (f := fun a => negb (DecideableEnsembles.dec a)); eauto. + 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