referring to instance fields

Stream: new members

[Alex Meiburg]

I'm trying to write something like

instance inst_name : foo bar :=
{
  mul := begin ..... end,
  mul_comm := begin ..... end,
}

And I need to repeatedly apply the definition of multiplication (mul) in the proof of mul_comm, of course. The first time, a call to simp does it -- although of course that's not great because it's non-terminal. Subsequent calls aren't doing rewriting even though I need it. How do I manually get it to expand the definition of *?

[Alex Meiburg]

I'm expecting there's some name like (foo bar).mul that I can use with ... rw? With dsimp? I'm not sure

[Alex Meiburg]

The application of * is under a binder, so it might be that I have to go into conv mode or something

[Alex Meiburg]

But I thought simp searched throughout the tree for places to do rewrites

[Alex J. Best]

does simp only [(*)] help in your situation?

[Alex Meiburg]

sadly no :c that just gives "simplify tactic failed to simplify"

[Alex Meiburg]

The goal has the form dite (a * b = a) (xxx a b) (yyy a b) = b. Is there a particular reason it wouldn't be rewriting it inside the dite?

[Alex Meiburg]

Seems like dite h t e := λ t e, decidable.rec_on h e t, so I'm guessing this is some issue with simp not going inside the λ?

[Alex Meiburg]

Huh, a second and separate dsimp seems to do it ... I didn't know that dsimp would simplify anything that simp wouldn't. That's surprising.

[Scott Morrison]

I think there is a library note about this.

[Scott Morrison]

See the bottom of src#category_theory.category.default for some explanation of why dsimp, simp is often needed.

[Scott Morrison]

Although maybe that explanation is too specific to category theory to be helpful here.

[Alex Meiburg]

I'm not sure what you mean to link, but that's a broken link

[Scott Morrison]

Sorry:

[Scott Morrison]

https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/category/basic.lean#L254

[Alex Meiburg]

Hmm, okay, that makes some sense...

[Alex Meiburg]

I think I figured out why [(*)] was also causing weird problems for me. The instance of foo that I'm deriving from bar is, specifically, creating a Steiner Triple System on units K, where K is an field of characteristic 2. The (multiplicatively denoted) structure of the STS is built from the additive structure of the units.

K has its own multiplicative structure, though, which means that when I write a * b it is using the field's multiplication, even though my goal has statements like a * b = a where * is in the STS language.

Which brings it back to, how do I specify that I want to use the STS's instance of has_mul, and its *, and not the field's?

[Scott Morrison]

Can you post a #mwe? Usually it is a bad idea to have two instances of has_mul on the same type; you will inevitably go insane trying to keep them straight.

[Scott Morrison]

Usually better is to define a type synonym with the "new" instance, and explicit functions (which are just the identity, but type signatures old_type <-> new_type) for translating when needed.

[Scott Morrison]

e.g. you might want to do something like def steiner (K) := units K, which won't have a multiplicative structure.

[Alex Meiburg]

Okay, good point, that makes more sense than an instance. It's not really that every set of units in a field of char 2 _is_ a steiner triple system, it's that it _can_ be given that structure in a canonical way. :)

[Alex Meiburg]

So, I'll re-work it to be that.

[Alex Meiburg]

Still curious though: if I wanted to differentiate between the two, and do it in that awful way, how would I? Just trying to learn the syntax a bit better.