Data.Nat.EvenOddRec

Stream: mathlib4

[Shreyas Srinivas]

I noticed that Nat.odd_even_rec has not been taken up yet. I'd like to take it up. Is there anything I should know (for e.g. : this file being on the "not to be ported" list?)

[Shreyas Srinivas]

Fixed: Also I don't see data.nat.bits and init.data.nat.bitwise in master yet. I thought this was already merged (see: mathlib4#1095

[Shreyas Srinivas]

PR mathlib4#1148

[Arien Malec]

I looked at it briefly --- it uses bit1, bit0 and theorems about bit and bit0/1heavily so probably wants some design thought to use a more sensible definition of parity or blaze on.

[Shreyas Srinivas]

Is this something that needs to be done during or after the port?

[Mario Carneiro]

it's best to just translate as is for now; deprecate anything with bit0/bit1 in the statement and put a TODO on any proofs that require referencing deprecated definitions (but otherwise translate them as normal), and do it all in a section deprecated where you turn off the linter (and put another TODO on that)

[Shreyas Srinivas]

In addition, the purpose of this file is to give users the option to avoid using bit0 and bit1. So it seems like a good idea to port it. I will try to finish by tonight (CET)

[Shreyas Srinivas]

So, I just started making the non-trivial fixes. In doing so there was a problem with lean not being able to fill in the implicit parameters of binary_rec_eq. So I supplied them. I got one of the strangest errors I have seen thus far:

Hb : ∀ (z : P 0), brecPind false 0 z = z
application type mismatch
  binary_rec_eq (Hb h0)
argument
  Hb h0
has type
  @Eq (P (bit false 0)) (brecPind false 0 h0) h0 : Prop
but is expected to have type
  @Eq (P (bit false 0)) (brecPind false 0 h0) h0 : Prop

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

Here's the #mwe:

import Mathlib.Data.Nat.Basic
import Mathlib.Init.Data.Nat.Bitwise


namespace Nat


@[elab_as_elim]
def evenOddRec {P : ℕ → Sort _} (h0 : P 0) (h_even : ∀ (n) (ih : P n), P (2 * n))
    (h_odd : ∀ (n) (ih : P n), P (2 * n + 1)) (n : ℕ) : P n := by
  refine' binaryRec h0 (fun b i hi => _) n
  cases b
  · simpa [bit, bit0_val i] using h_even i hi
  · simpa [bit, bit1_val i] using h_odd i hi
#align nat.even_odd_rec Nat.evenOddRec

@[simp]
theorem even_odd_rec_zero (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) : @evenOddRec _ h0 h_even h_odd 0 = h0 :=
  binary_rec_zero _ _
#align nat.even_odd_rec_zero Nat.even_odd_rec_zero

@[simp]
theorem even_odd_rec_even (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
    @evenOddRec _ h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n) := by
  have bit_val_zero : ∀ n, 2 * n = bit false n := by
    intro
    rw[bit_val, cond]
    simp
  have bit_val_one : ∀ n, 2*n+1 = bit true n := by
    intro
    rw [bit_val, cond]
  let brecPind : (b : Bool) → (n : ℕ) → P n -> P (bit b n):= λ (b : Bool) (n : ℕ) (h_n : P n) => by
    cases b
    case false =>
        have h_2n : P (2*n) := h_even n h_n
        rw [bit_val_zero] at h_2n
        exact h_2n
    case true =>
        have h_2n_1 : P (2*n + 1) := h_odd n h_n
        rw [bit_val_one] at h_2n_1
        exact h_2n_1
  have Hb: ∀ z, brecPind false 0 z = z := sorry
  refine @binary_rec_eq P h0 (fun b n => _) (Hb h0) false n
  · exact (bit0_eq_two_mul _).symm
  · exact (bit0_eq_two_mul _).symm
  · apply heq_of_cast_eq
    rfl
  · exact H

@[simp]
theorem even_odd_rec_odd (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
    @evenOddRec _ h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n) := by
  convert binary_rec_eq _ true n
  · exact (bit0_eq_two_mul _).symm
  · exact (bit0_eq_two_mul _).symm
  · apply heq_of_cast_eq
    rfl
  · exact H


end Nat

[Shreyas Srinivas]

You can see the other theorem in its pristine lean3 form for comparison. The proofs are almost entirely identical

[Shreyas Srinivas]

The question is, how does this error even make sense?

