Zulip Chat Archive

Stream: general

Topic: rw / simp difference

view this post on Zulip Sebastien Gouezel (May 22 2019 at 06:38):

I just encountered a very weird behavior. I have at the end of a proof a line

simp [written_in_ext_chart_at, ext_chart_at, local_equiv.to_inv, mem_some_chart_at_source]

With this line, the proof works, but I get red squiggles under the name of the theorem, with the error message

type mismatch at application
  @written_in_ext_chart_at k _inst_1 (@tangent_space_at k _inst_1 E _inst_2 H _inst_3 I M _inst_4 _inst_5 _inst_6 x)
has type
  @manifold.smooth 1 k _inst_1 E' _inst_7 H' _inst_8 I'_1 M' _inst_9 _inst_10
but is expected to have type
  @manifold.smooth 1 k _inst_1 E' _inst_7 H' _inst_8 I' M' _inst_9 _inst_10
types contain aliased name(s): I'
remark: the tactic `dedup` can be used to rename aliases

Except that I can't see any place where I would have introduced two different variables I'. What is funny is that if I replace my simp line with the two lines

rw written_in_ext_chart_at,
simp [written_in_ext_chart_at, ext_chart_at, local_equiv.to_inv, mem_some_chart_at_source]

then the error goes away. Highly non-minimal example at https://github.com/sgouezel/mathlib/blob/b87ee06fe4385c12fa2e53b867913b62feb609fb/src/geometry/manifolds/mderiv.lean#L599

I am afraid it indicates there is something fishy in the way I define stuff (or, at the very least, something that Lean doesn't like very much). The motivation for the definitions as they are is at https://github.com/sgouezel/mathlib/blob/b87ee06fe4385c12fa2e53b867913b62feb609fb/src/geometry/manifolds/mderiv.lean#L154 (and I can explain here on Zulip if needed).

Last updated: May 15 2021 at 23:13 UTC