Zulip Chat Archive

Stream: general

Topic: scavenging flypitch for lemmas

Yury G. Kudryashov (Oct 22 2021 at 16:13):

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

Yury G. Kudryashov (Oct 22 2021 at 16:13):

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

Yakov Pechersky (Oct 22 2021 at 16:14):

I have a fork with a branch that has at least fol.lean and its prereqs working on a very recent mathlib:

Yury G. Kudryashov (Oct 22 2021 at 16:17):

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 (Oct 22 2021 at 16:24):

@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 (Oct 22 2021 at 16:26):

being able to pattern match on dvectors is really nice

Mario Carneiro (Oct 22 2021 at 16:26):

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

Floris van Doorn (Oct 22 2021 at 16:42):

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 (Oct 22 2021 at 20:26):

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

Yury G. Kudryashov (Oct 22 2021 at 20:26):

Which one should I fix?

Yury G. Kudryashov (Oct 22 2021 at 20:27):

Current definition inserts x into the sequence at position n.

Yury G. Kudryashov (Oct 22 2021 at 20:31):

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

Yury G. Kudryashov (Oct 22 2021 at 20:57):

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 (Oct 23 2021 at 05:42):

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

Mario Carneiro (Oct 23 2021 at 05:43):

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

Yury G. Kudryashov (Oct 26 2021 at 20:16):

@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 (Oct 28 2021 at 21:30):

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

Yury G. Kudryashov (Nov 15 2021 at 03:14):

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 (Nov 15 2021 at 17:45):

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)

Last updated: Aug 03 2023 at 10:10 UTC