HumanEval155

[marcusrossel]

Any ideas for other theorems?

[TwoFX]

How about a theorem that expresses evenOddCount (10 * n + d) in terms of evenOddCount n and d % 2?

[marcusrossel]

@TwoFX Do you mean something like this?

instance : Add (Nat × Nat) where
  add | (l₁, r₁), (l₂, r₂) => (l₁ + l₂, r₁ + r₂)

instance : Sub (Nat × Nat) where
  sub | (l₁, r₁), (l₂, r₂) => (l₁ - l₂, r₁ - r₂)

theorem evenOddCount_decompose : 
    evenOddCount (10 * n + d) = evenOddCount n + evenOddCount (d % 10) := 
  sorry

[TwoFX]

@marcusrossel I guess I was thinking of

theorem evenOddCount_decompose {n : Int} {d : Nat} (hd : d < 10) :
    evenOddCount (10 * n + d) = evenOddCount n + (d % 2, 1 - d % 2) :=
  sorry

[marcusrossel]

@TwoFX this PR will again depend on another PR (to batteries), as I added some material to batteries which I use in this PR. I'm guessing it might be somewhat common to add theorems to core/std/batteries when solving tasks in this repo. Would it therefore be possible to add labels like awaiting-v4.22, awaiting-v4.23, etc to mark PRs which cannot be merged before a given version of Lean lands?

[TwoFX]

@marcusrossel

this PR will again depend on another PR (to batteries), as I added some material to batteries which I use in this PR.

As stated in the readme, this project will not have Batteries as a dependency, as the idea is to test out Lean's out-of-the-box experience. The fact that the lemmas are missing from core important to document! Not making any promises regarding the timeline, but the FRO will periodically be looking at the files in this repo to see which general lemmas people had to prove themselves and extend the standard library to cover these use cases.

So while I think it's good that you have made the Batteries PR, I would suggest you just copy the lemmas you need into your file with a comment explaining that they are part of Batteries. I will clarify the readme to explain this.

Would it therefore be possible to add labels like awaiting-v4.22, awaiting-v4.23, etc to mark PRs which cannot be merged before a given version of Lean lands?

This a good idea! Will do.

[marcusrossel]

I would suggest you just copy the lemmas you need into your file with a comment explaining that they are part of Batteries.

Unfortunately this comes with the caveat that either the given theorems need to be sorry-ed, which doesn't feel nice, or their proofs may have to be partially reworked, which feels a bit redundant. For example, when copying the theorems from leanprover-community/batteries#1267, some omega and simp_all steps fail, and some lemmas used in the proofs are not available.

Other than that, all theorems in this PR are now completed.

[TwoFX]

or their proofs may have to be partially reworked, which feels a bit redundant

This is a fair point. In #176 I have added an axiom proved_elsewhere which you can use instead of sorry. This way, wo don't have a noisy build, and we can use the call hierarchy feature of the language server to easily see all places where we are relying on missing results.

If the proofs can be copy-pasted without having to redo them, I still think that copying them is better.

[marcusrossel]

Turns out I didn't need to proved_elsewhere anything now (not sure what I ran into before ¯_(ツ)_/¯). So as far as I'm concerned this PR is complete.

[TwoFX]

Very nice, thanks!