Redundant hypotheses in `Data.List.Cycle`

Stream: mathlib4

[Snir Broshi]

Data.List.Cycle contains a lot of theorems with redundant hypotheses:

• docs#List.next_cons_cons_eq' has x = y and x ∈ y :: z :: l
• docs#List.next_cons_cons_eq has x ∈ x :: z :: l
• docs#List.next_ne_head_ne_getLast has x ∈ l and x ∈ y :: l
• docs#List.next_cons_concat has x ∈ y :: l ++ [x] (although it does have a proof as a default value)
• docs#List.next_getLast_cons has x ∈ l and x ∈ y :: l (and also x ≠ y)
• docs#List.prev_getLast_cons' has x = y and x ∈ y :: l
• docs#List.prev_getLast_cons has x ∈ x :: l
• docs#List.prev_cons_cons_eq' has x = y and x ∈ y :: z :: l
• docs#List.prev_cons_cons_eq has x ∈ x :: z :: l
• docs#List.prev_cons_cons_of_ne' has x = z and x ∈ y :: z :: l
• docs#List.prev_cons_cons_of_ne has x ∈ y :: x :: l

I believe most of them exist because the statement itself needs a proof of them, and while they trivially follow from the other hypotheses they make the statement much longer. E.g.

theorem next_cons_cons_eq (z : α) : next (x :: z :: l) x (mem_cons.mpr (.inl rfl)) = z := ...

vs.

theorem next_cons_cons_eq (z : α) (h : x ∈ x :: z :: l) : next (x :: z :: l) x h = z :=

I think we should remove the redundancy and fill in the proofs. Many of them are solved by simp (such as the example above) so they don't take up that much space, but more importantly I think it burdens the caller to provide more proofs to use a theorem which shouldn't require such a proof.

What are your thoughts on this? How common is it across Mathlib to add a redundant hypothesis to simplify a statement? Is the default parameter approach a best-of-both-worlds? Or perhaps a have inside the theorem statement?

[Aaron Liu]

but it makes unifying them easier

[Snir Broshi]

unifying who?

[Aaron Liu]

I guess unifying the conclusion of the theorem?

[Aaron Liu]

I'm not looking at the statements right now so this is just a guess

[Snir Broshi]

From my experience proof irrelevance applies when unifying, so replacing a proof variable by a proof term shouldn't make a difference for unification

[Yakov Pechersky]

Supplying the hypothesis as part of the arguments to the lemma vs directly in the statement allows for rw to work with side goals.

[Yakov Pechersky]

If you inline the proof, then you don't match syntactically

[Snir Broshi]

rw works even when the proofs differ

[Snir Broshi]

Although if we're talking about rewriting the parts which aren't the proofs, then a variable proof might save a few "motive is not type correct" errors, but that'll just help the theorem proof and won't help the user at all. So again I don't see an advantage

[Antoine Chambert-Loir]

Snir Broshi said:

rw works even when the proofs differ

Because the proofs don't differ.

[Johan Commelin]

@Snir Broshi I advocate to not drop the x = y hyps. Those lift a defeq to a propeq, which can be genuinely useful in applications.
The other types of hyps, I don't mind dropping.

[Snir Broshi]

Johan Commelin said:

Those lift a defeq to a propeq, which can be genuinely useful in applications.

I agree they're useful, but doesn't the convert tactic solve that problem already?

[Johan Commelin]

It's a bit of a hammer though, and you have to give up any form of fine-grained control over defeqs when you use it.

[Kevin Buzzard]

convert can also lead to hard-to-maintain code, because any changes in definitions can completely change the behaviour of the tactic.