Data.Fin.Basic (mathlib4#1084)

Stream: mathlib4

[Eric Wieser]

We could stick that on docs4#instOfNat I guess

[Eric Wieser]

Unfortunately Data.Fin.Basic is now full of workarounds for what we had before, so it's a bit tricky for me to test out my change

[Eric Wieser]

Eric Wieser said:

Is that true? Lean 3 didn't use mod here so it was irrelevant how it was defined

I misdiagnosed this; the cause is that in Lean3, this is true:

example (n) : nat.mod 0 n = 0 := rfl

but in Lean4, it's not

example : Nat.mod 0 n = 0 := rfl

What prevents us using the Lean3 definition of mod here?

[Eric Wieser]

For comparison, the two definitions are (docs#nat.mod)

protected def mod_core (y : ℕ) : ℕ → ℕ → ℕ
| 0 x := x
| (fuel+1) x := if h : 0 < y ∧ y ≤ x then mod_core fuel (x - y) else x

protected def mod (x y : ℕ) : ℕ :=
nat.mod_core y x x

and docs4#Nat.mod

protected def mod (x y : @& Nat) : Nat :=
  if 0 < y ∧ y ≤ x then
    Nat.mod (x - y) y
  else
    x
decreasing_by apply div_rec_lemma; assumption

[Kevin Buzzard]

docs4#Nat.mod -- bleurgh it's in core

[Eric Wieser]

Yeah, so I guess my question should have been "would MSR care if we pushed for the definition we used to have?"

[Eric Wieser]

Because if we have the old definition, then Fin.val 0 = 0 is true by rfl

[Mario Carneiro]

Actually we used to have the lean 4 definition in lean 3 (definition by well founded recursion), it was refactored in community lean because the fuel based definition evaluates by rfl and in decidable instances

[Eric Wieser]

Is that an argument for doing the same in Lean4, or is the claim that Lean4 achieves those goals without the refactor?

[Mario Carneiro]

lean4 does not achieve those goals without the refactor, but also refactoring everything to avoid well founded recursion is not a sustainable solution

[Mario Carneiro]

div/mod just happen to be especially important definitions

[Mario Carneiro]

I think we would rather have a solution which allows well founded recursions to compute by rfl, without unfolding proofs

[Eric Wieser]

Is there any disadvantage to the Lean3 spelling?

[Mario Carneiro]

it's not as good for the compiler, although in this particular case that's probably not a problem since the definition is overridden anyway

[Kevin Buzzard]

right now the main disadvantage seems to be that it's not the same as the lean 4 spelling. What is the motivation behind changing the definition?

[Mario Carneiro]

you don't want the compiled code to actually have a fuel variable

[Eric Wieser]

Kevin, are you asking what my motivation is for changing it back or Leo's for the version that's different from Lean3?

[Kevin Buzzard]

I guess I'm asking why Leo changed it but I guess actually he didn't change it, we changed it.

[Eric Wieser]

I think the only difficulty in changing the definition In Lean4 to match Lean3 is we have to reprove docs4#Nat.mod_eq; and that's only difficult because I've never written a Lean4 proof before

[Kevin Buzzard]

What does the @& Nat mean in the definition? Is this to do with @[extern]?

[Mario Carneiro]

it's a borrow annotation, these are only relevant for @[extern]s

[Henrik Böving]

It does not make any type theoretic difference, it's just meta data in an Expr tree

[Mario Carneiro]

Eric Wieser said:

I think the only difficulty in changing the definition In Lean4 to match Lean3 is we have to reprove docs4#Nat.mod_eq; and that's only difficult because I've never written a Lean4 proof before

Isn't that proof in lean 3 already? You should be able to use the mathported lean 3 proof

[Eric Wieser]

docs#nat.mod_eq doesn't exist

[Mario Carneiro]

docs#nat.mod_def

[Mario Carneiro]

I wonder if we can make a align#nat.mod_def linkifier

[Eric Wieser]

How can I find the mathport output? Based on what you said in the meeting, mathport removes its own output once someone ports it

[Mario Carneiro]

it's in the mathlib3port repo

[Eric Wieser]

Do I have to go back to an old commit?

[Eric Wieser]

Or does "mathport output" not mean the same thing as "stuff in mathlib3port"?

[Mario Carneiro]

I'm confused by the question. mathport output means stuff in mathlib3port, but you will see the #prints in new (post-port) commits, not old ones

[Eric Wieser]

Either way, I found the code at https://github.com/leanprover-community/lean3port/blob/master/Leanbin/Init/Data/Nat/Lemmas.lean#L1318-L1345

[Eric Wieser]

The · syntax is unfortunately causing trouble

[Mario Carneiro]

what trouble?

[Eric Wieser]

I get "expected command" if I paste that output in the file in coer

[Eric Wieser]

I would guess it's using syntax that isn't available yet there

[Mario Carneiro]

the dot syntax is available in core, but induction' isn't

[Mario Carneiro]

everything else looks ok

[Notification Bot]

24 messages were moved from this topic to #mathlib4 > Nat.mod 0 n = 0 no longer true by rfl by Eric Wieser.

[Johan Commelin]

This file is now error free, except for the last 10 lines:

-- Note that here we are disabling the "safety" of reflected, to allow us to reuse `nat.mk_numeral`.
-- The usual way to provide the required `reflected` instance would be via rewriting to prove that
-- the expression we use here is equivalent.
attribute [local semireducible] reflected

unsafe instance reflect : ∀ n, has_reflect (Fin n)
  | 0 => finZeroElim
  | n + 1 =>
    nat.mk_numeral q(Fin n.succ) q((by infer_instance : Zero (Fin n.succ)))
        q((by infer_instance : One (Fin n.succ))) q((by infer_instance : Add (Fin n.succ))) ∘
      Fin.val
#align fin.reflect fin.reflect

[Johan Commelin]

#lookup3 has_reflect doesn't give me output. What is the Lean 4 equivalent of has_reflect?

[Mario Carneiro]

meta code = ignore

[Mario Carneiro]

just remove it

[Mario Carneiro]

(we should #noalign has_reflect to make this clearer)

[Johan Commelin]

Where should we #noalign ?

[Mario Carneiro]

same place as the lean 3 definition

[Johan Commelin]

which is core, I guess?

[Mario Carneiro]

Somehow Mathlib.Init is really hard for people to discover

[Mario Carneiro]

actually it's probably in the meta code in init so there is probably a heading for it in Mathlib.Init.Align

[Eric Wieser]

Is the convention to #noalign Fin.reflect too?

[Mario Carneiro]

instances are usually not aligned unless they are referred to by name in lean 3

[Eric Wieser]

The reflect instances seem to always be given explicit names

[Eric Wieser]

If we don't align instances, doesn't that mean we can't use mathport to check if we ported them?

[Mario Carneiro]

mathport currently can't provide #align statements for instances even if it wanted to because it doesn't know the instance naming convention

[Eric Wieser]

Doesn't understand the mathlib3 or mathlib4 conventions?

[Eric Wieser]

Presumably it has access to the mathlib3 name by inspection?

[Mario Carneiro]

it doesn't

[Mario Carneiro]

it's part of a general class of issues due to the fact that we don't know for a given syntax which declarations correspond to it, unless we have something like an identifier foo in def foo to give us a hint where to look

[Mario Carneiro]

I'd like to fix this by adding some landmarks in the tlean file corresponding to the beginning of a new command

[Mario Carneiro]

so that we can say that everything between one landmark and the next is "owned" by that command and synport can combine that with the AST info to list all the #align commands needed

[Mario Carneiro]

that will fix to_additive, simps, alias and lots of other commands that add declarations in a weird way

[Johan Commelin]

There are four simpNF linting errors left.

[Johan Commelin]

With two, the linter claimes simp can prove this. But if you try by simp then it actually fails.

[Kevin Buzzard]

Can we minimise and open a std4 issue if there is not already an issue? I remember writing one at some point but then not tracking it

[Johan Commelin]

I dunno how to do that. If some expert can take a look at these final four errors, that would be great.

[Johan Commelin]

Is there any reason to keep the AdHoc version around:
https://github.com/leanprover-community/mathlib4/pull/1084/files#diff-c18192a96f99c01756605bb84a74796b3842d271b2afed5aa23f62a241853dc9

[Johan Commelin]

I would be happy to ditch it.

[Johan Commelin]

cc @Ruben Van de Velde @Mario Carneiro

[Ruben Van de Velde]

I have no opinion

[Johan Commelin]

I think you created the file. So if you don't care, let's remove it.

[Ruben Van de Velde]

Looks like it dates back to mathlib4#84, but Scott moved some things there in my mathlib4#729

[Johan Commelin]

Well, if someone needs it, we know where to find it.

[Johan Commelin]

There's a weird CI build failure: https://github.com/leanprover-community/mathlib4/actions/runs/3856247402/jobs/6572230703

I can't reproduce it locally

[Johan Commelin]

Ooh, actually I can reproduce. But I'm very surprised by the fact that this PR breaks Mathlib.Testing.SlimCheck.Sampleable

[Ruben Van de Velde]

Maybe that depended on the ad hoc port?

[Johan Commelin]

In a pretty bad way, if that's the case

[Johan Commelin]

Mathlib.Mathport.Syntax is also broken, it seems

[Johan Commelin]

Ooh, maybe it isn't, and the output in the logs was just garbled up

[Johan Commelin]

I have to stop for a bit. If someone else wants to fix these, that would be great.

[Johan Commelin]

The broken files seem to be

• Mathlib.Testing.SlimCheck.Sampleable
• Mathlib.Data.UInt

[Johan Commelin]

The AdHoc port contains

variables [Nonempty (Fin n)]

instance : AddMonoidWithOne (Fin n) where
  __ := inferInstanceAs (AddCommMonoid (Fin n))
  natCast n := Fin.ofNat' n Fin.size_positive'
  natCast_zero := rfl
  natCast_succ _ := Fin.ofNat'_succ

whereas the ported files has

instance : AddMonoidWithOne (Fin (n + 1)) :=
  { Fin.addCommMonoid n with
    one := 1
    natCast := Fin.ofNat
    natCast_zero := rfl
    natCast_succ := fun _ => eq_of_veq (add_mod _ _ _) }

[Johan Commelin]

This causes trouble in Mathlib.Data.UInt.

[Johan Commelin]

@Mario Carneiro @Scott Morrison what do we do?

[Ruben Van de Velde]

Didn't the ad hoc port mention this in a comment?

[Johan Commelin]

Ooh, maybe it did...

[Mario Carneiro]

the adhoc port version seems more flexible. Don't we have something like this in data.zmod?

[Mario Carneiro]

could we maybe try a backport?

[Ruben Van de Velde]

Alternatively, do we need the uint code right now?

[Mario Carneiro]

We don't (for mathlib), but it is likely to move to std so we should try not to make any decisions mutually exclusive with it

[Johan Commelin]

Ok, I'll switch to the nonempty instance and add a porting note.

[Johan Commelin]

I've pulled in some of the stuff from the AdHoc port

[Johan Commelin]

But Data.UInt still has errors

genIntDeclars UInt8
genIntDeclars UInt16
genIntDeclars UInt32
genIntDeclars UInt64
genIntDeclars USize

[Johan Commelin]

This is some macro with pretty mysterious error reporting.

[Johan Commelin]

@Mario Carneiro Could you please take a look? I have no clue at all what we want this file to look like.

[Mario Carneiro]

I believe the macro is just a fancy copy-paste which proves the same theorems for each size of integer

[Mario Carneiro]

a trick to get better error messages is to find/replace $typeName with UInt8 and then remove the syntax quotation and macro declaration to make it just a bunch of regular definitions

[Mario Carneiro]

I can't really help with the error message without more context though:

-- set_option hygiene false
-- /-- `genIntDeclars UInt8` generates a `CommRing UInt8` instance.  -/
-- local macro "genIntDeclars" typeName:ident : command => do
--   `(
    namespace UInt8
      instance : Inhabited (Fin size) where
        default := Fin.ofNat' 0 size_positive

      instance : AddSemigroup UInt8 where
        add_assoc := fun _ _ _ ↦ by rw [AddSemigroup.add_assoc _ _ _]

      instance : AddCommSemigroup UInt8 where
        add_comm := fun _ _ ↦ by rw [AddCommSemigroup.add_comm _ _]

      instance : Semigroup UInt8 where
        mul_assoc := fun _ _ _ ↦ by rw [Semigroup.mul_assoc _ _ _]

we get some errors here saying it can't find ?a + ?b + ?c, I guess some typeclasses have been redefined or something

[Mario Carneiro]

I got everything working by using a less weird proof for those instances, the only thing that is still broken is here:

      instance : Ring UInt8 where
        sub_eq_add_neg := fun _ _ ↦ congrArg mk (sub_eq_add_neg _ _)
        add_left_neg := fun a ↦ by apply eq_of_val_eq; simp [neg_def, add_def, zero_def]
        intCast n := ⟨Int.cast n⟩
        intCast_ofNat _ := rfl
        intCast_negSucc _ := rfl

the ⟨Int.cast n⟩ doesn't work because it is looking for IntCast (Fin size) where size is UInt8.size, i.e. 256

[Mario Carneiro]

Previously this worked because of a previous instance of Inhabited (Fin size) together with the instance you mentioned above

[Johan Commelin]

So maybe we need to grab even more from the AdHoc port?

[Mario Carneiro]

I'm not sure what you did exactly to the instances, but we need to know that Fin n is a ring when n > 0

[Mario Carneiro]

we need to spell n > 0 somehow but it can't be n := n' + 1 because we want to use things like UInt8.size which are not syntactically of that form

[Mario Carneiro]

The way that was used in the adhoc file was Nonempty (Fin n)

[Mario Carneiro]

we can also use Fact (0 < n) once that is ported

[Johan Commelin]

I think I did CommSemiRing

[Johan Commelin]

So that will explain the failure.

[Mario Carneiro]

I pushed my fixes for everything other than the missing Ring (Fin n) instance

[Chris Bailey]

Johan Commelin said:

Mario Carneiro Could you please take a look? I have no clue at all what we want this file to look like.

I added the macro after doing the original version of Fin some time ago when a lot of things were still in the experimentation phase. The convenience factor was that you wouldn't have to track down every integer size when there was a change/experiment implicating one of the items in the macro or its dependencies.

FWIW I agree with Mario that once you guys are relatively happy with the interface for the UInt types, the UX is probably nicer if there are individual non-macro definitions. Rust left these kinds of macro invocations in the source and it is frustrating sometimes to be directed to that in the docs.

[Mario Carneiro]

I was thinking the macro could be improved by doing it all in one command, something like run_cmd for typeName in [`UInt8, ...] do elabCommand `(...) since I think the error messages will go to the right place in that case

[Mario Carneiro]

or we can declare a fancier macro-macro to fix the error messages

[Mario Carneiro]

in principle there isn't anything stopping this kind of pattern from being just as usable as any other command

[Mario Carneiro]

it's just not worth investing too much on a macro that is used only once

[Chris Bailey]

I'll look into improving the macro.

[Mario Carneiro]

Another related work is @[to_additive], which is also doing a similar copy paste job. We could have a version of to_additive which replaces UInt8 stuff by UIntN

[Johan Commelin]

Hurray! Errors are gone

[Johan Commelin]

CI gives a green :check:

[Eric Wieser]

Does that adhoc port AddMonoidWirhOne instance create a diamond with the OfNat instance in core?

[Johan Commelin]

@Eric Wieser I have absolutely no clue.

[Eric Wieser]

Mario Carneiro said:

could we maybe try a backport?

I really think we should do this, rather than doing the refactor in the port and hoping that it won't cause us trouble later. If we do all the hard work refactoring in Lean3, then mathport will do all the lean4 work for us. If we do the refactoring in Lean4, we won't know whether it works everywhere until the port is done

[Johan Commelin]

I'm not yet convinced that we should switch to Nonempty (Fin n) in the first place.
@Mario Carneiro Why is the ad hoc port of Data/UInt.lean doing something different from the Lean 3 version of the file?

[Mario Carneiro]

again, if we only have an instance of Fin (n + 1) then Fin size doesn't work

[Mario Carneiro]

Data.UInt is a new file, not a port

[Mario Carneiro]

UInt8 didn't exist in lean 3

[Mario Carneiro]

I'm not saying we need to use Nonempty (Fin n), but we need something isomorphic to it: Inhabited (Fin n), Fact (0 < n), NeZero n are all possible alternatives

[Mario Carneiro]

that is, a typeclass on n that says it is not zero

[Mario Carneiro]

otherwise you get things like this (using the lean 4 core instance, which is defined for Fin (n+1)):

#check (1 : Fin UInt8.size)
-- failed to synthesize instance
--   OfNat (Fin UInt8.size) 1

example : (1 : UInt8) = ⟨1⟩ := rfl
-- failed to synthesize instance
--   OfNat (Fin UInt8.size) 1

[Eric Wieser]

Can we delete UInt and add it back (along with the needed refactor) after the port? It sounds like the ad hoc stuff just gets in the way of porting here

[Mario Carneiro]

I don't think this is a constructive approach to new lean 4 features. This is like saying we can't be bothered to implement ByteString theorems because it wasn't there in lean 3

[Mario Carneiro]

If anything, the file is a candidate to move to std, but that doesn't solve any of the problems you are talking about and I don't want mathlib to make it impossible to have this file

[Mario Carneiro]

this is not an ad hoc port, it is a new file

[Eric Wieser]

I don't think we should spend any time thinking about ByteString theorems until the port is done

[Mario Carneiro]

I don't think it is mathlib's call to say what other projects are doing

[Mario Carneiro]

you are talking about restricting not just mathlib but also core/std here

[Mario Carneiro]

you may as well say lean 4 itself is getting in the way of the port. Which I suppose is true but overcoming those hurdles is exactly the point of porting

[Mario Carneiro]

We have new primitives now. We need to deal with it

[Eric Wieser]

I think the thing that I don't get here is why mathlib4 during its porting stage needs to provide any theorems about UintXX

[Eric Wieser]

Generalizing things in a way that works with new Lean4 primitives (from core / std) is great, but if those primitives aren't used anywhere in mathlib then why bother solving that before the port is done?

[Mario Carneiro]

I am totally fine with moving this file out of mathlib. But if it moves to std we'll have the same theorems and the same instances causing the same problems. Maybe it will be easier to handle the problem if it is considered "out of our hands" in that way, but it's mostly just a shell game. But I don't want us to drop the theorems without replacement or moving them somewhere upstream, and I don't want std picking up said theorems to make it incompatible with mathlib, so in the end we still have to deal with the fallout.

[Eric Wieser]

in the end we still have to deal with the fallout.

I completely agree; I just think mid-port is not the time to do this because it risks creating fallout for the >80% of mathlib that we haven't tried to port yet

[Johan Commelin]

Is there anyone who has the time and energy to attempt to backport this refactor of Fin n to mathlib3?

[Chris Hughes]

I'll give it a go. What do I have to do?

[Mario Carneiro]

The instances for Fin n being a ring or having numerals etc should depend on an instance of ne_zero n, rather than being hard-coded to Fin (n+1)

[Mario Carneiro]

I think the relevant code is partly in core which is one of the reasons it wasn't refactored earlier

[Johan Commelin]

Since ne_zero is not available in core, I think we can also use nonempty (fin n).

[Johan Commelin]

That shouldn't make too much of a difference.

[Eric Wieser]

One thing to note is that the it sounds like in Lean 4 we're going to end up with a Fin n.succ instance in core, and a Fin n instance in mathlib

[Eric Wieser]

I think they'll be defeq so this isn't an issue

[Eric Wieser]

But it means that we don't need to backport to lean 3 core, only to mathlib 3

[Chris Hughes]

Could I just add the ne_zero instance in mathlib and make sure it's defeq?

[Chris Hughes]

And leave core alone?

[Johan Commelin]

I think that's what Eric is suggesting.

[Eric Wieser]

The only slight downside of that approach is that the lemmas in core like docs#fin.val_zero refer to the weaker instance. I think we ignore those lemmas anyway though.

[Chris Hughes]

https://github.com/leanprover-community/mathlib/pull/18107

[Johan Commelin]

@Chris Hughes Thanks a lot! Did you already test locally whether it compiles?

[Chris Hughes]

No

[Johan Commelin]

Also, can't you golf one_mul using mul_comm?

[Chris Hughes]

I know the data/fin folder compiles though

[Yakov Pechersky]

A while back, I started this refactor, branch#pechersky/fin-nontrivial

[Chris Hughes]

The PR now builds locally

[Eric Wieser]

Yakov Pechersky said:

A while back, I started this refactor, branch#pechersky/fin-nontrivial

Here's the previous discussion

[Eric Wieser]

I had vague recollections of objections, but it seems that all of them are resolved by docs#ne_zero now existing

[Chris Hughes]

I've almost fixed norm_num to fix the tests that are breaking #18107. However one of the tests uses guard_target which tests alpha equivalence of expressions so it is a very tough test to pass because all the instances have to be equal up to alpha equivalence. Is there a more sensible version of guard_target?

[Eric Wieser]

Would de-instancing the core instances (either in data/fin/basic.lean or in the test) help with that?

[Chris Hughes]

Not really. There was a difference in the ne_zero instance for some numeral as well.

[Chris Hughes]

I just made a guard_target\_2 that unfolded reducibles.

[Mario Carneiro]

guard_target is configurable to use either syntactic equality, alpha equiv, reducible defeq, or regular defeq. If it is not reasonable to ask for alpha equiv then you should just downgrade the test to whnfR

[Mario Carneiro]

(Oh, is this lean 3 you are talking about? In lean 3 there are other variants of guard_target which offer these different matching behaviors)

[Chris Hughes]

I couldn't find the one with the behaviour I wanted

[Mario Carneiro]

You probably want either guard_target_mod_implicit or guard_target'

[Chris Hughes]

I think guard_target_mod_implicit is the closest I guess.

[Chris Hughes]

By the way, how does expression matching work on instances. Will it match if it's a different path to the same instance as long as its defeq or something close to that?

[Eric Wieser]

IIRC expression matching matches the exact term

[Chris Hughes]

Or they can be unified I suppose

[Eric Wieser]

So instances are never something you should match on

[Chris Hughes]

Then this norm_fin is kind of flaky

[Eric Wieser]

What I'd recommend is matching with a wildcard %%inst, then docs#unify inst with the expected instance to check it's a sensible one

[Eric Wieser]

(or maybe docs#is_defeq, I don't remember the difference)

[Mario Carneiro]

In lean 3 there are a fair number of tactics that match on instances, to decide whether to do the nat thing or the int thing. I'm not sure it's worth changing them at this point

[Eric Wieser]

Can you point to one?

[Mario Carneiro]

src#tactic.norm_fin.match_fin is probably what Chris is talking about

[Mario Carneiro]

src#tactic.norm_num.eval_cast

[Eric Wieser]

That's going to fail if the term is instead fin.add_monoid_with_one.to_has_one, right?

[Eric Wieser]

Or does norm_num canonize the instances first?

[Mario Carneiro]

yes, it will fail

[Mario Carneiro]

I'm not saying this is great, I'm saying that lean 4 fixes this issue so let's just not worry about it as long as mathlib isn't broken

[Eric Wieser]

Yep, here's a repro:

import tactic.norm_fin
import data.zmod.defs

def foo (α) [has_lt α] [add_comm_monoid_with_one α] := (1 : α) < 2

example : foo (fin 3) :=
begin
  rw foo,
  norm_num -- fail
end

example : (1 : fin 3) < 2 :=
by norm_num -- ok

[Johan Commelin]

#18107 is now broken by a deterministic timeout in ring_theory/adjoin_root

[Yuyang Zhao]

Seems @[simps] of docs#adjoin_root.power_basis_aux' should be removed.

[Johan Commelin]

Seems like a legit use of simps to me? But you determined that it is causing the timeout?

[Johan Commelin]

cc @Chris Hughes

[Yuyang Zhao]

There is no @[simps] for docs#adjoin_root.power_basis_aux.

[Johan Commelin]

Yeah, but looking at the definition, it doesn't look like it would create nice simp-lemmas.

[Johan Commelin]

So to me it seems reasonable that one has simps and the other does not.

[Yuyang Zhao]

It does cause the timeout and seems the generated lemmas are not used, however. I'm not sure if there is a better solution.

[Johan Commelin]

Chris moves the simps to after the defn. Let's see if that helps.

[Yuyang Zhao]

https://github.com/leanprover-community/mathlib/compare/fin_refactor...fin_refactor2?expand=1
Also I tried to use ne_zero n for fin.last as well, but seems it may not a good idea. fin.last is used a lot in mathlib. I'm not sure if this change helps.

[Eric Rodriguez]

The power_basis simps can be quite slow, I've sometimes written them by hand instead of using simps for this sad reason :/

[Eric Wieser]

Yuyang Zhao said:

https://github.com/leanprover-community/mathlib/compare/fin_refactor...fin_refactor2?expand=1
Also I tried to use ne_zero n for fin.last as well, but seems it may not a good idea. fin.last is used a lot in mathlib. I'm not sure if this change helps.

I don't think this is a clear win; coe (fin last n) = n is currently true by rfl, which is nice

[Eric Wieser]

We can always revisit it after the port

[Eric Wieser]

Mario Carneiro said:

In lean 3 there are a fair number of tactics that match on instances, to decide whether to do the nat thing or the int thing. I'm not sure it's worth changing them at this point

Fixed in #18129 for norm_num and abel.

[Johan Commelin]

@Chris Hughes bumped this PR to match the backports that he did in mathlib 3.

[Johan Commelin]

Who wants to review it? (I worked on this PR quite a bit, so I think I shouldn't be the main reviewer.)

[Chris Hughes]

The one issue is a breakage in Data.UInt

[Chris Hughes]

There were changed to this file in master and the PR branch, so I accepted the changes in master but this broke everything. Maybe someone who understands this file can have a look, or I'll have a proper go after lunch

[Chris Hughes]

I think this should be ready now

[Eric Wieser]

I've added a dummy commit so that we can compare again with the mathport output

[Eric Wieser]

Does it makes sense to temporarily change the base commit such that review can be against that diff?

[Johan Commelin]

We're reviewing it right now.

[Johan Commelin]

Let's do a final review against your dummy commit after that.

[Reid Barton]

I just finished a review with a bunch of naming fixes, now lgtm (though I haven't been following this thread closely)

[Johan Commelin]

We're heading to some seminar. So if someone else wants to do the final review, please go ahead.

[Jihoon Hyun]

There are some fin which should be modified to Fin in comments.

[Jihoon Hyun]

I will directly fix those and give a commit if nobody's working on it

[Reid Barton]

Yes please go ahead.

[Jihoon Hyun]

Actually I already committed the fix. Now comment looks good to me, except at line 35 I missed one nat..

[Reid Barton]

I fixed that one and some other occurrences of nat.

[Jihoon Hyun]

Should cast_nat_eq_last be cast_Nat_eq_last?

[Reid Barton]

No, in a snake_case_name, the individual components always start with a lowercase letter

[Jihoon Hyun]

Then I guess the comments are now all good!

[Eric Wieser]

I'll have another look over the diff with mathport

[Eric Wieser]

Are we ready to swap the diffbase so that we can more accurately review against that?

[Eric Wieser]

I'm going to assume yes, based on @Johan Commelin's comment above. Hopefully it's easy to switch back anyway.

[Johan Commelin]

Yes, I think you can

[Eric Wieser]

Done already and left some comments

[Eric Wieser]

The add hoc port seems to have made a bunch of other refactors re moving lemmas around, and I think we should probably discard them to avoid more confusion in docstream files

[Eric Wieser]

For instance, docs#fin.comm_semiring lives in data.zmod.defs in mathlib, but in data.fin.basic in the ad-hoc port

[Eric Wieser]

I've spotted another ad-hoc refactor that we should probably backport

[Eric Wieser]

The adhoc docs#fin.add_comm_monoid implements a custom nsmul that is not defeq to the one in mathlib3

[Johan Commelin]

That's probably easier to fix on the mathlib4 side, right?

[Johan Commelin]

Also, we can move the port of fin.comm_semiring out of Data.Fin.Basic into Data.Zmod.AdHocDefs, and then import that file in Data.UInt.

[Johan Commelin]

That way we don't have to change mathlib3 right now.

[Eric Wieser]

I'm done pushing changes for now

[Eric Wieser]

That's probably easier to fix on the mathlib4 side, right?

You mean the nsmul change? Yes, we can almost certainly just revert it

[Eric Wieser]

I imagine a lot of ad-hoc things diverge from mathlib3 because someone said "I have a clean slate, let's try something different"

[Eric Wieser]

Which was fine when mathlib4 was ad-hoc, but is in my opinion a bad idea now we're trying to faithfully port mathlib3.

[Eric Wieser]

So I'd be very tempted to just rename all ad-hoc files to Some/FileAdHoc.lean so that this doesn't happen with other files, assuming there are still adhoc ports left

[Eric Wieser]

Johan Commelin said:

Also, we can move the port of fin.comm_semiring out of Data.Fin.Basic into Data.Zmod.AdHocDefs, and then import that file in Data.UInt.

I moved these, but then discovered Data.UInt doesn't even use these instances! Should we rewrite Data.Uint so that it does, write a TODO comment, or just drop them?

[Johan Commelin]

@Eric Wieser So, do you think it is merge-ready now?

[Eric Wieser]

Was the verdict that I should revert the ad-hoc nsmul refactor, rather than ask someone to backport it?

[Johan Commelin]

Yes, that sounds good to me

[Eric Wieser]

(note also that we definitely should not merge without first switching the base branch back!)

[Eric Wieser]

Johan Commelin said:

Yes, that sounds good to me

Done

[Eric Wieser]

Just this comment left of mine to resolve

[Eric Wieser]

I think someone else should:

• Do a final pass over the diff looking for accidental changes (implicit/explicit arguments, switches from n.succ to n+1). This would be a lot easier if someone could run mathport's oneshot.
• change the base commit
• merge

[Johan Commelin]

Can we just rewrite history, and make your current base commit part of the history of the original PR?

[Johan Commelin]

I think it makes a lot of sense to preserve that as part of the PR history

[Eric Wieser]

Changing the base doesn't change the history

[Eric Wieser]

And the current base commit is already in the history

[Eric Wieser]

Github is happy to show a diff, as in this comment; it's just not possible to comment on that diff, which is why I wanted to change the base. We could put that link the PR header

[Eric Wieser]

Johan Commelin said:

I think it makes a lot of sense to preserve that as part of the PR history

I do wonder if we want a mechanism such that we can do this for all PRs easily

[Johan Commelin]

Eric Wieser said:

Just this comment left of mine to resolve

@Mario Carneiro If this comment needs action, I'll make a seperate PR to fix it.

[Johan Commelin]

I've kicked the PR on the queue

[Johan Commelin]

Ooh snap. We need to update Mathlib.lean

[Eric Wieser]

There was also this comment but it's minor

[Johan Commelin]

mathlib4#1521 fixes the ofNat thing