Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

native.rb_map.insert not working as expected #738

Open
1 task done
isadofschi opened this issue Jul 10, 2022 · 2 comments
Open
1 task done

native.rb_map.insert not working as expected #738

isadofschi opened this issue Jul 10, 2022 · 2 comments

Comments

@isadofschi
Copy link

Prerequisites

  • Put an X between the brackets on this line if you have done all of the following:
    • Checked that your issue isn't already filed.
    • Reduced the issue to a self-contained, reproducible test case.

Description

Inserting to an rb_map is not working as expected:

import init.meta
import order.basic

-- evaluates to [(4, 5), (2, 3)] as expected
#eval (((native.rb_map.of_list ([] : list (ℕ × ℕ))).insert 2 3).insert 4 5).to_list

-- evaluates to [(tt, 3), (ff, 5)] as expected
#eval (((native.rb_map.of_list ([] : list (bool × ℕ))).insert tt 3).insert ff 5).to_list

-- evaluates to [((ff, 4), 5)] instead of  [((tt, 2), 3), ((ff, 4), 5)]
#eval (((native.rb_map.of_list ([] : list ((bool × ℕ) × ℕ ))).insert (tt,2) 3).insert (ff,4) 5).to_list

Steps to Reproduce

  1. This can be easily reproduced in gitpod with the latest mathlib.

Expected behavior: expression evaluates to [((tt, 2), 3), ((ff, 4), 5)]

Actual behavior: expression evaluates to [((ff, 4), 5)]

Reproduces how often: always

Versions

  • On gitpod: Lean (version 3.44.1, commit 9d5adc6, Release) and mathlib 861589f224456f278c61596c0ee8a1ba449a6e8b

  • On my PC (Ubuntu 20.04) Lean (version 3.42.1, commit 68455b0, Release)

@isadofschi
Copy link
Author

isadofschi commented Jul 10, 2022

Could this be happening because the order in bool × ℕ is not a total ordering?

Edit: yes, it seems that was the problem:

import init.meta
import order.lexicographic

#eval (((native.rb_map.of_list ([] : list ((bool ×ₗ ℕ) × ℕ ))).insert (tt,2) 3).insert (ff,4) 5).size

I don't know if we can require here that the ordering is a total order since rb_map is meta. For the "non meta" rbmap there seems to be a similar issue:

import order.basic

#eval (( (rbmap.from_list ([] : list ((bool×ℕ ) × ℕ))).insert (tt,2) 3).insert (ff,4) 5).to_list

If this is expected behaviour we probably want to document a reminder somewhere in mathlib_docs.

@fpvandoorn
Copy link
Member

Feel free to make a PR that adds docstrings/module docs explaining that the ordering needs to be total.
We can probably also change the definitions to require a linear_order, since the definition is nonsensical otherwise (incomparable elements are treated as equal, which is generally not a transitive relationship), but I'm not sure if that will have unfortunate side effects.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants