mul_one

Stream: new members

[YJ]

Hello, is there a way to define mul_one or one_mul without a lemma?

theorem mul_one : a * 1 = a :=

[Kevin Buzzard]

Can you post a #mwe? The answer depends on the types of your terms

[Kevin Buzzard]

Of course you can just copy the proof of mul_one, that way you don't use it. I don't really understand your question

[YJ]

Kevin Buzzard said:

Of course you can just copy the proof of mul_one, that way you don't use it. I don't really understand your question

type N , I would like to see how to define mul_one without using a lemma

[Scott Morrison]

Have you played the natural numbers games?

[YJ]

Scott Morrison said:

Have you played the natural numbers games?

just starting it

[Scott Morrison]

Not sure if the main one is actually working at the moment. There is a mirror at https://cbirkbeck.github.io/natural_number_game/?world=2&level=1

[Eric Wieser]

If your question is "how is it proved from first principles", then the following shows you how mathlib proves it:

src#nat.mul_one

Note that this is probably a spoiler for the NNG, although likely not a very helpful one.

[YJ]

Scott Morrison said:

Not sure if the main one is actually working at the moment. There is a mirror at https://cbirkbeck.github.io/natural_number_game/?world=2&level=1

Thank you so much this is really helpful

[YJ]

Eric Wieser said:

If your question is "how is it proved from first principles", then the following shows you how mathlib proves it:

src#nat.mul_one

thank you regardless, I will have a look!
Note that this is probably a spoiler for the NNG, although likely not a very helpful one.

[Kevin Buzzard]

That's actually one of my favourite proofs in mathlib. Abusing a<b = a+1<=b is one thing but this is something else.

[YJ]

How do I introduce this axiom in lean if I want to use it to rewrite the below theorem lemma mul_one?

one_eq_succ_zero : 1 = succ(0)

as an axiom for

lemma mul_one (m : mynat) : m * 1 = m :=

[Eric Wieser]

lemma one_eq_succ_zero : 1 = succ 0 := rfl  -- it's true by definition

[Eric Wieser]

src#nat.has_one oh nevermind, you're doing NNG with mynat not nat

[Eric Wieser]

By "introduce" do you mean "define" or "use"?

[YJ]

define and use

[YJ]

I tried defining it as it is earlier as it's true by definiton as you said but it seems that when i try to rewrite the mul_one using it, it doesn't work as it should

[Eric Wieser]

Is this in the NNG, or in your own file locally?

[Eric Wieser]

I don't think NNG lets you define your own lemmas, because it's not trying to teach that

[YJ]

its on the lean prover web editor

[Eric Wieser]

Can you give a #mwe?

[Eric Wieser]

Including the definition of mynat

[YJ]

I'm using nat,
Yeah In the NNG, one_eq_succ_zero : 1 = succ(0) is just introduced to be used for a theorem, but I would like to learn more about how it can be used to define mul_one

[Kevin Buzzard]

The definition of 1 is succ(0).