## Stream: new members

#### Ben Nale (Apr 03 2023 at 18:49):

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)


#### Ben Nale (Apr 03 2023 at 18:59):

fixed :). This is using Lean 4

#### Violeta Hernández (Apr 04 2023 at 15:04):

I believe the usual math problem solving techniques apply here

#### Violeta Hernández (Apr 04 2023 at 15:04):

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

#### Violeta Hernández (Apr 04 2023 at 21:53):

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

#### Violeta Hernández (Apr 04 2023 at 21:54):

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

#### Violeta Hernández (Apr 04 2023 at 22:03):

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 (Apr 04 2023 at 22:04):

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 (Apr 04 2023 at 22:34):

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

(deleted)

Like this

#### Ben Nale (Apr 05 2023 at 00:35):

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

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

Last updated: Dec 20 2023 at 11:08 UTC