Bitwise ops for integers #1665

digama0 · 2017-06-13T18:55:36Z

Expansion of the previous commit to include VM implementations of integer bitwise operations.

gebner · 2017-06-13T19:52:12Z

library/init/data/int/basic.lean

@@ -382,4 +417,10 @@ by rw -int.sub_nat_nat_eq_coe; exact sub_nat_nat_elim m n
  (λi n, by rw [nat.add_sub_cancel_left]; refl)
  (λi n, by rw [add_assoc, nat.sub_eq_zero_of_le (nat.le_add_right _ _)]; refl)

+#eval do m ← list.range 5,


Debugging code should not be in the library files.

gebner · 2017-06-13T19:52:52Z

library/init/data/int/bitwise.lean

+  | (m : ℕ) n := nat.test_bit m n
+  | -[1+ m] n := bnot (nat.test_bit m n)
+
+  def nat_bitwise (f : bool → bool → bool) (m n : ℕ) : ℤ :=


This function (and bitwise) doesn't seem to be used anywhere. Is there a reason we can't use it for lor, land, etc.?

I'm torn on whether the definitional equality should be the reduction into positive/negative cases as I've done here, or the theorems bitwise or = lor etc. Either way we will have both, but definitional reduction can be important here.

I see, they are used in the theorems at the end of the file.

gebner · 2017-06-13T19:56:51Z

library/init/data/nat/bitwise.lean

+
+  def div2 (n : ℕ) : ℕ := (bodd_div2 n).2
+
+  def bodd (n : ℕ) : bool := (bodd_div2 n).1


What was wrong with n % 2 = 1?

Dependence on WF definitions makes it more complicated for the kernel to reduce the definition. I didn't think it would be important, but it kept breaking proofs in weird ways.

I didn't think it would be important, but it kept breaking proofs in weird ways.

Do you still remember what it broke? As far as I can tell, bodd_div2 n only reduces if n is a numeral. But in this case I would have expected the WF definition to reduce as well.

It's not that it can't reduce; it reduces but only when unfold_lemmas is enabled. This causes a problem for binary_rec_eq, because the type of the theorem includes f ff 0 z = z (where the left side has type C (bit ff 0) and the right side has type C 0), so that any users of this theorem must also have unfold_lemmas enabled in order to reduce bit ff 0 := 0. If they don't, we are in the strange circumstance of having equalities embedded in constants whose type-correctness is not verifiable, and I have no idea what kind of guarantees lean can give in this situation.

Oooh, I see. Yes, this is really, really ugly. And we will probably see this again in the future, since it happens with every WF definition...

I see two potential solutions:

Use equational rfl-lemmas for reduction in the type_context. This is a bit of work, and Leo has mentioned that there are lots of issues here.

As a quick hack, we could special-case acc.rec (and maybe eq.rec and heq.rec?) in the type_context by reducing the major premise using transparency_mode::All.

BTW, we have exactly the same issue with attribute [irreducible].

gebner · 2017-06-13T19:57:50Z

library/init/data/nat/gcd.lean

