proposition: Lemma refine_Update_bupdate : forall or nr search_term update_term, or ≃ benumerate nr -> RepInvPlus nr -> ValidUpdatePlus update_term -> IndexedEnsembleUpdate or (fun tup => bfind_matcher search_term tup = true) (fun old new => new = (bupdate_transform update_term old)) ≃ benumerate (snd (bupdate nr search_term update_term)).
proof: Proof. simpl; intros; destruct_EnsembleIndexedListEquivalence; split. - exists bnd; unfold UnConstrFreshIdx in *; intros; destruct H2; destruct H2; intuition. rewrite H4; apply fresh_bnd; auto; intuition. - pose proof (bupdate_correct nr search_term update_term H0 H1). rewrite partition_filter_neq in H2; rewrite partition_filter_eq in H2. unfold UnIndexedEnsembleListEquivalence in *. unfold EnsembleListEquivalence in *. rewrite <- eqv_or in H2. repeat rewrite filter_map in H2. rewrite map_then_map in H2. rewrite <- map_app in H2. destruct H2 as [H2 H2']. pose proof (permu_exists _ H2). destruct H3 as [? [? ?] ]. exists x. intuition. + eapply Permutation_in. symmetry; apply H4. unfold IndexedEnsembleUpdate in H5; unfold In in H5. inversion H5. * destruct H6. destruct H6 as [ [? [? ?] ] ?]. apply in_app_iff; right; apply in_map_iff. exists x1; intuition. rewrite <- H9. rewrite <- H8; destruct x0; intuition. apply filter_In; intuition. apply eqv_nr; apply H6. rewrite <- H9; rewrite <- H8; destruct x0; intuition. apply filter_In; intuition. apply eqv_nr; apply H6. * destruct H6; unfold Complement in H7; unfold not in H7. apply in_app_iff; left. apply filter_In; intuition; apply eqv_nr; apply H6. + apply Permutation_in with (x:=x0) in H4. rewrite <- H3 in H2. unfold In; unfold IndexedEnsembleUpdate. apply in_app_iff in H4; destruct H4. * right; split; apply filter_In in H4; destruct H4. apply eqv_nr in H4; assumption. unfold Complement; unfold In; intuition. rewrite H7 in H6; inversion H6. * left; apply in_map_iff in H4; destruct H4; destruct H4. exists x1; intuition; apply filter_In in H6; destruct H6. apply eqv_nr; assumption. assumption. rewrite <- H4; intuition. rewrite <- H4; intuition. * assumption. + apply Permutation_map with (f:=elementIndex) in H4. symmetry in H4. apply NoDup_Permutation_rewrite in H4. * assumption. * rewrite -> map_app; rewrite -> map_map; simpl; rewrite <- map_app. apply NoDup_two_partitions; 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