Contributing to Core.

Stream: lean4

[Wrenna Robson]

Hi. I have some I think genuinely useful lemmas that really seem to fit into Init.Data.Array.Lemmas and similar places. Is it possibly to contribute such lemmas? I know that the process is different to that of Mathlib but I don't really understand what that difference is.

[Johannes Tantow]

Fork the core repo. In your fork you add the lemmas you need (best into a separate branch). Then you open a pull request from your fork to the main repo.
You will need a label once your PR is ready to review, which you can set writing a comment with the desired label, which should be changelog-library in your case.
There is a style guide here: https://github.com/leanprover/lean4/tree/master/doc/std , but this should be similar to mathlib

[Wrenna Robson]

Thanks.

An example of what I was intending to contribute:

theorem getElem_swapIfInBounds {as : Array α} {i j k : ℕ} (hk : k < (as.swapIfInBounds i j).size) :
    (as.swapIfInBounds i j)[k] =
    if h : k = i ∧ j < as.size then as[j]'h.2 else if h₂ : k = j ∧ i < as.size then as[i]'h₂.2
    else as[k]'(hk.trans_eq as.size_swapIfInBounds) := <proof_goes_here>

Would this be suitable? We seem to have most other getElem lemmas like this.

[Marc Huisinga]

For the standard library in particular, see https://github.com/leanprover/lean4/blob/master/doc/std/vision.md

[Wrenna Robson]

Yes, I was just reading that - it said to discuss possible contributions here first (I think?)

[Eric Wieser]

That looks like a pretty awkward lemma statement to me

[Wrenna Robson]

By analogy with

theorem getElem_swap {xs : Array α} {i j : Nat} (hi hj) {k : Nat} (hk : k < (xs.swap i j hi hj).size) :
    (xs.swap i j hi hj)[k] = if k = i then xs[j] else if k = j then xs[i] else xs[k]'(by simp_all) :=

[Wrenna Robson]

Which this seems similar to? I am not seeing the awkwardness.

[Wrenna Robson]

Well, except in so far as swapIfInBounds is an awkward function.

[Eric Wieser]

I'd suggest splitting it into multiple lemmas, one for each branch of the if

[Eric Wieser]

Which swap also does. But I guess the existence of docs#Array.getElem_swap is sufficient to justify your lemma in addition to those pieces.

[Wrenna Robson]

Yes, I wouldn't have the full fat lemma without that already existing. Sometimes it is useful to just hit the getElem on the head with no preconditions.

[Wrenna Robson]

(I was also going to add the other lemmas.)

[Wrenna Robson]

Hmm - elan is failing in these files (I assume because they are part of the bootstrapping process?). Getting errors like: error: no such release: lean4-stage0.

[Wrenna Robson]

do I have to make lean locally?

[Wrenna Robson]

https://github.com/leanprover/lean4/blob/master/doc/dev/index.md#dev-setup-using-elan

Ah it looks like this is what I need to do?

[Eric Wieser]

I think there's also a gitpod setup that kicks off most of the build for you

[Eric Wieser]

(but takes about half an hour before you can start writing Lean code)

[Wrenna Robson]

Johannes Tantow said:

Fork the core repo. In your fork you add the lemmas you need (best into a separate branch). Then you open a pull request from your fork to the main repo.
You will need a label once your PR is ready to review, which you can set writing a comment with the desired label, which should be changelog-library in your case.
There is a style guide here: https://github.com/leanprover/lean4/tree/master/doc/std , but this should be similar to mathlib

How is this, from a "correct form" point of view? lean4#8406