Flypitch integration

Stream: mathlib4

[Uni Marx]

Are there any plans to eventually integrate the set-theoretical parts of flypitch into mathlib? Otherwise, I'd work on showing that the cumulative hierarchy from file#Mathlib/SetTheory/ZFC/Basic satisfies the actual first-order axioms and maybe slowly continue towards some kind of reflection principle, since the prerequisites for that seem to be comparatively little

[Yury G. Kudryashov]

AFAIR, some parts were added to mathlib with a different API. This makes moving the rest of the code harder. Though it would be nice if someone does it.

[Yury G. Kudryashov]

But I'm not an expert in this part of the library.

[Yury G. Kudryashov]

@Floris van Doorn :up:

[Yury G. Kudryashov]

Also, flypitch uses docs3#dvector a lot. AFAIK, there are no DVectors in Lean 4 (yet).

[Mario Carneiro]

I think that's a flypitch definition, the link is broken

[Yury G. Kudryashov]

You're right. Sorry.

[Mario Carneiro]

I think that flypitch should definitely be mathported, it has been supplying a steady trickle of PRs to mathlib and I think it should continue to do so since our model theory is still lacking compared to what flypitch has

[Yury G. Kudryashov]

I tried to update it to the latest mathlib3. Even to_mathlib fails to compile.

[Yury G. Kudryashov]

I partially fixed it but probably I won't have time to go through the whole file.

[Uni Marx]

yeah, the fact that the API is already substantially different (mathlib is using Fin i -> Term instead of dependent vectors, for example) does make it pretty difficult too

[Yury G. Kudryashov]

And I see that many lemmas in to_mathlib use very old API.

[Yury G. Kudryashov]

E.g., mk_union_countable_of_countable should be docs#Set.Countable.union

[Mario Carneiro]

The use of dvector was deliberate, mathlib was using fin n -> A already at the time and they needed dvector for the defeqs

[Uni Marx]

dvectors seem like the right call too, right now you get a lot of

h: ↑i < n + 1
⊢ Fin.snoc (Fin.snoc xs X) X i = Fin.snoc (Fin.snoc xs X) Y i

goals every time you slightly reorder variables, more or less. not impossible to deal with but definitely a hassle

[Yury G. Kudryashov]

Pushed to https://github.com/urkud/flypitch/tree/YK-update-mathlib

[Yury G. Kudryashov]

I don't know what's the right way to port this project.