bugs and issues in the Data.List.Infix port

Stream: mathlib4

[Henrik Böving]

There are two bugs in meta utilities in the Data.List.Infix port.

The first is that the alias:

alias instDecidableOr ← Or.decidable

in Mathlib.Init.Logic seems to produce Or.decidable as a noncomputable instance even though the instDecidableOr is very much computable. This makes the following instance:

instance decidableSuffix [DecidableEq α] : ∀ l₁ l₂ : List α, Decidable (l₁ <:+ l₂)
  | [], l₂ => isTrue ⟨l₂, append_nil _⟩
  | a :: l₁, [] => isFalse <| mt (Sublist.length_le ∘ isSuffix.sublist) (by simp)
  | l₁, b :: l₂ =>
    @decidable_of_decidable_of_iff _ _ (@Or.decidable _ _ _ (l₁.decidableSuffix l₂)) suffix_cons_iff.symm
termination_by decidableSuffix l₁ l₂ => (l₁, l₂)

Or the following simpler example instance:

instance foo {a b : Prop }[Decidable a] [Decidable b] : Decidable (a ∨ b) :=
  Or.decidable

Demanded to be marked as noncomputable, just using the instDecidableOr does work out though.

Furthermore the file contains the alias:

theorem eq_nil_of_infix_nil (h : l <:+: []) : l = [] :=
  eq_nil_of_sublist_nil h.sublist
#align list.eq_nil_of_infix_nil List.eq_nil_of_infix_nil

@[simp]
theorem infix_nil_iff : l <:+: [] ↔ l = [] :=
  ⟨fun h => eq_nil_of_sublist_nil h.sublist, fun h => h ▸ infix_rfl⟩
#align list.infix_nil_iff List.infix_nil_iff

alias infix_nil_iff ↔ eq_nil_of_infix_nil _

Which produces:

(kernel) constant has already been declared 'List.eq_nil_of_infix_nil'

Which is understandable I guess? I'm not quite sure why the two things are aliased anyways? Shall I just delete this alias or am I understanding the purpose of it wrong? For some reason this does not seem to error in Lean 3.

And apart from that the question with shall I use List.get instead of List.nthLe like the linter tells me? Or do we want to keep those theorems on nthLe around for now?

[Floris van Doorn]

In Lean 3, alias silently did nothing if the declaration already existed: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/alias.20silently.20succeeds.20when.20name.20already.20exists

[Henrik Böving]

Based on marios answer it sounds like I should basically delete the alias then right?

[Floris van Doorn]

Yes, you can delete the alias.

[Floris van Doorn]

The issue that alias doesn't generate computable definitions hasn't been solved yet, so in !4#1455 I used def instead of alias for Or.decidable and similar instances.