Adding binary numbers

Stream: new members

[Ben Nale]

Hi all,
I don't think I'm smart enough to prove this in Lean. Kindly help.

import Mathlib

infix:30 " ^^ " => xor

def carry (x y : Nat) (i : Nat) : Bool := match i with
  | 0     => false
  | i + 1 =>
    (Nat.testBit x i && Nat.testBit y i) || ((Nat.testBit x i ^^ Nat.testBit y i) && carry x y i)

theorem pls_halp  {x y : Nat} : (x + y).testBit i = ((x.testBit i ^^ y.testBit i) ^^ carry x y i)

[Kevin Buzzard]

Can you re-ask your question (just edit the post above) as a #mwe (click on the link for more info)? Right now I have errors when I post your code into Lean. (thanks!)

[Ben Nale]

fixed :). This is using Lean 4

[Violeta Hernández]

I believe the usual math problem solving techniques apply here

[Violeta Hernández]

These being
a) try solving smaller problems first
b) if in doubt about a theorem on naturals, use induction

[Violeta Hernández]

This was a really nice but really hard exercise. Took about 7 hours total. Seems like we're missing a lot of API for bitwise operations. You're welcome to improve on my code:

Proof

import Mathlib.Data.Int.Bitwise

infix:30 " ^^ " => xor

namespace Bool

@[simp] lemma not_xor : ∀ x y : Bool, (!(x ^^ y)) = (x == y) := by decide
@[simp] lemma xor_not_left' : ∀ x y : Bool, (!x ^^ y) = (x == y) := by decide
@[simp] lemma xor_not_right' : ∀ x y : Bool, (x ^^ !y) = (x == y) := by decide

@[simp] lemma xor_eq_left : ∀ x y : Bool, ((x ^^ y) == x) = !y := by decide
@[simp] lemma xor_eq_right : ∀ x y : Bool, ((x ^^ y) == y) = !x := by decide

@[simp] lemma xor_left_inj : ∀ x y z : Bool, (x ^^ y) = (x ^^ z) ↔ y = z := by decide
@[simp] lemma xor_right_inj : ∀ x y z : Bool, (x ^^ z) = (y ^^ z) ↔ x = y := by decide

/-- Whether x + y + z produces a carry. Is true iff at least two of x, y, z are. -/
def carry (x y z : Bool) := x && y || (x ^^ y) && z

@[simp] lemma carry_self_self : ∀ x y, carry x x y = x := by decide

@[simp] lemma carry_false₁ : ∀ y z, carry false y z = (y && z) := by decide
@[simp] lemma carry_false₂ : ∀ x z, carry x false z = (x && z) := by decide
@[simp] lemma carry_false₃ : ∀ x y, carry x y false = (x && y) := by decide

@[simp] lemma carry_true₁ : ∀ y z, carry true y z = (y || z) := by decide
@[simp] lemma carry_true₂ : ∀ x z, carry x true z = (x || z) := by decide
@[simp] lemma carry_true₃ : ∀ x y, carry x y true = (x || y) := by decide

lemma carry_comm : ∀ x y z, carry x y z = carry y x z := by decide

end Bool

namespace Nat

variable (x y i : Nat)

lemma shiftr_one : x.shiftr 1 = div2 x := rfl

lemma shiftr_succ : x.shiftr i.succ = div2 (x.shiftr i) := rfl

lemma shiftr_succ' : x.shiftr i.succ = (div2 x).shiftr i := by
rw [←shiftr_one, ←shiftr_add, succ_eq_one_add]