argument
  Hb h0
has type
  @Eq (P (bit false 0)) (brecPind false 0 h0) h0 : Prop
but is expected to have type
  @Eq (P (bit false 0)) (brecPind false 0 h0) h0 : Prop

[Kevin Buzzard]

If you switch pp.all on you'll see they're different.

[Shreyas Srinivas]

But @Eq seems to suggest that all implicit parameters are already in there

[Kevin Buzzard]

yeah you're right, I don't see why they can't match.

[Kevin Buzzard]

Oh but pp.all shows more than just the implicit parameters -- everything has to match -- but I don't see why it won't match.

[Shreyas Srinivas]

Ok I think I fixed it.

[Kevin Buzzard]

Nice. I would really not recommend doing what you're doing though: you're defining brecPind in tactic mode with rw so there will be random stuck eq.recs in your definition and it will be hell to work with.

[Shreyas Srinivas]

What's the cleaner method?

[Kevin Buzzard]

I don't know enough about Lean 4 to answer this :-(

[Kevin Buzzard]

But this approach is not being used in the Lean 3 file. Did you have to diverge from the autoported file for some reason?

[Shreyas Srinivas]

Yeah
You can see the proof of the theorem after. These two proofs are exactly identical (except true vs false)

[Shreyas Srinivas]

even_odd_rec_odd

[Shreyas Srinivas]

The error you get there is
don't know how to synthesize implicit argument
@binary_rec_eq ?m.5713 ?m.5714 ?m.5715 ?m.5716 true n

[Shreyas Srinivas]

The second one is the mathlib3 version with the minor corrections necessary for mathlib4 (tt => true, ff => false)

[Kevin Buzzard]

I would be tempted to convert @binary_rec_eq _ _ _ _ true n and then try and fill in the blanks

[Shreyas Srinivas]

Doesn't work. The first two blanks are easy to fill. This still leaves the blank for the parameter f which is where brecPind comes in

[Shreyas Srinivas]

Also, I am learning that unfold looks for names only in _root_.. It wont unfold brecPind

[Kevin Buzzard]