+
+/- gcd -/
+
+def gcd.F : Π (y : ℕ), (Π (y' : ℕ), y' < y → nat → nat) → nat → nat


Can we define gcd using the equation compiler now?

Yes. We should probably also define div and mod using the equation compiler.

gebner · 2017-06-13T20:19:24Z

BTW, this PR doesn't build.

digama0 · 2017-06-14T06:13:43Z

Errors in the last commit were fixed, and it has been build-tested this time.

gebner · 2017-06-19T08:27:01Z

library/init/data/nat/bitwise.lean

+
+  def div2 (n : ℕ) : ℕ := (bodd_div2 n).2
+
+  def bodd (n : ℕ) : bool := (bodd_div2 n).1


I didn't think it would be important, but it kept breaking proofs in weird ways.

Do you still remember what it broke? As far as I can tell, bodd_div2 n only reduces if n is a numeral. But in this case I would have expected the WF definition to reduce as well.

gebner · 2017-06-19T08:27:19Z

library/init/data/nat/bitwise.lean

+  @[simp] lemma bodd_one : bodd 1 = tt := rfl
+  @[simp] lemma bodd_two : bodd 2 = ff := rfl
+
+  @[simp] def bodd_succ (n : ℕ) : bodd (succ n) = bnot (bodd n) :=


s/def/lemma/g

gebner · 2017-06-19T08:29:34Z

library/init/data/int/bitwise.lean

+  | (m : ℕ) n := nat.test_bit m n
+  | -[1+ m] n := bnot (nat.test_bit m n)
+
+  def nat_bitwise (f : bool → bool → bool) (m n : ℕ) : ℤ :=


I see, they are used in the theorems at the end of the file.

gebner · 2017-06-19T08:30:26Z

@digama0 This PR still has build errors.

digama0 · 2017-06-21T05:32:41Z

I think this PR is ready for merge (or at least ready for others to try to find issues with it) now.

digama0 · 2017-06-27T01:19:03Z

@gebner Is the "request changes" finished?

The type-correctness of binary_rec_eq (the statement, not the proof) depends on unfolding the embedded well-founded definition of mod. This definition avoids it by using two simpler functions bodd and div2 that reduce well in the kernel.

gebner · 2017-06-27T05:42:20Z

Is the "request changes" finished?

I still think that bodd_div2 is hideous, but I get why we need it.

We should define gcd using the equations compiler, but that can be done later. I don't think we can use the equations compiler for div and mod for bootstrapping reasons, since they are required by the tactics framework (more precisely init.data.repr) and the well-founded recursion support requires tactics.

digama0 · 2017-06-27T10:16:09Z

@gebner Actually the latest version of this PR does define gcd using the equation compiler. It did involve changing the definition so that it did induction on the left argument instead of the right, but I suppose gcd is commutative anyway so all the proofs are simply left-right mirrored.

The other reason for bodd_div2, which would remain even if WF definitions worked perfectly, is that it has different definitional equalities. I wanted bodd (succ n) = bnot (bodd n) to be a definitional equality instead of whatever you get with the mod definition.

leodemoura · 2017-06-28T02:00:27Z

Merged based on @gebner approval.

gebner suggested changes Jun 13, 2017

View reviewed changes

digama0 force-pushed the bitwise branch from bcdc7e5 to bb8662d Compare June 14, 2017 07:08

gebner reviewed Jun 19, 2017

View reviewed changes

gebner mentioned this pull request Jun 19, 2017

feat(library/type_context): unfold lemmas in major premise of acc.rec #1680

Closed

digama0 force-pushed the bitwise branch from bb8662d to 6b8fc62 Compare June 21, 2017 05:08

digama0 force-pushed the bitwise branch 3 times, most recently from 517a8c2 to c93b2c7 Compare June 22, 2017 23:51

digama0 added 7 commits June 26, 2017 21:20

feat(library/vm/vm_nat): implementation of new bitwise ops

9618c6d

feat(init/data/int): bitwise ops for integers

2d45846

feat(init/data/int): prove int bitwise ops

3ad8537

feat(init/data/int): int lemmas, more bitwise theorems

d73fa9c

fix(tests/lean): fix tests

d647cf7

refactor(init/data/nat/gcd): define gcd using eqn compiler

56752ce

digama0 force-pushed the bitwise branch from c93b2c7 to 56752ce Compare June 27, 2017 01:21

gebner approved these changes Jun 27, 2017

View reviewed changes

leodemoura closed this Jun 28, 2017

digama0 deleted the bitwise branch June 28, 2017 02:56

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Bitwise ops for integers #1665

Bitwise ops for integers #1665

digama0 commented Jun 13, 2017

gebner Jun 13, 2017

gebner Jun 13, 2017

digama0 Jun 13, 2017 •

edited

gebner Jun 19, 2017

gebner Jun 13, 2017

digama0 Jun 13, 2017

gebner Jun 19, 2017

digama0 Jun 19, 2017

gebner Jun 19, 2017

gebner Jun 13, 2017

digama0 Jun 13, 2017

gebner commented Jun 13, 2017

digama0 commented Jun 14, 2017

gebner Jun 19, 2017

gebner Jun 19, 2017

gebner Jun 19, 2017

gebner commented Jun 19, 2017

digama0 commented Jun 21, 2017

digama0 commented Jun 27, 2017

gebner commented Jun 27, 2017

digama0 commented Jun 27, 2017

leodemoura commented Jun 28, 2017


		def div2 (n : ℕ) : ℕ := (bodd_div2 n).2

		def bodd (n : ℕ) : bool := (bodd_div2 n).1


		/- gcd -/

		def gcd.F : Π (y : ℕ), (Π (y' : ℕ), y' < y → nat → nat) → nat → nat

Bitwise ops for integers #1665

Bitwise ops for integers #1665

Conversation

digama0 commented Jun 13, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 Jun 13, 2017 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gebner commented Jun 13, 2017

digama0 commented Jun 14, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gebner commented Jun 19, 2017

digama0 commented Jun 21, 2017

digama0 commented Jun 27, 2017

gebner commented Jun 27, 2017

digama0 commented Jun 27, 2017

leodemoura commented Jun 28, 2017

digama0 Jun 13, 2017 •

edited