proposition: Lemma refine_Update_invalid : forall or nr search_term update_term, or ≃ benumerate nr -> RepInvPlus nr -> IndexedEnsembleUpdate or (fun tup => bfind_matcher search_term tup = true) (fun old new => new = (bupdate_transform update_term old)) ≃ benumerate (fold_left (fun (b0 : BagTypePlus) (i : RawTuple) => binsert b0 i) (map (bupdate_transform update_term) (fst (bdelete nr search_term))) (snd (bdelete nr search_term))).
proof: Proof. simpl; intros; destruct_EnsembleIndexedListEquivalence; split. - exists bnd; unfold UnConstrFreshIdx in *. intros; destruct H1; destruct H1; intuition. rewrite H3; apply fresh_bnd; auto; intuition. - pose proof (bdelete_correct nr search_term H0); intuition. unfold UnIndexedEnsembleListEquivalence in *. rewrite <- eqv_or in H2, H3. rewrite partition_filter_neq in H2; symmetry in H2. rewrite partition_filter_eq in H3; symmetry in H3. pose proof (permutation_double_filter _ _ H3 H2). destruct H1; destruct H1 as [? [? ?] ]. symmetry in H5. pose proof (permu_exists _ H5); destruct H6; destruct H6. pose proof (permutation_map indexedElement (( filter (fun t => negb (bfind_matcher search_term (indexedElement t))) x0) ++ map (fun t => {|indexedElement := (bupdate_transform update_term) (indexedElement t); elementIndex := elementIndex t|}) (filter (fun t => bfind_matcher search_term (indexedElement t)) x0)) (benumerate (fold_left (fun (b0 : BagTypePlus) (i : RawTuple) => binsert b0 i) (map (bupdate_transform update_term) (fst (bdelete nr search_term))) (snd (bdelete nr search_term))))). assert ( Permutation (benumerate (fold_left (fun (b0 : BagTypePlus) (i : RawTuple) => binsert b0 i) (map (bupdate_transform update_term) (fst (bdelete nr search_term))) (snd (bdelete nr search_term)))) (map indexedElement (filter (fun t : IndexedElement => negb (bfind_matcher search_term (indexedElement t))) x0 ++ map (fun t : IndexedElement => {| elementIndex := elementIndex t; indexedElement := bupdate_transform update_term (indexedElement t) |}) (filter (fun t : IndexedElement => bfind_matcher search_term (indexedElement t)) x0)))). rewrite -> benumerate_fold_left. rewrite <- H1; rewrite <- H4; rewrite -> map_app. let lem := constr:(fun A => @filter_map A _ (fun t => negb (bfind_matcher search_term t))) in rewrite <- lem. rewrite <- map_then_map; rewrite <- filter_map. repeat rewrite <- H6; rewrite -> Permutation_app_comm; intuition. apply bdelete_RepInv; assumption. destruct H8. intuition. pose proof (permu_exists _ H9); destruct H10 as [? [? ?] ]; clear H9. exists x2. intuition. + unfold In, IndexedEnsembleUpdate in *. intuition. * destruct H12; intuition. rewrite -> H8 in H10; symmetry in H10; apply eqv_nr in H9; symmetry in H7. pose proof (Permutation_in _ H7 H9). eapply Permutation_in. symmetry; apply H11. apply in_app_iff; right; apply in_map_iff. exists x4; intuition. rewrite <- H13; rewrite <- H15; destruct x3; reflexivity. apply filter_In; intuition. * unfold Complement, not, In in *. eapply Permutation_in. symmetry; apply H11. apply in_app_iff; left. apply eqv_nr in H9; rewrite <- H7 in H9. apply filter_In; intuition. + unfold In, IndexedEnsembleUpdate, Complement. apply Permutation_in with (x:=x3) in H11. apply in_app_iff in H11; destruct H11. * right; rewrite filter_In in H11; destruct H11; split. rewrite -> eqv_nr; rewrite <- H7. assumption. unfold not, In; intros. rewrite -> H13 in H12; simpl in H12; intuition. * left; apply in_map_iff in H11; destruct H11; destruct H11; exists x4. rewrite filter_In in H12; destruct H12; intuition. apply eqv_nr; rewrite <- H7; assumption. rewrite <- H11; intuition. rewrite <- H11; intuition. * assumption. + apply Permutation_map with (f:=elementIndex) in H7; symmetry in H7. apply Permutation_map with (f:=elementIndex) in H11. eapply NoDup_Permutation_rewrite. symmetry; apply H11. rewrite -> map_app; rewrite -> map_map; simpl; rewrite <- map_app; apply NoDup_two_partitions. apply NoDup_Permutation_rewrite in H7; 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