feat: prove that omega-regularity is closed under union and is universe-polymorphic#168
Conversation
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
Mostly small comments. Are there other examples in Mathlib of this pattern of using existentials with types and typeclasses? It might be fine, I've just never seen this before.
| grind [reindex_run_iff] | ||
| · rintro ⟨ss, h_run, h_acc⟩ | ||
| use ss.map f | ||
| constructor <;> grind [reindex_run_iff'] |
There was a problem hiding this comment.
Needing to explicitly split this conjunction a single time to make grind work seems like an indicator that the annotations need some refinement.
I think the problem is that the = annotation on NA.Run eagerly splits it into the underlying conjunction, so then further API around NA.Run is not useful. I'm not sure, but could you try removing that annotation and seeing if that's an improvement?
A theorem (does this exist already?)
theorem foo (na : NA State Symbol) (xs : ωSequence Symbol) (ss : ωSequence State)
(h₁ : ss 0 ∈ na.start) (h₂ : ∀ n, na.Tr (ss n) (xs n) (ss (n + 1))) : Run na xs ss := ⟨h₁, h₂⟩with maybe annotation [grind =>] or [grind <=] could be helpful.
There was a problem hiding this comment.
Could you take a look at the commit I just pushed? (Not meant to be the final word, just experimenting). Regardless of grind, I think that if you are defining a type Run, it is good to have API theorems that construct and deconstruct it.
Adding grind annotations to these happens to help a little bit as a replacement for the annotation on NA.Run, but is still not perfect. The tradeoff is there are a few places where you need to know to specify grind [NA.Run], and I don't understand yet why this is the case.
There was a problem hiding this comment.
I reorganized the code a little bit: renaming Run.trace to Run.trans and putting the grind lemmas in a section with a comment. We should get more data as I develop the theory of NA.Buchi more.
There was a problem hiding this comment.
I also did some comparisons of the old and the new grind annotations. It seems that the new annotations sped up Sum.lean by quite a bit, although both runs are on the new version of Sum.lean.
There was a problem hiding this comment.
Hmm interesting. Soon we should have some benchmarking in place that makes these performance aspects easier to identify.
|
Merge in the new upstream/main and fix an import error caused by it. |
|
@chenson2018 About your question about NABuchiEquiv above: I basically copied the code, mutatis mutandis, from: |
chenson2018
left a comment
chenson2018
left a comment
There was a problem hiding this comment.
LGTM, we can iterate on the grind annotations as we have more usage to see what works and doesn't.
|
Very nice!! |
…se-polymorphic (leanprover#168) This patch proves that: (1) omega-regular languages are closed under finite union, and (2) the definition of omega-regular languages is universe-polymorphic. The `iSum` construction used to prove (1) actually works over an arbitrary indexed family of NA.Buchi automata. --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
…se-polymorphic (leanprover#168) This patch proves that: (1) omega-regular languages are closed under finite union, and (2) the definition of omega-regular languages is universe-polymorphic. The `iSum` construction used to prove (1) actually works over an arbitrary indexed family of NA.Buchi automata. --------- Co-authored-by: Chris Henson <chrishenson.net@gmail.com>
3 participants
This patch proves that:
(1) omega-regular languages are closed under finite union, and
(2) the definition of omega-regular languages is universe-polymorphic.
The
iSumconstruction used to prove (1) actually works over an arbitrary indexed family of NA.Buchi automata.