Zulip Chat Archive

Stream: general

Topic: killing easy nat goal

Kevin Buzzard (Mar 20 2018 at 16:17):

Faced with ∀ n, 2 * nat.succ (n) = nat.succ (2 * n + 1) I find that simp or ring don't seem to be able to do it. Even intro n, simp [nat.succ_eq_add_one,mul_add,one_add_one_eq_two] doesn't work. I can use simp and then ring!

Kevin Buzzard (Mar 20 2018 at 16:20):

  intro n,
  suffices : 2 + 2 * n = 1 + (1 + 2 * n),
    simp [nat.succ_eq_add_one,mul_add,this],
  ring

Kevin Buzzard (Mar 20 2018 at 16:20):

meh

Patrick Massot (Mar 20 2018 at 16:52):

Isn't there a lemma saying it suffices to prove this in Z, and then ring does it?

Simon Hudon (Mar 20 2018 at 17:06):

Interesting! What would that lemma look like?

Patrick Massot (Mar 20 2018 at 17:08):

From a mathematician perspective, the lemma says the inclusion of N into Z is injective

Patrick Massot (Mar 20 2018 at 17:08):

Insert words like coercion or cast

Patrick Massot (Mar 20 2018 at 17:08):

and get the CS version

Patrick Massot (Mar 20 2018 at 17:09):

I don't have a computer with Lean where I am right now

Kevin Buzzard (Mar 20 2018 at 17:09):

Fortunately I think ring seems to work on nat, faced with ring operations like + or *

Simon Hudon (Mar 20 2018 at 17:10):

ah! So the injectivity of coe plus the distributivity over +, * and succ would do it. That is really nice

Kevin Buzzard (Mar 20 2018 at 17:10):

One issue is that ring would rather see n + 1 than nat.succ n

Kevin Buzzard (Mar 20 2018 at 17:11):

to coerce into Z you'll need nat.cast_add, nat.cast_mul, nat.cast_one

Simon Hudon (Mar 20 2018 at 17:11):

I would assume that ↑(succ n) = ↑n + 1 would be a simp rule so succ would disappear

Chris Hughes (Mar 20 2018 at 17:14):

Have you tried rfl? 2succ n := 2n + 2 := succ(2*n+1), maybe rw add_comm or mul_comm first?

Patrick Massot (Mar 20 2018 at 17:20):

There should be a tactic doing that for any equality in nat which would immediately follow from ring in int

Patrick Massot (Mar 20 2018 at 17:20):

without any preliminary rw

Patrick Massot (Mar 20 2018 at 17:20):

I'm sure Simon is already writing it

Simon Hudon (Mar 20 2018 at 17:21):

I sneezed so you wrote the above before I could get started

Kevin Buzzard (Mar 20 2018 at 17:24):

Have you tried rfl? 2succ n := 2n + 2 := succ(2*n+1), maybe rw add_comm or mul_comm first?

Aah! I tried refl before intro n and it failed, but after intro n it succeeds.

Kevin Buzzard (Mar 20 2018 at 17:24):

Thanks.

Kevin Buzzard (Mar 20 2018 at 17:25):

Chris, I'm doing the exercises here:

Kevin Buzzard (Mar 20 2018 at 17:25):

https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html

Simon Hudon (Mar 20 2018 at 17:45):

I did a bit of scripting and then tried to find what fails and I found that this works:

example (n : ℕ) : 2 * nat.succ (n) = nat.succ (2 * n + 1) :=
begin
  ring,
end

Why doesn't it work for you?

Kevin Buzzard (Mar 20 2018 at 18:51):

because I had "forall n" in front of it :-/

Simon Hudon (Mar 20 2018 at 18:52):

Maybe ring should start with intros

Last updated: Dec 20 2023 at 11:08 UTC