scavenging flypitch for lemmas

Stream: general

[Yury G. Kudryashov]

I've opened to_mathlib file in flypitch and borrowed a few lemmas from there, see #9883, #9885, #9886, #9887.

[Yury G. Kudryashov]

Do we have any plans about porting flypitch to current mathlib / integrating it into mathlib?

[Yakov Pechersky]

I have a fork with a branch that has at least fol.lean and its prereqs working on a very recent mathlib:
https://github.com/pechersky/flypitch/tree/3.33.0

[Yury G. Kudryashov]

cloc says that it's less than 20K lines of code, so it should be possible to merge it into mathlib in a month or two.

[Yury G. Kudryashov]

@Floris van Doorn Are dvectors better than vectors in some sense? I mean, why add a type instead of adding an induction principle on an existing type?

[Mario Carneiro]

being able to pattern match on dvectors is really nice

[Mario Carneiro]

Probably it can be replaced with fin n -> A vectors though

[Floris van Doorn]

As Mario said, they were originally defined to be able to pattern match and have nice definitional equalities. If you can get the definitions in fol.lean to work equally nicely without dvector then that would be preferred.

[Yury G. Kudryashov]

It seems that the docstring of subst_realize in fol.lean describes something else.

[Yury G. Kudryashov]

Which one should I fix?

[Yury G. Kudryashov]

Current definition inserts x into the sequence at position n.

[Yury G. Kudryashov]

BTW, many lemmas about subst_realize etc look like good lemmas about docs#stream.

[Yury G. Kudryashov]

What would be a good (localized) notation for stream.insert_nth? Flypitch uses v[x//n] for the corresponding function on nat → S but this comes from a domain-specific meaning.

[Mario Carneiro]

I don't think stream.insert_nth needs a notation at all, any more than list.insert_nth does

[Mario Carneiro]

I think it's fine for the notation to be local to flypitch

[Yury G. Kudryashov]

@Floris van Doorn Could you please add a bit more docs to fol.lean in the original repo? E.g., a module docstring explaining the meaning of different definitions and how they are related would help me a lot with moving it to mathlib.

[Floris van Doorn]

Yes, I'll do that, but it will take 1-2 weeks.

[Yury G. Kudryashov]

I scavenged some more defs/lemmas into #10327 but I'm not the right person to write docstrings in this file. Also, I don't know who's the original author of this code.

[Floris van Doorn]

I added a bunch of documentation here: https://github.com/flypitch/flypitch/blob/3.33.0/src/fol.lean (based on top of @Yakov Pechersky's 3.33.0 branch)