data.nat.bits

Stream: mathlib4

[Shreyas Srinivas]

Hi, I noticed that data.nat.bits is ready for porting and I would like to port it. In the [linked message] (https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/data.2Eset.2Ebasic/near/314081134) @Sky Wilshaw mentions that there are some changes between lean 3 and 4 regarding bit0 and bit1. I would be grateful for any help with knowing what these changes are and how this affects the port. Thanks in advance.

[Shreyas Srinivas]

Additionally, I can't seem to follow step 4 of the porting process of claiming the file (no permission to edit wiki). Is it absolutely essential that I do this?

[Kevin Buzzard]

bit0 and bit1 are now deprecated and this file is being ignored. It will probably end up in core/std and I'm not sure it's used too much in mathlib. If you tell us your github userid and ping @maintainers without the quotes then someone will give you push access to the wiki file. Sorry for the confusion. Right now most porters are mathlib3 contributors! Thanks for joining us!

[Shreyas Srinivas]

Hi everyone,
So after the discussion in port progress (see : https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/316239933), I started porting data.nat.bits. The following happened in sequence.

1. I opened data.nat.bits and after correcting mathbin to mathlib, I found a number of identifiers such as bodd, bit _ _ , bodd_bit etc that lean couldn't find definitions for.
2. I looked at the corresponding mathlib3 file and documentations and traced these identifiers to init.data.nat.bitwise
3. I looked for the corresponding lean 4 file Init.Data.Nat.Bitwise. This file looks completely different from the lean3 file.

Now I can think of a few different ways, to fix this:

1. Write replacement definitions myself.
2. Try replacing them with the new definitions in Init.Data.Nat.Div.

From a porting perspective, it seems to make sense to just add new defs for these missing names, and leave the existing declarations of data.nat.bits untouched. If this is to be done, where should these new defs be added.

Is there a simpler fix?

[Siddhartha Gadgil]

Definitions that were removed from the lean core should be added to Mathlib/Init/Data/Nat/Div. They are in lean3port (partly broken as in mathlib3port)

[Siddhartha Gadgil]

So one has to port partly from lean3port and partly from mathlib3port.

[Shreyas Srinivas]

Okay, in this case, I will have to add init.data.nat.bitwise and see if there are still dependencies on init.data.nat.div

[Shreyas Srinivas]

In this file I see a lot of tt and ff, are these in any way distinct from true and false?

[Shreyas Srinivas]

The problem is they produce redundant case distinctions as far as lean 4 goes.

[Ruben Van de Velde]

tt is lean3 syntax for true

[Shreyas Srinivas]

ah okay. that makes a lot of sense now. lean3port appears to have left many of these untouched for very good reasons.

[Shreyas Srinivas]