yeah this sort of thing is hell, and a very long way from my area of expertise (I'm a mathematician).

[Shreyas Srinivas]

Here's a funny goal when I use brecPind: instMulNat = { mul := Nat.add }

[Shreyas Srinivas]

I am beginning to think lean4 believes 2+2 = potato

[Kevin Buzzard]

Lean 3 convert seems more powerful than Lean 4 convert here?

[Shreyas Srinivas]

or probably even broken

[Shreyas Srinivas]

As far as I know this is false. In another case it asked me to show n=2, without any relevant additional hypothesis.

[Shreyas Srinivas]

My limited understanding of lean tactics is that they make sound transformations

[Kevin Buzzard]

Shreyas Srinivas said:

Also, I am learning that unfold looks for names only in _root_.. It wont unfold brecPind

You could try defining it outside the proof. In Lean 3 we use a trick called eq_to_hom which given a proof that a = b will give you a map from P a to P b, and we have a bunch of API around it.

[Shreyas Srinivas]

I don't think that works in this case. We will have to parametrise on the predicate P. This will bring us back to square one

[Shreyas Srinivas]

In any case, I worked around the unfold limitation`

[Shreyas Srinivas]

convert's doc-string says it is actually an improved version of refine which means it is less strict about providing complete terms. So it is odd that it cannot handle implicit terms that lean3's version can, or that it can produce absurd looking goals.

[Mario Carneiro]

it's not odd that convert will produce false goals sometimes, this usually means it has gone too deep and you need to use convert ... using 1 or so

[Kevin Buzzard]

The issue is that convert refuses to eat binary_rec_eq _ true n in Lean 4 whereas it did so in Lean 3 -- the tactic fails in Lean 4.

[Mario Carneiro]

would be nice if there was an MWE that didn't require me to pull the branch...

[Kevin Buzzard]

You can see the problem in the MWE posted above. Forget about the long broken proof: the proof after is

@[simp]
theorem even_odd_rec_odd (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
    @evenOddRec _ h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n) := by
  convert binary_rec_eq _ true n
  · exact (bit0_eq_two_mul _).symm
  · exact (bit0_eq_two_mul _).symm
  · apply heq_of_cast_eq
    rfl
  · exact H

This is what the autoporter produced. But the convert fails and I've just spent an hour trying to make it not fail, and failed.

[Shreyas Srinivas]

Shreyas Srinivas said:

Here's the #mwe:

import Mathlib.Data.Nat.Basic
import Mathlib.Init.Data.Nat.Bitwise


namespace Nat


@[elab_as_elim]
def evenOddRec {P : ℕ → Sort _} (h0 : P 0) (h_even : ∀ (n) (ih : P n), P (2 * n))
    (h_odd : ∀ (n) (ih : P n), P (2 * n + 1)) (n : ℕ) : P n := by
  refine' binaryRec h0 (fun b i hi => _) n
  cases b
  · simpa [bit, bit0_val i] using h_even i hi
  · simpa [bit, bit1_val i] using h_odd i hi
#align nat.even_odd_rec Nat.evenOddRec

@[simp]
theorem even_odd_rec_zero (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) : @evenOddRec _ h0 h_even h_odd 0 = h0 :=
  binary_rec_zero _ _
#align nat.even_odd_rec_zero Nat.even_odd_rec_zero

@[simp]
theorem even_odd_rec_even (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
    @evenOddRec _ h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n) := by
  have bit_val_zero : ∀ n, 2 * n = bit false n := by
    intro
    rw[bit_val, cond]
    simp
  have bit_val_one : ∀ n, 2*n+1 = bit true n := by
    intro
    rw [bit_val, cond]
  let brecPind : (b : Bool) → (n : ℕ) → P n -> P (bit b n):= λ (b : Bool) (n : ℕ) (h_n : P n) => by
    cases b
    case false =>
        have h_2n : P (2*n) := h_even n h_n
        rw [bit_val_zero] at h_2n
        exact h_2n
    case true =>
        have h_2n_1 : P (2*n + 1) := h_odd n h_n
        rw [bit_val_one] at h_2n_1
        exact h_2n_1
  refine @binary_rec_eq P h0 brecPind H false n
  · exact (bit0_eq_two_mul _).symm
  · exact (bit0_eq_two_mul _).symm
  · apply heq_of_cast_eq
    rfl
  · exact H

@[simp]
theorem even_odd_rec_odd (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
    @evenOddRec _ h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n) := by
  convert binary_rec_eq _ true n
  · exact (bit0_eq_two_mul _).symm
  · exact (bit0_eq_two_mul _).symm
  · apply heq_of_cast_eq
    rfl
  · exact H


end Nat

Here

[Shreyas Srinivas]

It's the entire file because I wanted to show multiple things

[Shreyas Srinivas]

Made some changes

[Shreyas Srinivas]

1. The lean3 proof of even_odd_rec_odd and even_odd_rec_even are identical
2. If you open the #mwe now. In even_odd_rec_even I had to insert explicit arguments (same as even_odd_rec_odd, but I left it untouched for reference). These produced absurd case distinctions.

[Mario Carneiro]

this MWE shouldn't need any imports at all

[Kevin Buzzard]

You need binaryRec

[Mario Carneiro]

then state it

[Kevin Buzzard]

It compiles fine on mathlib master and building the imports is also super-quick

[Shreyas Srinivas]

Bitwise is necessary. binaryRec, binary_rec_eq, and all basic Nat stuff

[Shreyas Srinivas]

It also works quickly on the lean4 playground

[Mario Carneiro]

I've been building since 5 minutes ago -_-

[Kevin Buzzard]

you need bodd and all the other stuff Shreyas has been porting over the last few days. A mathlib-free MWE would be horrible

[Mario Carneiro]

switching branches is super painful because of the nightly bumps

[Kevin Buzzard]

Is it possible to make tools to make MWEs?

[Shreyas Srinivas]

image.png

[Mario Carneiro]

I tried that and failed on the imports

[Shreyas Srinivas]

You can open this on the playground

[Mario Carneiro]

because I was on a branch from yesterday I guess

[Mario Carneiro]

but for an MWE there are way too many lines

[Shreyas Srinivas]

I used the playground button on the screenshot

[Shreyas Srinivas]

Mario Carneiro said:

because I was on a branch from yesterday I guess

It's one def, one trivial theorem, and two nearly identical theorems. At best, the first trivial theorem could be removed, but that might also cause problems. The other two theorems depend on the def.

[Shreyas Srinivas]

And both these theorems have the same issue.

1. In the first one, I show what happens when you give explicit arguments to the convert line.
2. In the second one, I leave the lean3 version of the proof as is, so you can see the issue with the mathlib3 version of the proof.

[Shreyas Srinivas]

I don't see any meaningful ways to reduce this.

[Mario Carneiro]

import Mathlib.Data.Nat.Basic

def bit (b : Bool) : ℕ → ℕ := cond b bit1 bit0
theorem bit0_val (n : Nat) : bit0 n = 2 * n := sorry
theorem bit1_val (n : Nat) : bit1 n = 2 * n + 1 := sorry

def binaryRec {C : Nat → Sort u} (z : C 0) (f : ∀ b n, C n → C (bit b n)) : ∀ n, C n := sorry

theorem binary_rec_eq {C : Nat → Sort u} {z : C 0} {f : ∀ b n, C n → C (bit b n)}
    (h : f false 0 z = z) (b n) : binaryRec z f (bit b n) = f b n (binaryRec z f n) := sorry

@[elab_as_elim]
def evenOddRec {P : ℕ → Sort _} (h0 : P 0) (h_even : ∀ (n) (ih : P n), P (2 * n))
    (h_odd : ∀ (n) (ih : P n), P (2 * n + 1)) (n : ℕ) : P n := by
  refine' binaryRec h0 (fun b i hi => _) n
  cases b
  · simpa [bit, bit0_val i] using h_even i hi
  · simpa [bit, bit1_val i] using h_odd i hi

@[simp]
theorem even_odd_rec_odd (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
    @evenOddRec _ h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n) := by
  convert binary_rec_eq _ true n

[Mario Carneiro]

you can get rid of nat.basic too if you remove the \N syntax, but we don't need to go full mathlib-free here since convert is a mathlib tactic anyway

[Kevin Buzzard]

yeah but you've sorried a bunch of data now, so if you get the convert working then it might not work in the actual use case?

[Mario Carneiro]

true, if definition unfolding is involved then you should provide the bodies of defs

[Kevin Buzzard]

In this case it would take a lot longer to make the mwe (with only proofs sorried) than it would take you to compile Data.Nat.Basic :-( It can take a super-long time to make mathlib-free mwes now, this is why I was asking about auto-generating them (apparently they can do it in Coq?)

[Mario Carneiro]

Auto-generating MWEs would be very cool

[Mario Carneiro]

I think there are a couple levels we have to unlock before we can get there though

[Mario Carneiro]

But the set of things that come to bear on a single line of proof is generally approximately constant

[Mario Carneiro]

(unless it's a really bad definition-unfolding proof or a typeclass problem)

[Shreyas Srinivas]

Mario Carneiro said:

Auto-generating MWEs would be very cool

Could this not be hard to debug though? Especially in tactic heavy proofs

[Mario Carneiro]

why?

[Shreyas Srinivas]

Kevin Buzzard said:

yeah but you've sorried a bunch of data now, so if you get the convert working then it might not work in the actual use case?

This for example

[Mario Carneiro]

the other tactics in the proof are hopefully not relevant and can be removed

[Mario Carneiro]

As long as convert doesn't unfold the definition, it doesn't matter what's behind it

[Mario Carneiro]

In this case I belatedly realized you are unfolding evenOddRec to binaryRec in this line of proof so we need that definition, but not the stack leading up to binaryRec

[Shreyas Srinivas]

In broad terms: Tactics are doing very useful, but invisible work behind the scenes . It takes time to hone one's understanding about their exact behaviour. So one can only make educated guesses about what causes the error one observes using the tactic state output (and maybe pp). For example, if Kevin had not pointed out that sorrying out things might remove errors in downstream tactic uses, I would assume that such an example is in fact adequate.

[Mario Carneiro]

I think it's fine to start with aggressive sorrying and re-add stuff if it turns out it was oversimplified

[Mario Carneiro]

@[elab_as_elim]
def evenOddRec {P : ℕ → Sort _} (h0 : P 0) (h_even : ∀ (n) (ih : P n), P (2 * n))
    (h_odd : ∀ (n) (ih : P n), P (2 * n + 1)) (n : ℕ) : P n :=
  binaryRec h0 (fun
    | false, i, hi => (bit0_val i ▸ h_even i hi : P (bit0 i))
    | true, i, hi => (bit1_val i ▸ h_odd i hi : P (bit1 i))) n

@[simp]
theorem even_odd_rec_even (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
    @evenOddRec _ h0 h_even h_odd (2 * n) = h_even n (evenOddRec h0 h_even h_odd n) :=
  have : ∀ a, bit false n = a → HEq (@evenOddRec _ h0 h_even h_odd a) _
    | _, rfl => by rw [evenOddRec, binary_rec_eq]; apply eq_rec_heq; exact H
  eq_of_heq (this _ (bit0_val _))

@[simp]
theorem even_odd_rec_odd (n : ℕ) (P : ℕ → Sort _) (h0 : P 0) (h_even : ∀ i, P i → P (2 * i))
    (h_odd : ∀ i, P i → P (2 * i + 1)) (H : h_even 0 h0 = h0) :
    @evenOddRec _ h0 h_even h_odd (2 * n + 1) = h_odd n (evenOddRec h0 h_even h_odd n) :=
  have : ∀ a, bit true n = a → HEq (@evenOddRec _ h0 h_even h_odd a) _
    | _, rfl => by rw [evenOddRec, binary_rec_eq]; apply eq_rec_heq; exact H
  eq_of_heq (this _ (bit1_val _))

[Shreyas Srinivas]

okay that worked wow!

[Shreyas Srinivas]

I will commit this as is, but I am going to spend some time understanding this afterwards

[Shreyas Srinivas]

So in this proof you used heterogeneous equality, which I am guessing coerces equality between values of different types. Is there like a comprehensive list of ways this can go wrong (apart from the congr issue)? It seems quite handy for functional programmers, so I can see this getting wrongly used

[Shreyas Srinivas]

Data.Nat.EvenOddRec passed all checks and is ready to merge.

[Mario Carneiro]

Shreyas Srinivas said:

So in this proof you used heterogeneous equality, which I am guessing coerces equality between values of different types. Is there like a comprehensive list of ways this can go wrong (apart from the congr issue)? It seems quite handy for functional programmers, when dealing with representation issues, so I can potentially see this getting wrongly used

This sort of thing is what we call "DTT hell". It hopefully doesn't come up that often, but this is the standard trick for dealing with it: do induction on some equality with a carefully chosen "motive" (that is, the type of the have statement in this example) to do dependent rewrites. Most of lean's tactics will not handle this situation well, either complaining "the motive is not type correct" or doing nothing at all, so you have to do it manually in this way.

[Mario Carneiro]

the heterogeneous equality is needed to make the motive typecheck, since the LHS has type P a and the RHS has type P (2 * n)

[Mario Carneiro]

I'm not sure exactly what you mean by ways this can go wrong. This is a proof technique, it has a limited range of applicability but if it works then it works

[Shreyas Srinivas]

Mario Carneiro said:

Shreyas Srinivas said:

So in this proof you used heterogeneous equality, which I am guessing coerces equality between values of different types. Is there like a comprehensive list of ways this can go wrong (apart from the congr issue)? It seems quite handy for functional programmers, when dealing with representation issues, so I can potentially see this getting wrongly used

This sort of thing is what we call "DTT hell". It hopefully doesn't come up that often, but this is the standard trick for dealing with it: do induction on some equality with a carefully chosen "motive" (that is, the type of the have statement in this example) to do dependent rewrites. Most of lean's tactics will not handle this situation well, either complaining "the motive is not type correct" or doing nothing at all, so you have to do it manually in this way.

By "going wrong" I am referring to the note of caution inside docs4#HEq

[Shreyas Srinivas]

But I think I get the gist

[Shreyas Srinivas]

Thanks

[Shreyas Srinivas]

Hi,
I noticed that mathlib4#1148 has not been merged yet. Is there some issue with this PR that needs fixing?

[Kevin Buzzard]

It has no reviews and at the time of writing it doesn't even have a green tick. We don't yet know if there are issues with this PR that need fixing because it looks like nobody got round to looking at it yet other than Reid, who fixed some naming. Wel'l get there. Is this file on the critical line to any of the standard targets like data.real.basic ? Usually when I review I start at the top of #queue4 and probably when you get the green tick back you'll be at the bottom of that queue? I'm not sure about how the order works to be honest.

[Shreyas Srinivas]

Ah okay, I noticed a fresh commit from @Reid Barton

[Shreyas Srinivas]

Some names were fixed to meet the lean4 style. As I recall it, it was green last night.

[Kevin Buzzard]

Feel free to review other PRs on #queue4 ; this will get yours to the top quicker.