# Zulip Chat Archive

## Stream: new members

### Topic: proving 1 + 1 = 2. Why does my rewrite fail here?

#### agro1986 (Dec 22 2019 at 15:44):

Hi all. I wanted to build my own natural number-like number system and prove that 1 + 1 = 2. Why does my rw fail here?

constant mynumber: Type constant zero: mynumber constant one: mynumber constant two: mynumber constant after: mynumber → mynumber constant plus: mynumber → mynumber → mynumber def one_is_after_zero := one = after(zero) def two_is_after_one := two = after(one) def plus_zero (n: mynumber) := plus n zero = n def plus_after (n m: mynumber) := plus n (after m) = after (plus n m) theorem one_plus_one_is_two: plus one one = two := begin rw one_is_after_zero, -- FAILED HERE end

The popup in vs code just say "failed" without any explanation. Thanks.

#### Kevin Buzzard (Dec 22 2019 at 15:55):

You never need to use constants in Lean. But the reason for the failure is that `one_is_after_zero`

is the *statement* that `one = after(zero)`

-- it has type `Prop`

. The `rw`

tactic eats *proofs* -- you need to `rw h`

where `h`

has type `one_is_after_zero`

.

#### Kevin Buzzard (Dec 22 2019 at 15:56):

constant h : one = after(zero) theorem one_plus_one_is_two: plus one one = two := begin rw h, sorry end

#### Alex J. Best (Dec 22 2019 at 15:59):

You could change all your `def blah := ...`

to `axiom blah : ...`

to get the effect you want

#### Kevin Buzzard (Dec 22 2019 at 15:59):

Note the change from `:=`

to `:`

#### agro1986 (Dec 22 2019 at 16:00):

that makes sense. proposition != the proof that the proposition is true

#### agro1986 (Dec 22 2019 at 16:00):

constant one_is_after_zero: one = after(zero) constant two_is_after_one: two = after(one) constant plus_zero (n: mynumber): plus n zero = n constant plus_after (n m: mynumber) : plus n (after m) = after (plus n m) theorem one_plus_one_is_two: plus one one = two := begin rw one_is_after_zero, rw plus_after, rw plus_zero, rw two_is_after_one, rw one_is_after_zero, end

#### Kevin Buzzard (Dec 22 2019 at 16:02):

The constant-free version looks like this:

inductive mynumber: Type | zero: mynumber | one: mynumber | two: mynumber | after: mynumber → mynumber | plus: mynumber → mynumber → mynumber namespace mynumber variables (one_is_after_zero : one = after(zero)) (two_is_after_one : two = after(one)) (plus_zero : ∀ n, plus n zero = n) (plus_after : ∀ n m, plus n (after m) = after (plus n m)) include one_is_after_zero two_is_after_one plus_zero plus_after theorem one_plus_one_is_two: plus one one = two := begin rw one_is_after_zero, rw plus_after, rw plus_zero, rw two_is_after_one, rw one_is_after_zero, end end mynumber

#### Kevin Buzzard (Dec 22 2019 at 16:04):

`include`

should be purple. I can't remember the reason this can't be fixed.

#### agro1986 (Dec 22 2019 at 16:07):

Wow thanks! Other than 'inductive' I've encountered them from TPiL. I hope I can write my code more closer to everyone else's style

#### Kevin Buzzard (Dec 22 2019 at 16:19):

The only advantage I can think of for the `inductive`

method over the `constant`

method is that with the `inductive`

method the principle of induction gets generated automatically by Lean. Other than that the two methods are very similar. If you write `#print prefix mynumber`

you can see all the stuff that Lean generates for you, the key one being `mynumber.rec`

. With your method you'd have to make the principle of induction yourself as another constant.

#### Mario Carneiro (Dec 22 2019 at 16:50):

Umm...

theorem one_plus_one_is_not_two: plus one one ≠ two.

#### Mario Carneiro (Dec 22 2019 at 16:51):

the inductive structure is assuming things that you don't necessarily want to assert

#### Mario Carneiro (Dec 22 2019 at 16:52):

You could just do this:

variables (mynumber: Type) (zero: mynumber) (one: mynumber) (two: mynumber) (after: mynumber → mynumber) (plus: mynumber → mynumber → mynumber) (one_is_after_zero : one = after(zero)) (two_is_after_one : two = after(one)) (plus_zero : ∀ n, plus n zero = n) (plus_after : ∀ n m, plus n (after m) = after (plus n m)) include one_is_after_zero two_is_after_one plus_zero plus_after theorem one_plus_one_is_two: plus one one = two := begin rw one_is_after_zero, rw plus_after, rw plus_zero, rw two_is_after_one, rw one_is_after_zero, end

#### Kevin Buzzard (Dec 22 2019 at 17:17):

That's really annoying. There's no way you can put the relations in the definition of an inductive type?

#### Mario Carneiro (Dec 22 2019 at 18:39):

They call those HITs (higher inductive types), and the theory is much more subtle

Last updated: Dec 20 2023 at 11:08 UTC