Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-21 20:56 3b9cbdfe

View on Github →

feat(data/ordmap): Ordered maps (like rb_map but better) (#5353) This cleans up an old mathlib branch from 2 years ago, so it probably isn't in very modern style, but it would be best to get it merged and kept up to date rather than leaving it to rot. It is an implementation of size balanced ordered maps based on Haskell's Data.Map.Strict. The ordnode structure can be used directly if one is only interested in using it for programming purposes, and the ordset structure bundles the proofs so that you can prove theorems about inserting and deleting doing what you expect.

Estimated changes

added def cmp_le
added theorem cmp_le_eq_cmp
added theorem cmp_le_swap
added def ordnode.all
added def ordnode.alter
added def ordnode.amem
added def ordnode.any
added def ordnode.attach'
added def ordnode.balance
added def ordnode.delta
added def ordnode.diff
added def ordnode.disjoint
added def ordnode.drop
added def ordnode.drop_aux
added def ordnode.dual
added def ordnode.emem
added def ordnode.empty
added def ordnode.equiv
added def ordnode.erase
added def ordnode.filter
added def ordnode.find
added def ordnode.find_ge
added def ordnode.find_gt
added def ordnode.find_le
added def ordnode.find_lt
added def ordnode.find_max
added def ordnode.find_min
added def ordnode.fold
added def ordnode.foldl
added def ordnode.foldr
added def ordnode.glue
added def ordnode.image
added def ordnode.insert'
added def ordnode.inter
added def ordnode.link
added def ordnode.map
added def ordnode.mem
added def ordnode.merge
added def ordnode.node'
added def ordnode.nth
added def ordnode.of_list'
added def ordnode.of_list
added def ordnode.pmap
added def ordnode.powerset
added def ordnode.ratio
added def ordnode.repr
added def ordnode.size
added def ordnode.span
added def ordnode.split3
added def ordnode.split
added def ordnode.split_at
added def ordnode.take
added def ordnode.take_aux
added def ordnode.to_list
added def ordnode.union
added inductive ordnode
added theorem ordnode.all.imp
added theorem ordnode.all_balance'
added theorem ordnode.all_balance_l
added theorem ordnode.all_balance_r
added theorem ordnode.all_dual
added theorem ordnode.all_iff_forall
added theorem ordnode.all_node'
added theorem ordnode.all_node3_l
added theorem ordnode.all_node3_r
added theorem ordnode.all_node4_l
added theorem ordnode.all_node4_r
added theorem ordnode.all_rotate_l
added theorem ordnode.all_rotate_r
added theorem ordnode.all_singleton
added theorem ordnode.any.imp
added theorem ordnode.any_iff_exists
added theorem ordnode.any_singleton
added def ordnode.balance'
added theorem ordnode.balanced.dual
added def ordnode.balanced
added theorem ordnode.balanced_sz_up
added theorem ordnode.bounded.dual
added theorem ordnode.bounded.mem_gt
added theorem ordnode.bounded.mem_lt
added theorem ordnode.bounded.of_gt
added theorem ordnode.bounded.of_lt
added theorem ordnode.bounded.to_lt
added theorem ordnode.bounded.to_nil
added theorem ordnode.bounded.to_sep
added theorem ordnode.bounded.weak
added def ordnode.bounded
added theorem ordnode.delta_lt_false
added theorem ordnode.dual_balance'
added theorem ordnode.dual_balance_l
added theorem ordnode.dual_balance_r
added theorem ordnode.dual_dual
added theorem ordnode.dual_erase_max
added theorem ordnode.dual_erase_min
added theorem ordnode.dual_insert
added theorem ordnode.dual_node'
added theorem ordnode.dual_node3_l
added theorem ordnode.dual_node3_r
added theorem ordnode.dual_node4_l
added theorem ordnode.dual_node4_r
added theorem ordnode.dual_rotate_l
added theorem ordnode.dual_rotate_r
added theorem ordnode.emem_iff_all
added theorem ordnode.equiv_iff
added theorem ordnode.find_max'_all
added theorem ordnode.find_max'_dual
added theorem ordnode.find_max_dual
added theorem ordnode.find_min'_all
added theorem ordnode.find_min'_dual
added theorem ordnode.find_min_dual
added theorem ordnode.insert'.valid
added theorem ordnode.insert.valid
added theorem ordnode.length_to_list
added theorem ordnode.merge_nil_left
added theorem ordnode.merge_node
added def ordnode.node3_l
added theorem ordnode.node3_l_size
added def ordnode.node3_r
added theorem ordnode.node3_r_size
added def ordnode.node4_l
added theorem ordnode.node4_l_size
added def ordnode.node4_r
added theorem ordnode.not_le_delta
added theorem ordnode.raised.dist_le
added theorem ordnode.raised.right
added def ordnode.raised
added theorem ordnode.raised_iff
added def ordnode.rotate_l
added def ordnode.rotate_r
added theorem ordnode.size_balance'
added theorem ordnode.size_balance_l
added theorem ordnode.size_balance_r
added theorem ordnode.size_dual
added theorem ordnode.sized.balance'
added theorem ordnode.sized.dual
added theorem ordnode.sized.dual_iff
added theorem ordnode.sized.eq_node'
added theorem ordnode.sized.node'
added theorem ordnode.sized.node3_l
added theorem ordnode.sized.node3_r
added theorem ordnode.sized.node4_l
added theorem ordnode.sized.pos
added theorem ordnode.sized.rotate_l
added theorem ordnode.sized.rotate_r
added theorem ordnode.sized.size_eq
added def ordnode.sized
added theorem ordnode.split_max_eq
added theorem ordnode.split_min_eq
added theorem ordnode.to_list_nil
added theorem ordnode.to_list_node
added theorem ordnode.valid'.balance
added theorem ordnode.valid'.dual
added theorem ordnode.valid'.glue
added theorem ordnode.valid'.left
added theorem ordnode.valid'.node'
added theorem ordnode.valid'.node3_l
added theorem ordnode.valid'.node3_r
added theorem ordnode.valid'.node4_l
added theorem ordnode.valid'.node
added theorem ordnode.valid'.of_gt
added theorem ordnode.valid'.of_lt
added theorem ordnode.valid'.right
added theorem ordnode.valid'.valid
added structure ordnode.valid'
added theorem ordnode.valid'_nil
added theorem ordnode.valid.dual
added theorem ordnode.valid.dual_iff
added theorem ordnode.valid.left
added theorem ordnode.valid.merge
added theorem ordnode.valid.right
added theorem ordnode.valid.size_eq
added def ordnode.valid
added theorem ordnode.valid_nil
added def ordset.empty
added theorem ordset.empty_iff
added def ordset.insert'
added def ordset.nil
added def ordset.size
added def ordset