Gray code

Stream: mathlib4

[Daniel Weber]

I have defined reflected binary gray code and proved some theorems about it in Lean. Is this something which could be added to Mathlib? Where?

I have also proved a few simple lemmas about bitwise operators - would it be OK to add them as simp lemmas? There is also a problem that simp uses Nat.bit_false and Nat.bit_true, which change stuff to bit0 and bit1, but they are deprecated. What's going on with that?

• bit_testBit_zero: (Nat.bit b n).testBit 0 = b
• bit_div2: (Nat.bit b n).div2 = n
• succ_bit_true: Nat.bit true n + 1 = Nat.bit false (n+1)
• succ_bit_false: Nat.bit false n + 1 = Nat.bit true n
• succ_testBit_zero: (n + 1).testBit 0 = !n.testBit 0
• bit_testBit_nonzero (h : i ≠ 0): (Nat.bit b n).testBit i = n.testBit (i-1)
• div2_testBit: n.div2.testBit i = n.testBit (i+1)
• xor_div2: (n ^^^ m).div2 = n.div2 ^^^ m.div2

[Kim Morrison]

Yes, it would be good to remove @[simp] from bit_false and bit_true.

[Kim Morrison]

I'm skeptical that bit_testBit_nonzero is useful (introduces a subtraction), but I guess the others are probably okay.

[Yaël Dillies]

Probably bit_testBit_succ : (Nat.bit b n).testBit (i + 1) = n.testBit i is better?

[Daniel Weber]

Yaël Dillies said:

Probably bit_testBit_succ : (Nat.bit b n).testBit (i + 1) = n.testBit i is better?

Yeah, seems so. Then I can replace by_cases i = 0 in my proof with cases i and everything is nicer

[Daniel Weber]

Ah, it exists already, docs#Nat.testBit_bit_succ

[Daniel Weber]

as does docs#Nat.testBit_bit_zero

[Daniel Weber]

and docs#Nat.div2_bit

[Daniel Weber]

It's a bit annoying that everything Init.Data.Nat.Bitwise.Lemmas is spelled with n / 2 while in Mathlib.Data.Nat.Bits everything is spelled with div2, but they aren't defeq

[Yuyang Zhao]

lean4#3756 and #12419 will make them defeq and provide some lemmas.

[Daniel Weber]

What would be a good location for this file? Mathlib.Data.Nat.GrayCode?

[Eric Wieser]

I'd argue that gray codes should be about BitVector not Nat

[Daniel Weber]

I first state everything as a permutation of Nat and then look at prefixes of it for BitVec

[Daniel Weber]

It slightly annoys me that it depends on choice even though there's no reason for it to. Any idea why Lean.Omega.normalize_sat depends on Classical.em? It seems to be due to the split, but its condition should be decidable

[Yaël Dillies]

... you opened a big can of worms right there

[Yaël Dillies]

lean4#2414

[Ruben Van de Velde]

If you want people to keep paying attention to your thread, I recommend not going much further in that direction :)

[Kim Morrison]

@Yuyang Zhao, there is an old request for motivation for lean4#3756 that hasn't been answered.

[Daniel Weber]

#12750 made a pull request

[Kim Morrison]

Could you move the non-gray code material into a separate PR? It will make reviewing easier.

[Daniel Weber]

Sorry, I don't have much experience with git–how do I do that?

[Kim Morrison]

To keep it simple, you can just:

git checkout master
git checkout -b pre_gray_code
git checkout CommandMaster_GrayCode <filenames containing the earlier material>
git commit -am "...."
git push

and make a new PR from that.

[Daniel Weber]

:thumbs_up: #12751

[Daniel Weber]

Daniel Weber said:

:thumbs_up: #12751

Is anyone available to take a look at this?

[Yaël Dillies]

In a month, after my exams... :grimacing:

[Rida Hamadani]

Daniel Weber said:

:thumbs_up: #12751

LGTM

[Rida Hamadani]

I wonder if size_eq_iff_testBit can be simplified more though ...