Zulip Chat Archive

I've fixed a good chunk of the file, but the coercions are still causing trouble and simp is unable to find proofs, so I am suspecting that there are more fundamental issues. Maybe someone that has experience with porting an Equiv file wants to look at this.

Moritz Doll (Mar 13 2023 at 09:21):

I've fixed almost everything now, there is one issue left with initialize_simps_projections (it wants some arguments to be implicit, while the theorem takes them explicitly) which I don't know how to fix.

Floris van Doorn (Mar 13 2023 at 11:33):

The implicitness of arguments doesn't matter. The argument order of implicit arguments does.

Note: make sure order of implicit arguments is exactly the same.

Moritz Doll (Mar 13 2023 at 11:54):

ah thanks, I misread that. The issue was that I swapped a ring instance and the other type definitions, because of 2074.

Eric Wieser (Mar 13 2023 at 11:58):

Why did you reorder the arguments?

Moritz Doll (Mar 13 2023 at 12:06):

I was being lazy and only moved the ring out of the definition, I reverted to the original order now.

Eric Wieser (Mar 13 2023 at 12:08):

Why did you need to move anything out of the definition?

Moritz Doll (Mar 13 2023 at 12:09):

Is there actually a preferred way? I think I've seen both {a : Type _} [inst a] {b : Type _} [inst b] [inst a b] and {a b : Type _} [inst a] [inst b] [inst a b].

Moritz Doll (Mar 13 2023 at 12:09):

Can I remove the attribute in the def?

Eric Wieser (Mar 13 2023 at 12:09):

The attribute is nothing to do with the variables (edit: unless I'm missing something)

Eric Wieser (Mar 13 2023 at 12:09):

Just remove the instance attribute before the def

Eric Wieser (Mar 13 2023 at 13:08):

I think it's perhaps worth adding a fun_like instead before finishing this file; the coercions would be much less of a mess (edit: #18575)

Eric Wieser (Mar 15 2023 at 11:46):

@Moritz Doll, I think it might be best to re-port everything depending on !4#2692 from scratch. You've presumably added a lot of workarounds to deal with coercion problems that no longer exist, and it might be easier to avoid keeping them around by accident by just throwing the whole lot out and starting over.