simp and dedup

Stream: general

[Sebastien Gouezel]

I have been bitten several times lately by a weird simp behavior (bug?). Each time I have avoided it by using rw instead, but it keeps showing up, so I would be glad if someone can help me understand what is going on. I tried to build a minimal working example as follows:

import analysis.normed_space.basic

def foo_rec (n : ℕ) (k : Type) [normed_field k]
  {E : Type} [normed_space k E] (f : E → E) : Prop :=
nat.rec_on n (true) (λn rec, true)

lemma stupid {k : Type} [normed_field k] {E : Type} [normed_space k E] {f : E → E} {n : ℕ} :
  foo_rec n k f ↔ foo_rec n k f :=
begin
  induction n with n IH,
  { simp },
  { simp }
end

Everything here is stupid, but hopefully my real use case is not. The proof of stupid is not accepted: more precisely, I get red squiggles under the name of the lemma, with the message

type mismatch at application
  @foo_rec n k _inst_1
term
  _inst_1
has type
  normed_field k_1
but is expected to have type
  normed_field k
types contain aliased name(s): k
remark: the tactic `dedup` can be used to rename aliases

This looks to me like a simp or induction bug. Any opinion on this?

[Rob Lewis]

It looks like simp might be building a buggy congr proof. Here's a slightly more condensed example. It succeeds if you change the order of n and k in foo_rec.

def foo_rec (n : ℕ) (k : Type) [group k]  : Prop :=
nat.rec_on n (true) (λn rec, true)

lemma stupid (k : Type) [group k] (n : ℕ) :
  foo_rec n k ↔ foo_rec n k :=
begin
  induction n with n IH,
  simp only [nat.nat_zero_eq_zero],
  admit,
  tactic.result >>= tactic.trace,
end

[Sebastien Gouezel]

It looks like simp might be building a buggy congr proof. Here's a slightly more condensed example. It succeeds if you change the order of n and k in foo_rec.

Thanks for this remark on the order of n and k. In my use case, the order does not really matter, so I put kbefore n and now everything works fine. The bug is still here, though, and mysterious, but at least it won't be a problem for me.

[Bhavik Mehta]

Does anyone have any ideas on this?

[Jalex Stark]

Bhavik Mehta said:

Does anyone have any ideas on this?

What is this pointing to? (hopefully I'm not crazy, it looks like this is the first message in a new topic?)

[Johan Commelin]

There are 3 earlier posts from half a year ago

[Jalex Stark]

Ah, i joined the server between now and then, and the part of the history that says "you subscribed to stream general" breaks this up visually in the same way that different topics are broken up if I look at the stream-wide feed

[Bryan Gin-ge Chen]

Is there a leanprover-community/lean issue about this? (If not, someone who's familiar with the issue should create one.)

[Bhavik Mehta]

None that I'm aware of, but I don't understand enough what's happening to make a coherent issue

[Gabriel Ebner]

I think it would be enough to submit an issue including a #mwe, mainly so that we don't forget about this.

[Bhavik Mehta]

https://github.com/leanprover-community/lean/issues/236