what is the xor operator for Bool in lean 4? Currently xor defaults to Nat.xor (because there is such an instance in Init.Data.Nat.Bitwise (the one not inside mathlib4)

[Yaël Dillies]

In Lean 3, it's docs#bxor. Does docs4#BXor hit anything?

[Shreyas Srinivas]

unfortunately no.

[Shreyas Srinivas]

My best bet right now seems to be to define my own Boolean Xor. Quite a few identifiers there are undefined. My next issue is going to be with bit0 and bit1.

[Shreyas Srinivas]

But from a library design standpoint, and language consistency standpoint, this is not ideal

[Ruben Van de Velde]

I remember now why I'm getting a déjà vu feeling about your questions... We moved the xor stuff to data.nat.bits because I didn't figure out how to port them in mathlib4#729 :)

[Shreyas Srinivas]

If we put the boolean xor in data.nat.bits :

1. We will have a circular dependency between data.nat.bits and Init.Data.Nat.Bitwise
2. We have inconsistent naming. Why should operations for Bool be hidden inside a Nat related file

[Shreyas Srinivas]

What is the suggested fix? Should I define the boolean xor inside Init.Data.Nat.Bitwise?

[Yaël Dillies]

Is there no Bool.defs file?

[Shreyas Srinivas]

Found an xor inside Bool.Basic

[Shreyas Srinivas]

Is there a way to make a qualified import so that I can use it instead of Nat.xor?

[Shreyas Srinivas]

more specifically, is abbrev bxor = xor which seems to do the trick okay? Should the name be hidden somehow?

[Arien Malec]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/status.20of.20data.2Enat.2Ebits/near/313758405

[Shreyas Srinivas]

Arien Malec said:

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/status.20of.20data.2Enat.2Ebits/near/313758405

There was an update to this : https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/316239933

[Arien Malec]

Hmm. I didn't see @Mario Carneiro weigh in there... My understanding is that the reason bit0/bit1 appear all over mathlib is because they are central to binary representation in Lean 3, but bitwise operations are going to be done differently in Lean 4

[Arien Malec]

And otherwise bit0/bit1 are incomplete ways of spelling even and odd which will get ported in algebra.parity

[Shreyas Srinivas]

Arien Malec said:

Hmm. I didn't see Mario Carneiro weigh in there... My understanding is that the reason bit0/bit1 appear all over mathlib is because they are central to binary representation in Lean 3, but bitwise operations are going to be done differently in Lean 4

My understanding is that this is holding up the port process. It makes sense to separate the porting process from these fixes. Avoids all sorts of deadlocks. The file can be deprecated or perhaps some renaming done as soon as the necessary changes to std are made.

[Arien Malec]

fair enough....

[Shreyas Srinivas]

For now I think defining abbreviations

abbrev bit0 := 0
abbrev bit1 :=1

is the quickest fix

[Shreyas Srinivas]

@experts : Is this acceptable for now?

[Shreyas Srinivas]

Then, in order to meet this requirement (https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/port.20progress/near/316275723)
I manually change occurrences of bit0 and bit1 to 0 and 1 respectively, in all statements (but not proofs)

[Yaël Dillies]

I don't understand. That means you will be writing a bunch of useless lemmas that don't have mathlib counterparts.

[Yaël Dillies]

Why don't you just keep the current meaning of bit0 and bit1?

[Shreyas Srinivas]

Currently bit0 and bit1 have no meaning in lean4. Giving them the same meaning would mean writing all these instances here :
https://leanprover-community.github.io/mathlib_docs/init/core.html#bit0

[Yaël Dillies]

What instances do you mean? I see none in there.

[Yaël Dillies]

Oh, you mean typeclass arguments?

[Shreyas Srinivas]

Yaël Dillies said:

What instances do you mean? I see none in there.

Yes

[Yaël Dillies]

Then please do.

[Shreyas Srinivas]

Okay, I'll do that. I just realised my abbrevs wont work on some of them anyway. This will go inside Init.Data.Nat.Bitwise

[Shreyas Srinivas]

Found bit0 and bit1 in Mathlib.Init.ZeroOne

[Kevin Buzzard]

A good way to find everything is import Mathlib.

[Jireh Loreaux]

or docs4#bit0 and docs4#bit1.

[Kevin Buzzard]

(and you can send messages to yourself on Zulip if you want to experiment with other docs4# stuff)

[Jireh Loreaux]

@Shreyas Srinivas I'm confused about what you wrote:
Shreyas Srinivas said:

For now I think defining abbreviations

abbrev bit0 := 0
abbrev bit1 := 1

is the quickest fix

Do you realize that this isn't what bit0 and bit1 mean? bit0 x = x + x

[Shreyas Srinivas]

Consider that canceled

[Shreyas Srinivas]

I said that two seconds before I read the definition

[Johan Commelin]

Kevin Buzzard said:

(and you can send messages to yourself on Zulip if you want to experiment with other docs4# stuff)

Talking to yourself on zulip is one of those things that's much more helpful than you'd think :grinning:

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

Shreyas Srinivas said:

Found bit0 and bit1 in Mathlib.Init.ZeroOne

Using this now

[Shreyas Srinivas]

I am encountering a number of errors with the cases tactic in Init.data.nat.bitwise . The documentation says that the tactic basically expands objects of an inductive type along each of its constructors, in order to a case-by-case analysis. By that definition the proofs look like they ought to work. Basically lean complains that the definition is not really inductive on objects of the Bool type

Before I individually tackle these proofs and fix them, is there a known issue? Are there standard fixes?

[Kevin Buzzard]

Can you give a mwe?

[Shreyas Srinivas]

mwe?

[Kevin Buzzard]

#mwe . That's the best way to ask a question on this site.

[Shreyas Srinivas]

abbrev ℕ := Nat
open Nat
def boddDiv2 : ℕ → Bool × ℕ
  | 0 => (false, 0)
  | succ n =>
    match boddDiv2 n with
    | (false, m) => (true, m)
    | (true, m) => (false, succ m)


def div2 (n : ℕ) : ℕ :=
  (boddDiv2 n).2

def bodd (n : ℕ) : Bool :=
  (boddDiv2 n).1


@[simp]
theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
  unfold bodd <;> unfold boddDiv2 <;> cases boddDiv2 n <;> cases fst <;> rfl

[Shreyas Srinivas]

fails at cases fst. This is directly from the library with abbrev \N = Nat and open Nat

[Kevin Buzzard]

There is no fst. There is a fst✝ but that is inaccessible.

[Shreyas Srinivas]

But why does it work in lean 3 (from where, modulo lean3port, the code came)? and what's the typical fix?

[Ruben Van de Velde]

Does cases' fst with fst fst work?

[Kevin Buzzard]

In Lean 3 there were no inaccessible terms. You are using the code generated by the porting program, right? mathlib3port and lean3port?

[Ruben Van de Velde]

Lean 3 introduced more (accessible) names automatically

[Shreyas Srinivas]

yeah

[Shreyas Srinivas]

Ruben Van de Velde said:

Does cases' fst with fst fst work?

cases' is an unknown tactic (playground link : https://lean.math.hhu.de/#code=import%20Mathlib%0A%0Aabbrev%20%E2%84%95%20%3A%3D%20Nat%0Aopen%20Nat%0Adef%20boddDiv2%20%3A%20%E2%84%95%20%E2%86%92%20Bool%20%C3%97%20%E2%84%95%0A%20%20%7C%200%20%3D%3E%20(false%2C%200)%0A%20%20%7C%20succ%20n%20%3D%3E%0A%20%20%20%20match%20boddDiv2%20n%20with%0A%20%20%20%20%7C%20(false%2C%20m)%20%3D%3E%20(true%2C%20m)%0A%20%20%20%20%7C%20(true%2C%20m)%20%3D%3E%20(false%2C%20succ%20m)%0A%0A%0Adef%20div2%20(n%20%3A%20%E2%84%95)%20%3A%20%E2%84%95%20%3A%3D%0A%20%20(boddDiv2%20n).2%0A%0Adef%20bodd%20(n%20%3A%20%E2%84%95)%20%3A%20Bool%20%3A%3D%0A%20%20(boddDiv2%20n).1%0A%0A%0A%40%5Bsimp%5D%0Atheorem%20bodd_succ%20(n%20%3A%20%E2%84%95)%20%3A%20bodd%20(succ%20n)%20%3D%20not%20(bodd%20n)%20%3A%3D%20by%0A%20%20unfold%20bodd%20%3C%3B%3E%20unfold%20boddDiv2%20%3C%3B%3E%20cases%20boddDiv2%20n%20%3C%3B%3E%20cases'%20fst%20with%20fst%20fst%20%3C%3B%3E%20rfl%0A)

[Kevin Buzzard]

You can get it with import Mathlib.Tactic.Cases. The problem seems to be that the definitions of boddDiv2 generated by the equation compilers in Lean 3 and Lean 4 are different.

[Kevin Buzzard]

-- lean 3
import logic.basic

open nat

@[simp] lemma bodd_succ' (n : ℕ) : bodd (succ n) = bnot (bodd n) :=
begin
  unfold bodd bodd_div2,
  cases bodd_div2 n,
  /-
  ⊢ (bodd_div2._match_1 (fst, snd)).fst = bnot (fst, snd).fst -/
  cases fst;
  refl
end

-- lean 4

-- ... your code omitted

@[simp]
theorem bodd_succ (n : ℕ) : bodd (succ n) = not (bodd n) := by
  unfold bodd
  unfold boddDiv2
  cases boddDiv2 n with
  /-
  ⊢ (match x✝ with
    | (false, m) => (true, m)
    | (true, m) => (false, succ m)).fst =
  !(match n with
      | 0 => (false, 0)
      | succ n =>
        match boddDiv2 n with
        | (false, m) => (true, m)
        | (true, m) => (false, succ m)).fst
        -/
  | mk fst snd =>
    cases fst with
    | true => sorry
    | false => sorry

[Shreyas Srinivas]

Thanks. it is interesting that one can use a match inside a tactic like that

[Shreyas Srinivas]

also, in many of the induction proofs. the cases clause seems unnecessary where simp is used for the base case of the induction

[Shreyas Srinivas]

This is very interesting

[Shreyas Srinivas]

An update:
I am still manually weeding out errors in Init.Data.Nat.Bitwise of which there were a considerable number in the beginning.

1. A number of errors can be traced to inaccessible variables. I have removed those with rename_i.
2. A number of errors arise from the rw tactic. Some are removed by applying simp instead. Others get removed when I introduce that part of the proof in a have statement. My goal tomorrow is to identify more of these cases and narrow them down
3. I would be grateful for any help with binaryRec, theorem bodd_succ and theorem div2_succ.

You can see the current state on the latest commit in mathlib4#1075.

[Shreyas Srinivas]

@Scott Morrison I saw your comment on the issue. I will do this tomorrow. Is there a simple way to move the PR or is a fresh one required?

[Shreyas Srinivas]

In addition, Data.Nat.Bits is less than half the size of Bitwise and has tiny proofs for the most part. So hopefully once this file is done, data.nat.bits will follow soon.

[Siddhartha Gadgil]

@Shreyas Srinivas
One way to make a PR from a branch is to merge your PR (which is into a mathlib4 branch) and then make a PR from there. But after that it is better to just push to the branch on mathlib4 by changing the git remote (or checking it out) otherwise changes made by others will cause a mess.

[Shreyas Srinivas]

New PR mathlib4#1095

[Shreyas Srinivas]

Need some help with tactics:
I have the following tactic state:

C: ℕ → Sort u
z: C 0
f: (b : Bool) → (n : ℕ) → C n → C (bit b n)
h': f false 0 z = z
b: Bool
n: ℕ
h: bit b n = 0
bf: false = b
n0: 0 = n
e✝: C (bit false 0)
e: C 0
⊢ e✝ = z

For context, there is a theorem bit_zero that says bit false 0 = 0. I applied rw on e^{\dagger} to get e. I was under the impression that I could use proof irrelevance to show the goal. How do I get there?

[Shreyas Srinivas]

Is there such a way?

[Kevin Buzzard]

Your goal shouldn't contain inaccessible terms, they're inaccessible. How did the dagger term appear? You should have named it when it did

[Shreyas Srinivas]

The goal looked like this:

C: ℕ → Sort u
z: C 0
f: (b : Bool) → (n : ℕ) → C n → C (bit b n)
h': f false 0 z = z
b: Bool
n: ℕ
h: bit b n = 0
bf: false = b
n0: 0 = n
e: C (bit false 0)
⊢ e = z

Then I applied
rw [bit_zero] at e
This gave the goal you see there

[Shreyas Srinivas]

Okay, I think I found the mistake. C does not return a value of type Prop

[Shreyas Srinivas]

are there limits on how deep rw can look and replace terms in lean4? I see instances where rw should work per the basic idea that it takes equalities and replaces instances of LHS with RHS, but it doesn't do so.

[Shreyas Srinivas]

The lean3port version of the proof makes it clear that the same rw's actually work in lean3

[Shreyas Srinivas]

Update + Help Needed:

1. Update : I have reduced the errors in Init.Data.Nat.Bitwise to about 5 theorems.
2. Help needed : I need help with the proof of test_bit_bitwise. Producing an #mwe is next to impossible because of the dependency chain.

Specifically : in commit https://github.com/leanprover-community/mathlib4/pull/1095/commits/b1cac6a15b860e7e4420fa021de72dfc596caf06
(This is the top commit on this branch data_nat_bits right now ).

In lines 544 and 540, I have reduced the goal to testBit (succ n) (succ k) = true and testBit (succ n) (succ k) = false respectively.
These are the cases I generated using the line cases testBit (succ n) (succ k) (line 534) in the first place, so it seems that trivially these goals should be true (by the case distinction). I am not sure how to make this claim a proof

[Shreyas Srinivas]

A screenshot if it helps :
image.png

[Anand Rao]

@Shreyas Srinivas Just to clarify, is the proof also supposed to have a succ.succ case?

[Anand Rao]

Here is the code: https://github.com/leanprover-community/mathlib4/pull/1095/commits/feedbe3a84e06d4a190d3289420a664926c97981

[Shreyas Srinivas]

Anand Rao said:

Shreyas Srinivas I have pushed a fix for test_bit_bitwise, following this Lean3 proof.

That is where is started. It seemed it wouldn't work, which is how I ended up with the long proof.

[Shreyas Srinivas]

It works thanks

[Scott Morrison]

@Shreyas Srinivas, @Anand Rao, anyone else working on Data.Nat.Bits.

I don't think it was a good idea to start translating proofs that were about mathlib3's bitwise into proofs about Lean 4's bitwise.

We just don't care, for the purpose of getting the port done, what Lean 4 thinks bitwise means. We just copy across the mathlib3 bitwise, call it bitwise' to avoid a name collision, and get on with it.

I've done this, and removed all the errors in Mathlib.Init.Dat.Nat.Bitwise.

What I want to do next is to change all the theorems you've written in terms of (Lean 4's) bitwise back into theorems about (mathlib3's) bitwise'. This will obviate the need for the sorried bitwise_eq_bitwise' I added, because nothing in this file will mention bitwise itself.

However doing so seems like if might be reverting a bunch of your work, so I wanted to discuss this first.

[Shreyas Srinivas]

Scott Morrison said:

Shreyas Srinivas, Anand Rao, anyone else working on Data.Nat.Bits.

I don't think it was a good idea to start translating proofs that were about mathlib3's bitwise into proofs about Lean 4's bitwise.

We just don't care, for the purpose of getting the port done, what Lean 4 thinks bitwise means. We just copy across the mathlib3 bitwise, call it bitwise' to avoid a name collision, and get on with it.

I've done this, and removed all the errors in Mathlib.Init.Dat.Nat.Bitwise.

What I want to do next is to change all the theorems you've written in terms of (Lean 4's) bitwise back into theorems about (mathlib3's) bitwise'. This will obviate the need for the sorried bitwise_eq_bitwise' I added, because nothing in this file will mention bitwise itself.

However doing so seems like if might be reverting a bunch of your work, so I wanted to discuss this first.

I had to undo a substantial number of errors arising from rw, simp, cases etc. Undoing all that work might mean starting with 70 odd errors again (took me 3.5 days to bring it all down)

[Shreyas Srinivas]

So I would like to understand what this entails

[Shreyas Srinivas]

In terms of errors that might creep back in

[Scott Morrison]

Hopefully just:

1. comment out bitwise_eq_bitwise'
2. see which theorems break
3. change their statements to being about bitwise' rather than bitwise
4. replace your new proofs with the proofs that mathport provides in lean3port

[Scott Morrison]

I think step two is only bitwise_zero_left and bitwise_zero_right.

[Shreyas Srinivas]

Further, if it indeed doesn't matter and you have fixed all the errors (as I recall, there were errors in 4 or 5 theorems as of 9 hours ago), is there a reason to change it now?

[Shreyas Srinivas]

What's the trade off between making this change vs proving bitiwise_eq_bitwise'

[Scott Morrison]

My change fixed all the errors, at the expense of one sorry, namely bitwise_eq_bitwise'

[Scott Morrison]

I just pushed another change that postpones that later in the file, and it only needed to make the definitions of lor and land match up.

[Scott Morrison]

I don't really want this to hold up other stuff. I propose we just define lor' and land' the mathlib3 way too. These are barely used later in mathlib.

[Shreyas Srinivas]

Okay. As a beginner, I guess I am okay with changes as long as I don't have to redo the error fixing for several hours more

[Shreyas Srinivas]

Hopefully this does not require significant refactoring downstream. All the occurrences of bitwise might have to be replaced with bitwise'. Is this something that should be recorded on the port wiki?

[Scott Morrison]

All done.

[Scott Morrison]

No, we don't have to record this at all.

[Scott Morrison]

The #align nat.bitwise Nat.bitwise' will do the translation automatically in all downstream files.

[Shreyas Srinivas]

Okay. I will get started on data.nat.bits then

[Scott Morrison]

Mathlib.Init.Data.Nat.Bitwise is error and sorry free (but all in terms of mathlib3 definitions, no contact at all with Lean 4's bitwise.)

[Scott Morrison]

I left a -- Porting note explaining that if one wants to merge these, you should start with the theorem bitwise_eq_bitwise', which I stated, but left commented out.

[Anand Rao]

Should I change the name of the theorem bitwise_bit_aux to bitwise'_bit_aux?

[Shreyas Srinivas]

So I will leave that untouched for now and use the file as is. I guess as long as it is error free bitwise_bit_aux needs no further changes?

[Anand Rao]

Yes, bitwise_bit_aux does not need any changes. I was only suggesting the renaming to keep it consistent with the rest of the file.

[Shreyas Srinivas]

Ah okay. I'll take care of that, once I get to my office

[Shreyas Srinivas]

Shreyas Srinivas said:

Update + Help Needed:

1. Update : I have reduced the errors in Init.Data.Nat.Bitwise to about 5 theorems.
2. Help needed : I need help with the proof of test_bit_bitwise. Producing an #mwe is next to impossible because of the dependency chain.

Specifically : in commit https://github.com/leanprover-community/mathlib4/pull/1095/commits/b1cac6a15b860e7e4420fa021de72dfc596caf06
(This is the top commit on this branch data_nat_bits right now ).

In lines 544 and 540, I have reduced the goal to testBit (succ n) (succ k) = true and testBit (succ n) (succ k) = false respectively.
These are the cases I generated using the line cases testBit (succ n) (succ k) (line 534) in the first place, so it seems that trivially these goals should be true (by the case distinction). I am not sure how to make this claim a proof

For port purposes, this question got resolved. But I am curious about this: if you use cases x on some bool x, then presumably you have one case for x being true and another for x being false. So how do you show a goal like x = true and x=false in the respective cases. rfl did not work for me, but I can guess that this was because of the absence of an explicit hypothesis to this effect. What's the solution then?

[Scott Morrison]

Can you give a #mwe? Usually in this case I would expect such a goal to be replaced by true = true!

[Scott Morrison]

You may be looking for cases h : x or cases' h : x. Read the doc-strings for those two tactics.

[Scott Morrison]

Data.Nat.Bits is down to one annoying error about casts, where I'm forgetting how to use HEq, as usual.

[Mario Carneiro]

do you want help with the proof? what's the theorem / goal?

[Shreyas Srinivas]

Mario Carneiro said:

do you want help with the proof? what's the theorem / goal?

@Mario Carneiro : directed to me or @Scott Morrison ?

[Mario Carneiro]

@Scott Morrison

[Mario Carneiro]

I think scott already gave you the clue for your issue

[Scott Morrison]

@[simp]
theorem bitCasesOn_bit {C : ℕ → Sort u} (H : ∀ b n, C (bit b n)) (b : Bool) (n : ℕ) :
    bitCasesOn (bit b n) H = H b n :=
  eq_of_heq <| (eq_rec_heq _ _).trans <| by rw [bodd_bit, div2_bit]

is the last sorry.

[Scott Morrison]

The eq_rec_heq is giving a dud goal full of mvars.

[Scott Morrison]

Presumably because bitCasesOn, defined via pattern matching, has changed slightly, and Lean can't see an eq.rec.

[Mario Carneiro]

if I'm reading the proof correctly it first introduces an HEq and then turns it into an equality with eq.rec of stuff

[Scott Morrison]

Maybe we just need to give the motive for the eq_rec_heq?

[Mario Carneiro]

Do you have a mathlib-free mwe?

[Mario Carneiro]

I assume bitCasesOn is the only new thing here

[Mario Carneiro]

oh and bit

[Scott Morrison]

This is in Mathlib.Data.Nat.Bits

[Scott Morrison]

on branch data_nat_bits

[Mario Carneiro]

yes but that will take 10 minutes ;)

[Mario Carneiro]

eq_of_heq <| (eq_rec_heq (φ := fun x => x) _ _).trans

[Mario Carneiro]

I guess it took 10 minutes anyway

[Scott Morrison]

Okay, can you explain how the phi := is helping?

[Mario Carneiro]

I suggest you change the definition of bitCasesOn to

def bitCasesOn {C : Nat → Sort u} (n) (h : ∀ b n, C (bit b n)) : C n := bit_decomp n ▸ h ..

though if the proof is going to depend on how it's written

[Mario Carneiro]

as a bonus, you don't need to specify the motive in that case

[Scott Morrison]

Nice! I still don't understand, though. :-)

[Scott Morrison]

But perhaps I should sleep, in any case.

[Mario Carneiro]

it's what you suspected: lean can't figure out the motive here, because eq_rec_heq isn't stated for arbitrary motive (which would be solved by unification), it is actually a lambda which drops one of the arguments:

set_option pp.explicit true in
#print eq_rec_heq

theorem eq_rec_heq.{u, v} : ∀ {α : Sort u} {φ : α → Sort v} {a a' : α} (h : @Eq α a a') (p : φ a),
  @HEq ((fun x x_1 ↦ φ x) a' h) (@Eq.recOn α a (fun x x_1 ↦ φ x) a' h p) (φ a) p :=
@eqRec_heq

[Scott Morrison]

Ah, I saw that (fun x x_1 ↦ φ x) at one point, and thought it was weird, but didn't follow it up.

[Mario Carneiro]

coupled with the fact that bitCasesOn doesn't use Eq.recOn, it uses Eq.mpr, I suspect it's throwing lean into confusion

[Shreyas Srinivas]

(deleted)

[Shreyas Srinivas]

What are the rules for writing documentation strings? At the moment there are 21 linting errors in Init...Bitwise alone of the form
/- definition missing documentation string -/

[Kevin Buzzard]

Please try to write docstrings as best you can. My guess is that this was a file from core Lean 3 if the mathlib4 name starts Init, and core Lean 3 was not being linted for docstrings (so the linter is only picking up on this now), but docstrings are invaluable. A simple sentence suffices. If you're not sure what to write then please ask for help.

[Shreyas Srinivas]

And there is one linter error that complains that simp can prove this lemma using simp only ..... Of course the original proofs are not using simp but unfolds and rws

[Kevin Buzzard]

Lean 4 simp is sometimes better than Lean 3. If the linter is telling you that simp can prove it then you don't have to change the proof to by simp but please remove the @[simp] attribute and make a porting note saying that in mathlib3 this was simp. That should placate the linter.

[Shreyas Srinivas]

One last linter error. Lean is complaining about some unused have that I can't see anywhere.
More specifics:

#check @Nat.binary_rec_zero /- unnecessary have this : n' < 0 -/
#check @Nat.binary_rec_eq /- unnecessary have this : n' < Nat.bit b n -/

Unfortunately, there doesn't seem to be such haves anywhere. What would cause this? I have searched across the file for such patterns.

[Riccardo Brasca]

I just encountered the same error in another file.

[Riccardo Brasca]

here

[Shreyas Srinivas]

Riccardo Brasca said:

I just encountered the same error in another file.

I checked if it might be happening because of a tactic unfolding a definition which contains haves that are unnecessary for some particular instantiation. But this does not seem to be the case, otherwise the file-wide pattern search would have returned something

[Scott Morrison]

I've resolved this now, see discussion at https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/spurious.20.60unusedHavesSuffices.60.20linter.20error.3F