Commit 2020-04-24 11:14 13393e3c

chore(data/list/*): various renamings to use dot notation (#2481)

• use dot notation
• add a version of list.perm.prod_eq that only assumes that elements of the list pairwise commute instead of commutativity of the monoid.

List of renamed symbols

data/list/basic

• append_sublist_append_of_sublist_right : sublist.append_right;
• reverse_sublist : sublist.reverse;
• append_sublist_append : sublist.append;
• subset_of_sublist: sublist.subset;
• sublist_antisymm : sublist.antisymm;
• filter_map_sublist_filter_map : sublist.filter_map
• map_sublist_map : sublist.map
• erasep_sublist_erasep: sublist.erasep
• erase_sublist_erase : sublist.erase;
• diff_sublist_of_sublist : sublist.diff_right;

data/list/perm

• perm.skip : perm.cons;
• perm_comm (new);
• perm_subset : perm.subset;
• mem_of_perm : perm.mem_iff;
• perm_app_left : perm.append_right (note right vs left)
• perm_app_right : perm.append_left (note right vs left)
• perm_app : perm.append;
• perm_app_cons : perm.append_cons;
• perm_cons_app : perm_append_singleton;
• perm_app_comm : perm_append_comm;
• perm_length : perm.length_eq;
• eq_nil_of_perm_nil : perm.eq_nil and perm.nil_eq with different choices of lhs/rhs;
• eq_singleton_of_perm_inv : perm.eq_singleton and perm.singleton_eq with different choices of lhs/rhs;
• perm_singleton and singleton_perm: iff versions of perm.eq_singleton and perm.singleton_eq;
• eq_singleton_of_perm : singleton_perm_singleton;
• perm_cons_app_cons : perm_cons_append_cons;
• perm_repeat : repeat_perm; new perm_repeat differs from it in the choice of lhs/rhs;
• perm_erase : perm_cons_erase;
• perm_filter_map : perm.filter_map;
• perm_map : perm.map;
• perm_pmap : perm.pmap;
• perm_filter : perm.filter;
• subperm_of_sublist : sublist.subperm;
• subperm_of_perm : perm.subperm;
• subperm.refl : now has @[refl] attribute;
• subperm.trans : now has @[trans] attribute;
• length_le_of_subperm : subperm.length_le;
• subset_of_subperm : subperm.subset;
• exists_perm_append_of_sublist : sublist.exists_perm_append;
• perm_countp : perm.countp_eq;
• countp_le_of_subperm : subperm.countp_le;
• perm_count : perm.count_eq;
• count_le_of_subperm : subperm.count_le;
• foldl_eq_of_perm : perm.foldl_eq, added a primed version with slightly weaker assumptions;
• foldr_eq_of_perm : perm.foldr_eq;
• rec_heq_of_perm : perm.eec_heq;
• fold_op_eq_of_perm : perm.fold_op_eq;
• prod_eq_of_perm: perm.prod_eq and perm.prod_eq';
• perm_cons_inv : perm.cons_inv;
• perm_cons : now is a @[simp] lemma;
• perm_app_right_iff : perm_append_right_iff;
• subperm_app_left : subperm_append_left;
• subperm_app_right : subperm_append_right;
• perm_ext_sublist_nodup : nodup.sublist_ext;
• erase_perm_erase : perm.erase;
• subperm_cons_erase (new);
• erase_subperm_erase : subperm.erase;
• perm_diff_left : perm.diff_right (note left vs right);
• perm_diff_right : perm.diff_left (note left vs right);
• perm.diff, subperm.diff_right, erase_cons_subperm_cons_erase (new);
• perm_bag_inter_left : perm.bag_inter_right (note left vs right);
• perm_bag_inter_right : perm.bag_inter_left (note left vs right);
• perm.bag_inter (new);
• perm_erase_dup_of_perm : perm.erase_dup;
• perm_union_left : perm.union_right (note left vs right);
• perm_union_right : perm.union_left (note left vs right);
• perm_union : perm.union;
• perm_inter_left : perm.inter_right (note left vs right);
• perm_inter_right : perm.inter_left (note left vs right);
• perm_inter : perm.inter;
• perm_nodup : perm.nodup_iff;
• perm_bind_left : perm.bind_right (note left vs right);
• perm_bind_right : perm.bind_left (note left vs right);
• perm_product_left : perm.product_right (note left vs right);
• perm_product_right : peerm.product_left (note left vs right);
• perm_product : perm.product;
• perm_erasep : perm.erasep;

data/list/sigma

• nodupkeys.pairwise_ne (new);
• perm_kreplace : perm.kreplace;
• perm_kerase : perm.kerase;
• perm_kinsert : perm.kinsert;
• erase_dupkeys_cons : now take x : sigma β instead of {x : α} and {y : β x};
• perm_kunion_left : perm.kunion_right (note left vs right);
• perm_kunion_right : perm.kunion_left (note left vs right);
• perm_kunion : perm.kunion;