Data.List.Func

Stream: mathlib4

[Rémi Bottinelli]

I'm giving a go at porting Data.List.Func (not claiming the file), and came upon two things which I'm wondering about:

• mathport translated a mem_cons_iff to mem_cons_iff which doesn't exist anymore, but now mem_cons replaces it. Is that a sign of a missing #align or not at all?
• The signature of eq_get_of_mem looks wrong to me: I think this random d is meant to be interpreted as the "default value", but shouldn't get be called like @get _ \<d\> for this to make sense?

[Ruben Van de Velde]

eq_get_of_mem was broken in https://github.com/leanprover-community/mathlib/pull/827/commits/3826b52128110b8fdf7a89c41075bd3d8d797f32

[Ruben Van de Velde]

The forall d should just be removed

[Rémi Bottinelli]

and the align kept? or is changing the function's signature not cause for dropping an align?

[Rémi Bottinelli]

OK, just sharing my progress here in case someone wants to have a stab at it before I finish my port.

[Ruben Van de Velde]

Mm, probably #noalign it - I would suggest fixing in mathlib3, but it's literally only used once in the same file

[Ruben Van de Velde]

So not worth spending time on, I think

[Ruben Van de Velde]

I'm not sure if people would prefer fixing it in the port or leave it with the weird signature and a note in a comment

[Rémi Bottinelli]

OK, I've got it typechecking in its entirety, but #lint is unhappy.

The main cause for errors was that I had to provide instances of Inhabited \alpha manually when working, say, with AdditiveMonoid \alpha. What's the cause for that?

[Rémi Bottinelli]

Mmh, that seemed to be a problem with the mathlib 3 code already:

@[simp] lemma get_neg [add_group α] {k : ℕ} {as : list α} :
  @get α ⟨0⟩ k (neg as) = -(@get α ⟨0⟩ k as) :=
by {unfold neg, rw (@get_map' α α ⟨0⟩), apply neg_zero}

Why doesn't [inhabited α] follow here?

[Rémi Bottinelli]

PR here: https://github.com/leanprover-community/mathlib4/pull/1048

[Rémi Bottinelli]

I was wondering: when porting, are we encouraged to simplify/bikeshed/golf proofs down, or should we stick to being as close to the mathport source as possible?

[Kevin Buzzard]

I think it's worth flagging if a proof doesn't work and needs to be expanded, with a porting note. If you just feel like golfing and your new proof is definitely not something which takes 10x as long to compile, then why not go for it. I'm not sure it's _encouraged_ though! What's encouraged is that we get through this job ASAP :-)

[James Gallicchio]

Rémi Bottinelli|461830 said:

• mathport translated a mem_cons_iff to mem_cons_iff which doesn't exist anymore, but now mem_cons replaces it. Is that a sign of a missing #align or not at all?

The mem_cons_iff missing align strikes again, this time in Data.List.Permutation :)

It was previously declared in init: https://github.com/leanprover-community/lean/blob/master/library/init/data/list/lemmas.lean#L100

Where should I put an #align?

[Yaël Dillies]

Mathlib.Init.Data.List.Lemmas