proposition: Lemma refine_Delete_bdelete : forall or nr search_term, or ≃ benumerate nr -> RepInvPlus nr -> EnsembleDelete or (fun tup => bfind_matcher search_term tup = true) ≃ benumerate (snd (bdelete nr search_term)).
proof: Proof. simpl; intros; destruct_EnsembleIndexedListEquivalence; clear H. split. - exists bnd; unfold UnConstrFreshIdx in *; intros; apply fresh_bnd; destruct H; eauto. - pose proof (bdelete_correct nr search_term H0); intuition. rewrite partition_filter_neq in H1; symmetry in H1. destruct (permutation_filter _ _ _ H1) as [l [l_eq Perm_l] ]. symmetry in Perm_l. destruct (permutation_map_base indexedElement Perm_l _ eqv_or) as [l' [l'_eq Perm_l'] ]. exists (filter (fun a => negb (bfind_matcher search_term (indexedElement a))) l'); repeat split. + rewrite <- l_eq, <- l'_eq, filter_map; reflexivity. + unfold In, EnsembleDelete; intros. inversion H; subst. unfold In, Complement, In in *. rewrite <- partition_filter_neq. rewrite <- partition_filter_neq in l_eq. rewrite eqv_nr in H3. rewrite (In_partition (fun itup => bfind_matcher search_term (indexedElement itup))) in H3; intuition. rewrite partition_filter_eq, filter_In in H5; intuition. rewrite partition_filter_neq, filter_In in H5; rewrite partition_filter_neq, filter_In; intuition. symmetry in Perm_l'; eapply Permutation_in; eauto. + unfold In, EnsembleDelete; intros. rewrite filter_In in H; intuition. apply eqv_nr; eapply Permutation_in; eauto. + unfold In, Complement, In in *. rewrite filter_In in H; intuition. rewrite H3 in H5; discriminate. + apply Permutation_map with (f:=elementIndex) in Perm_l'. symmetry in Perm_l'; apply NoDup_Permutation_rewrite in Perm_l'. apply NoDup_filter_in_map; assumption. assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsInterface Fiat.QueryStructure.Implementation.DataStructures.Bags.CountingListBags Fiat.QueryStructure.Implementation.DataStructures.Bags.TreeBags Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist Coq.Bool.Bool Coq.Strings.String Coq.Arith.Arith Coq.Structures.OrderedTypeEx Fiat.Common.String_as_OT Fiat.Common.i2list Fiat.Common.DecideableEnsembles Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.ADTRefinement.GeneralBuildADTTactics Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.Bags.BagsOfTuples Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.Common.List.ListFacts TransparentAbstract