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