Grind and unfolding

Stream: computer science

[Fabrizio Montesi]

I'm playing around with using grind for bisimulation/bisimilarity results, and it's going pretty well. I've encountered a weird problem with unfolding definitions though. @Chris Henson perhaps it's similar to your problem with forward reasoning? I feel like this should be pretty simple though...

Check out the unfolding I'm doing here: https://github.com/leanprover/cslib/blob/01dd639de4b55c944958d27ff2b6bebf89226ee9/Cslib/Languages/CCS/BehaviouralTheory.lean#L162

Basically, I have to manually unfold a structure (Lts) for grind to be able to proceed. I've tried using grind ext on Lts, the etaStruct config, and even making an explicit theorem like this:

@[grind =]
theorem foo :
  (@lts Name Constant defs : Lts (Process Name Constant) (Act Name)).Tr =
    @CCS.Tr Name Constant defs := by
  rfl

But nothing seems to work. What I want is to get rid of those unfold instructions. Ideally, we'd golf the entire proof to a single grind use.

[Chris Henson]

It may be related, though I am not sure about ext. I think the problem is the automatic selection of defs.

[Fabrizio Montesi]

@Kim Morrison maybe you have some insight?

[Kim Morrison]

I had a brief look, but I'm not sure.

It's suspicious, I guess, that the step we're having difficulty with is unfold lts, where lts is an abbrev (mildly further suspicious that it is generated by meta code in elab "create_lts", but that's probably okay).

[Kim Morrison]

How important is this lts function? If you replace the theorem statement with

theorem bisimilarity_choice_idem :
  (choice p p) ~[{ Tr := Tr (defs := defs) }] p := by

then everything goes through. (arguably this is more readable: I really don't like this "all implicit arguments" lts...)

But I agree it should still work!

[Kim Morrison]

(As general advice, I would suggest never set up any notation until after you have things working, but I accept that I am an extremist about notation. :-)

[Kim Morrison]

Hmm... I tried making it not an abbrev, or making the defs argument explicit, to no avail.

[Sebastian Ullrich]

Could it be this definition is missing equational theorems etc. usually generated by the def elaborator and relied on by grind?

[Fabrizio Montesi]

I'm starting to suspect that too after Kim's reply.

[Fabrizio Montesi]

But I hadn't thought of deffing that explicitly, let's see..

[Fabrizio Montesi]

Making it an explicit reducible def works!

@[reducible]
def lts : Lts (Process Name Constant) (Act Name) := ⟨@Tr Name Constant defs⟩

[Chris Henson]

To make sure I understand, this is because of the way it was defined using addAndCompile?

[Fabrizio Montesi]

Kim Morrison said:

How important is this lts function? If you replace the theorem statement with

theorem bisimilarity_choice_idem :
  (choice p p) ~[{ Tr := Tr (defs := defs) }] p := by

then everything goes through. (arguably this is more readable: I really don't like this "all implicit arguments" lts...)

But I agree it should still work!

Pretty important, we use the Lts type that it returns for various convenient dot notations and other notations.

But I can do this:

theorem bisimilarity_choice_idem :
  (choice p p) ~[lts (defs := defs)] p

which reads much, much better, thanks. :-)

[Fabrizio Montesi]

Kim Morrison said:

(As general advice, I would suggest never set up any notation until after you have things working, but I accept that I am an extremist about notation. :-)

This code predates grind, so we were unaware. We have a design puzzle with multiple moving parts (transition and program equivalence notation, dot-notation, supporting automation/grind, ...), and the theorems in that file are a good test to figure things out. Otherwise, in general I agree.

[Kim Morrison]

I made a PR cslib#54 with some minor grind-golfing. Once you fix the lts equational lemmas issue much more will be possible!

[Fabrizio Montesi]

(deleted)

[Fabrizio Montesi]

Kim Morrison said:

I made a PR cslib#54 with some minor grind-golfing. Once you fix the lts equational lemmas issue much more will be possible!

The docs say that grind cases is always scoped, correct? What about your line:

attribute [grind] ParNil.parNil

Should I be concerned about polluting the search space for grind in any way?

[Fabrizio Montesi]

@Kim Morrison @Chris Henson: I've created a grind-ccs branch to play with these issues.
Therein, I have manually defined lts so that we can exclude problems introduced by our elaborators (but we should fix that once we know what we wanna do, ofc).

Please have a look at my two 'grind hacks' given in https://github.com/leanprover/cslib/blob/c74dd26bd7cea93c96d96ab542aa18bdfac6ac21/Cslib/Languages/CCS/BehaviouralTheory.lean#L38. Specifically, I have to (a) require that the definition of lts is reducible (otherwise, we need manual unfoldings) and (b) introduce some equations manually to get through instances like Zero if people don't use those uniformly.

Re (a): I'm unsure whether requiring reducibility is intended with grind. Is it? It's weird to me, at least, since grind seems to get the right equalities out, but somehow doesn't use them when needed.

Re (b): An easy solution here is probably to tell people to use the notations given by classes uniformly all over the place, instead of just some places. ;-) That sounds ok?

[Chris Henson]

I have created the issue cslib#55 for the elab issues, I'll take a look soon.

I'm reminded that despite being the author of that meta code, I still don't quite understood the usefulness of Lts (and ReductionSystem). I've had the thought that it would be nicer if the notations directly were the relation and closure versus this bundling. Do you think you could comment on the issue with an explanation @Fabrizio Montesi?

Re (b) I do like the paramaterized notations and they should be the encouraged interface. However even if you only use the notation, and despite the notation3-generated delaborators, you can still occasionally be exposed to the underlying Lts or ReductionSystem. In some places I have grind annotations like this that are helpful, with a TODO comment that I should generate these along with Lts and ReductionSystem.

[Fabrizio Montesi]

There are two motivations behind them. One, which we can forget about, is historical: I was in doubt as to whether we should bundle more stuff (like the types of states and actions), but that turned out not to be necessary. The other reason is that I wanted good support for automatically deriving the MTr and STr relations for any Lts and offering them to users, and the dot-notation achieves that. I'm unsure how to do without a structure, but if there's a better way I'm all for it. :-)

[Fabrizio Montesi]

@Chris Henson Btw, this reveals that sometimes it's convenient to control attributes on the lts/rs definition. Maybe we should allow for it being defined separately and still benefit from the notation?..

[Fabrizio Montesi]

Chris Henson said:

Re (b) I do like the paramaterized notations and they should be the encouraged interface. However even if you only use the notation, and despite the notation3-generated delaborators, you can still occasionally be exposed to the underlying Lts or ReductionSystem. In some places I have grind annotations like this that are helpful, with a TODO comment that I should generate these along with Lts and ReductionSystem.

Not sure I get what you mean, as I was talking about the notation generated by Zero and similar. (See the link to my 'hacks'.)

[Chris Henson]

Fabrizio Montesi said:

Chris Henson Btw, this reveals that sometimes it's convenient to control attributes on the lts/rs definition. Maybe we should allow for it being defined separately and still benefit from the notation?..

You mean being able to add attributes to the derived definition? We could probably pass those along in the attribute if you wanted.

Note however, you can already use the command that adds these notations on existing definitions. See reduction_notation and lts_transition_notation.

[Chris Henson]

Fabrizio Montesi said:

Not sure I get what you mean, as I was talking about the notation generated by Zero and similar. (See the link to my 'hacks'.)

I think we are describing the same problem form different perspectives. The issue is when grind cannot see through a notation. So when instantiating a notation typeclass, it can be helpful to follow up with a grind _=_ lemma to treat them interchangeably.

[Chris Henson]

Not sure if that's considered a "hack", but I don't know of another way to do this. As an example, in working with contexts, I have found it helpful to add grind annotations to existing lemmas like docs#List.append_eq and docs#Option.mem_def