@[simp] lemma shiftr_bit (b : Bool) : shiftr (bit b x) i.succ = shiftr x i := by
rw [shiftr_succ', div2_bit]

-- why are Nat.zero_shiftr and Nat.shiftr_zero the same and neither is this one?
@[simp] lemma zero_shiftr' : x.shiftr 0 = x := rfl

@[simp] lemma testBit_zero_left : testBit 0 i = false := by
simp [testBit]

@[simp] lemma testBit_zero_right : x.testBit 0 = x.bodd := by
simp [testBit]

lemma testBit_succ_right : x.testBit i.succ = (div2 x).testBit i := by
rw [testBit, succ_eq_one_add, shiftr_add]
rfl

@[simp] lemma testBit_one_succ : testBit 1 i.succ = false := by
rw [testBit_succ_right, div2_one, testBit_zero_left]

@[simp] lemma testBit_one_zero : testBit 1 0 = true := rfl

@[simp] lemma testBit_bit (b : Bool) : testBit (bit b x) i.succ = testBit x i := by
rw [testBit, shiftr_bit]
rfl

-- Should be marked simp in Mathlib.
attribute [simp] bodd_bit div2_bit bit_zero

@[simp] lemma succ_bit0 : (bit false x).succ = bit true x := rfl
@[simp] lemma succ_bit1 : (bit true x).succ = bit false x.succ := by
simp [bit, Nat.bit0_succ_eq]
rfl

lemma bit_succ (b : Bool) : bit b x.succ = (bit b x).succ.succ := match b with
| false => Nat.bit0_succ_eq x
| true => Nat.bit1_succ_eq x

lemma bit1_add' : bit true x + bit true y = bit false (x + y).succ := by
change bit false x + 1 + (bit false y + 1) = _ rw [add_add_add_comm, ←bit_add, bit_succ]

/-! ## Carry theorem -/

def carry (x y i : Nat) : Bool := match i with
| 0 => false
| i + 1 => Bool.carry (Nat.testBit x i) (Nat.testBit y i) (carry x y i)

@[simp] lemma carry_zero : carry x y 0 = false := rfl

lemma carry_succ :
carry x y i.succ = Bool.carry (Nat.testBit x i) (Nat.testBit y i) (carry x y i) :=
rfl

lemma carry_comm : carry x y i = carry y x i := by
induction' i with i IH
· rfl
· rw [carry_succ, carry_succ, Bool.carry_comm, IH]

@[simp] lemma carry_zero' : carry 0 y i = false := by
induction' i with i IH
· rfl
· simp [carry_succ, IH]

@[simp] lemma carry_zero'' : carry x 0 i = false := by
rw [carry_comm, carry_zero']

@[simp] lemma carry_bit0_left (b : Bool) : carry (bit false x) (bit b y) i.succ = carry x y i := by
induction' i with i IH
· rw [carry_succ]
simp
· rw [carry_succ]
simp [IH]
rfl

@[simp] lemma carry_bit0_right (b : Bool) : carry (bit b x) (bit false y) i.succ = carry x y i := by
rw [carry_comm, carry_bit0_left, carry_comm]

@[simp] lemma carry_bit0_one : carry (bit false x) 1 i = false := by
cases i
· rfl
· change carry _ (bit true 0) _ = _ rw [carry_bit0_left, carry_zero'']

@[simp] lemma carry_bit1_one_succ_succ :
carry (bit true x) 1 i.succ.succ = carry x 1 i.succ := by
induction' i with i IH
· simp [carry_succ]
· rw [carry_succ, carry_succ x 1 (succ i)]
simp [IH]

@[simp] lemma carry_bit1_bit0_bit1 :
carry (bit true (bit false x)) (bit true y) i.succ.succ =
carry (bit true x) y i.succ := by
induction' i with i IH
· simp [carry_succ]
· rw [carry_succ, carry_succ (bit true x)]
simp [IH]

@[simp] lemma carry_bit1_bit1_bit0 :
carry (bit true x) (bit true (bit false y)) i.succ.succ =
carry x (bit true y) i.succ := by
rw [carry_comm, carry_bit1_bit0_bit1, carry_comm]

@[simp] lemma carry_bit1_bit1_bit1_bit1 :
carry (bit true (bit true x)) (bit true (bit true y)) i.succ.succ =
carry (bit true x) (bit true y) i.succ := by
induction' i with i IH
· simp [carry_succ]
· rw [carry_succ, carry_succ (bit true x)]
simp [IH]

lemma carry_bit1_bit1 : ∀ x y,
carry (bit true x) (bit true y) i.succ.succ =
(carry x 1 i.succ ^^ carry (succ x) y i.succ) := by
induction' i with i IH
· have : ∀ a b : Bool, (a || b) = (a ^^ !a && b) := by decide
simp [carry_succ, this]
· intro x y
apply x.bitCasesOn
apply y.bitCasesOn
rintro (_ | _) x (_ | _) y
· rw [carry_succ]
simp [IH]
rfl
· simp [IH]
· simp
· simp [IH]

lemma carry_bit1_one : carry (bit true x) 1 i.succ.succ = carry x 1 i.succ := by
induction' i with i IH
· simp [carry_succ]
· rw [carry_succ, carry_succ x]
simp [IH]

lemma testBit_succ_one : x.succ.testBit 1 = (x.testBit 1 ^^ bodd x) := by
induction' x with x IH
· rfl
· apply x.bitCasesOn
rintro (_ | _) x
all_goals simp [IH, testBit, shiftr_one, div2_succ]

lemma testBit_succ_succ : ∀ x, x.succ.testBit i.succ = (x.testBit i.succ ^^ carry x 1 i.succ) := by
induction' i with i IH
· simp [carry_succ]
exact testBit_succ_one
· intro x
apply x.bitCasesOn
rintro (_ | _) x
· simp [testBit_succ_right _ i.succ, carry_bit0_one]
· simp [testBit_succ_right _ i.succ, IH, carry_bit1_one]

theorem testBit_add :
∀ x y, (x + y).testBit i = ((x.testBit i ^^ y.testBit i) ^^ carry x y i) := by
induction' i with i IH
· simp
· intro x y
apply x.bitCasesOn
apply y.bitCasesOn
rintro (_ | _) x (_ | _) y
· simp [←bit_add, IH]
· simp [←bit_add', IH]
· simp [←bit_add, IH]
· rw [bit1_add', ←add_succ]
simp [IH]
cases' i with i
· simp [carry_succ]
· rw [carry_comm (bit true y), carry_bit1_bit1, testBit_succ_succ]
simp [carry_comm]

end Nat

[Violeta Hernández]

I do apologize for the wall of text, I was hoping Zulip would auto-hide it

[Violeta Hernández]

Here's some general pointers as to how I came up with all of this code:

• Lean rewards you if you take the time to fill in the basic API. No matter how trivial, marking the easy stuff as simp can be really helpful down the line.
• It's really easy to get lost in a wall of Lean symbols. If you find that the easiest route doesn't work, try working through the problem on paper, then translate that into Lean code.
• If faced with a hard problem, it's a good idea to try simpler problems first. They'll often appear as lemmas in the harder one.

[Violeta Hernández]

I hope the goal here was for a Mathlib PR, and that I didn't accidentally just do your homework :stuck_out_tongue:

[Eric Wieser]

(Note you can collapse large walls of text with ```spoiler title\n ``` blocks)

[Violeta Hernández]

(deleted)

[Eric Wieser]

Like this

````spoiler Proof
```lean
import oh_no
```
````

gives

Proof

import oh_no

[Ben Nale]

Violeta Hernández said:

This was a really nice but really hard exercise. Took about 7 hours total. Seems like we're missing a lot of API for bitwise operations. You're welcome to improve on my code:

Proof

import Mathlib.Data.Int.Bitwise

infix:30 " ^^ " => xor

namespace Bool

@[simp] lemma not_xor : ∀ x y : Bool, (!(x ^^ y)) = (x == y) := by decide
@[simp] lemma xor_not_left' : ∀ x y : Bool, (!x ^^ y) = (x == y) := by decide
@[simp] lemma xor_not_right' : ∀ x y : Bool, (x ^^ !y) = (x == y) := by decide

@[simp] lemma xor_eq_left : ∀ x y : Bool, ((x ^^ y) == x) = !y := by decide
@[simp] lemma xor_eq_right : ∀ x y : Bool, ((x ^^ y) == y) = !x := by decide

@[simp] lemma xor_left_inj : ∀ x y z : Bool, (x ^^ y) = (x ^^ z) ↔ y = z := by decide
@[simp] lemma xor_right_inj : ∀ x y z : Bool, (x ^^ z) = (y ^^ z) ↔ x = y := by decide

/-- Whether x + y + z produces a carry. Is true iff at least two of x, y, z are. -/
def carry (x y z : Bool) := x && y || (x ^^ y) && z

@[simp] lemma carry_self_self : ∀ x y, carry x x y = x := by decide

@[simp] lemma carry_false₁ : ∀ y z, carry false y z = (y && z) := by decide
@[simp] lemma carry_false₂ : ∀ x z, carry x false z = (x && z) := by decide
@[simp] lemma carry_false₃ : ∀ x y, carry x y false = (x && y) := by decide

@[simp] lemma carry_true₁ : ∀ y z, carry true y z = (y || z) := by decide
@[simp] lemma carry_true₂ : ∀ x z, carry x true z = (x || z) := by decide
@[simp] lemma carry_true₃ : ∀ x y, carry x y true = (x || y) := by decide

lemma carry_comm : ∀ x y z, carry x y z = carry y x z := by decide

end Bool

namespace Nat

variable (x y i : Nat)

lemma shiftr_one : x.shiftr 1 = div2 x := rfl

lemma shiftr_succ : x.shiftr i.succ = div2 (x.shiftr i) := rfl

lemma shiftr_succ' : x.shiftr i.succ = (div2 x).shiftr i := by
rw [←shiftr_one, ←shiftr_add, succ_eq_one_add]

@[simp] lemma shiftr_bit (b : Bool) : shiftr (bit b x) i.succ = shiftr x i := by
rw [shiftr_succ', div2_bit]

-- why are Nat.zero_shiftr and Nat.shiftr_zero the same and neither is this one?
@[simp] lemma zero_shiftr' : x.shiftr 0 = x := rfl

@[simp] lemma testBit_zero_left : testBit 0 i = false := by
simp [testBit]

@[simp] lemma testBit_zero_right : x.testBit 0 = x.bodd := by
simp [testBit]

lemma testBit_succ_right : x.testBit i.succ = (div2 x).testBit i := by
rw [testBit, succ_eq_one_add, shiftr_add]
rfl

@[simp] lemma testBit_one_succ : testBit 1 i.succ = false := by
rw [testBit_succ_right, div2_one, testBit_zero_left]

@[simp] lemma testBit_one_zero : testBit 1 0 = true := rfl

@[simp] lemma testBit_bit (b : Bool) : testBit (bit b x) i.succ = testBit x i := by
rw [testBit, shiftr_bit]
rfl

-- Should be marked simp in Mathlib.
attribute [simp] bodd_bit div2_bit bit_zero

@[simp] lemma succ_bit0 : (bit false x).succ = bit true x := rfl
@[simp] lemma succ_bit1 : (bit true x).succ = bit false x.succ := by
simp [bit, Nat.bit0_succ_eq]
rfl

lemma bit_succ (b : Bool) : bit b x.succ = (bit b x).succ.succ := match b with
| false => Nat.bit0_succ_eq x
| true => Nat.bit1_succ_eq x

lemma bit1_add' : bit true x + bit true y = bit false (x + y).succ := by
change bit false x + 1 + (bit false y + 1) = _ rw [add_add_add_comm, ←bit_add, bit_succ]

/-! ## Carry theorem -/

def carry (x y i : Nat) : Bool := match i with
| 0 => false
| i + 1 => Bool.carry (Nat.testBit x i) (Nat.testBit y i) (carry x y i)

@[simp] lemma carry_zero : carry x y 0 = false := rfl

lemma carry_succ :
carry x y i.succ = Bool.carry (Nat.testBit x i) (Nat.testBit y i) (carry x y i) :=
rfl

lemma carry_comm : carry x y i = carry y x i := by
induction' i with i IH
· rfl
· rw [carry_succ, carry_succ, Bool.carry_comm, IH]

@[simp] lemma carry_zero' : carry 0 y i = false := by
induction' i with i IH
· rfl
· simp [carry_succ, IH]

@[simp] lemma carry_zero'' : carry x 0 i = false := by
rw [carry_comm, carry_zero']

@[simp] lemma carry_bit0_left (b : Bool) : carry (bit false x) (bit b y) i.succ = carry x y i := by
induction' i with i IH
· rw [carry_succ]
simp
· rw [carry_succ]
simp [IH]
rfl

@[simp] lemma carry_bit0_right (b : Bool) : carry (bit b x) (bit false y) i.succ = carry x y i := by
rw [carry_comm, carry_bit0_left, carry_comm]

@[simp] lemma carry_bit0_one : carry (bit false x) 1 i = false := by
cases i
· rfl
· change carry _ (bit true 0) _ = _ rw [carry_bit0_left, carry_zero'']

@[simp] lemma carry_bit1_one_succ_succ :
carry (bit true x) 1 i.succ.succ = carry x 1 i.succ := by
induction' i with i IH
· simp [carry_succ]
· rw [carry_succ, carry_succ x 1 (succ i)]
simp [IH]

@[simp] lemma carry_bit1_bit0_bit1 :
carry (bit true (bit false x)) (bit true y) i.succ.succ =
carry (bit true x) y i.succ := by
induction' i with i IH
· simp [carry_succ]
· rw [carry_succ, carry_succ (bit true x)]
simp [IH]

@[simp] lemma carry_bit1_bit1_bit0 :
carry (bit true x) (bit true (bit false y)) i.succ.succ =
carry x (bit true y) i.succ := by
rw [carry_comm, carry_bit1_bit0_bit1, carry_comm]

@[simp] lemma carry_bit1_bit1_bit1_bit1 :
carry (bit true (bit true x)) (bit true (bit true y)) i.succ.succ =
carry (bit true x) (bit true y) i.succ := by
induction' i with i IH
· simp [carry_succ]
· rw [carry_succ, carry_succ (bit true x)]
simp [IH]

lemma carry_bit1_bit1 : ∀ x y,
carry (bit true x) (bit true y) i.succ.succ =
(carry x 1 i.succ ^^ carry (succ x) y i.succ) := by
induction' i with i IH
· have : ∀ a b : Bool, (a || b) = (a ^^ !a && b) := by decide
simp [carry_succ, this]
· intro x y
apply x.bitCasesOn
apply y.bitCasesOn
rintro (_ | _) x (_ | _) y
· rw [carry_succ]
simp [IH]
rfl
· simp [IH]
· simp
· simp [IH]

lemma carry_bit1_one : carry (bit true x) 1 i.succ.succ = carry x 1 i.succ := by
induction' i with i IH
· simp [carry_succ]
· rw [carry_succ, carry_succ x]
simp [IH]

lemma testBit_succ_one : x.succ.testBit 1 = (x.testBit 1 ^^ bodd x) := by
induction' x with x IH
· rfl
· apply x.bitCasesOn
rintro (_ | _) x
all_goals simp [IH, testBit, shiftr_one, div2_succ]

lemma testBit_succ_succ : ∀ x, x.succ.testBit i.succ = (x.testBit i.succ ^^ carry x 1 i.succ) := by
induction' i with i IH
· simp [carry_succ]
exact testBit_succ_one
· intro x
apply x.bitCasesOn
rintro (_ | _) x
· simp [testBit_succ_right _ i.succ, carry_bit0_one]
· simp [testBit_succ_right _ i.succ, IH, carry_bit1_one]

theorem testBit_add :
∀ x y, (x + y).testBit i = ((x.testBit i ^^ y.testBit i) ^^ carry x y i) := by
induction' i with i IH
· simp
· intro x y
apply x.bitCasesOn
apply y.bitCasesOn
rintro (_ | _) x (_ | _) y
· simp [←bit_add, IH]
· simp [←bit_add', IH]
· simp [←bit_add, IH]
· rw [bit1_add', ←add_succ]
simp [IH]
cases' i with i
· simp [carry_succ]
· rw [carry_comm (bit true y), carry_bit1_bit1, testBit_succ_succ]
simp [carry_comm]

end Nat

omg, thank you so much. This is actually incredible. I appreciate it!!!