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

Stream: new members

[agro1986]

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]

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]

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

[Alex J. Best]

You could change all your def blah := ... to axiom blah : ... to get the effect you want

[Kevin Buzzard]

Note the change from := to :

[agro1986]

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

[agro1986]

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]

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]

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

[agro1986]

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]

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]

Umm...

theorem one_plus_one_is_not_two: plus one one ≠ two.

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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