Should `list.pairwise.nil` be marked simp

Stream: general

[Eric Wieser]

This proof doesn't work today, because it gets stuck on list.pairwise ne nil:

import data.list.pairwise

example {α : Type} {i₁ i₂ i₃ : α} (hi₁₂ : i₁ ≠ i₂) (hi₁₃ : i₁ ≠ i₃) (hi₂₃ : i₂ ≠ i₃) : [i₁, i₂, i₃].pairwise (≠) :=
by tidy

I can fix it either with attribute [simp] list.pairwise.nil or

@[simp] lemma list.pairwise_nil {α : Type*} {R : α → α → Prop} : [].pairwise R := list.pairwise.nil

noting that the latter is consistent with docs#list.pairwise_cons.

Should one of these be PR'd?

[Scott Morrison]

Yes please. I ran into the same problem just recently, but didn't fix it.

[Mario Carneiro]

LGTM

[Reid Barton]

I note there is attribute [simp] chain.nil a bit lower in data.list.defs.

[Eric Wieser]

Presumably I should prefer the pairwise_nil spelling for consistency?

[Eric Wieser]

Ah, nevermind, I'll just match chain

[Eric Wieser]

#4254

[Eric Wieser]

As a follow-up question - if I didn't have hi₁₂ etc in the above example, is there some case-bash tactic I can use to convert a goal of [i₁, i₂, i₃].pairwise R into R i₁ i₂ ∧ R i₁ i₃ ∧ R i₂ i₃?

[Mario Carneiro]

simp should do that?

[Eric Wieser]

simp doesn't know I want it in that form, and gives me a slightly ugly forall

[Mario Carneiro]

Oh, you need a simp lemma for forall_mem

[Mario Carneiro]

in theory forall_mem_cons should trigger

[Eric Wieser]

It seems that list.mem_cons_iff triggers instead

[Eric Wieser]

simp [-list.mem_cons_iff], gives me what I want

[Mario Carneiro]

example {α : Type} (R) {i₁ i₂ i₃ : α} : [i₁, i₂, i₃].pairwise R :=
by simp [-list.mem_cons_iff, list.pairwise.nil]

this works well

[Eric Wieser]

list.pairwise.nil will be included automatically shortly

[Eric Wieser]

Can we teach simp to match mem_cons_iff with lower priority that forall_mem_cons?

[Mario Carneiro]

I don't think so, because it matches in a subterm

[Eric Wieser]

Doesn't that mean the LHS of @list.forall_mem_cons is not in simp-normal form?

[Mario Carneiro]

yes

[Mario Carneiro]

it's not a simp lemma though

[Eric Wieser]

Oh, that's what I missed

[Eric Wieser]

How do I ask lean to show me annotations on a lemma?

[Mario Carneiro]

the "fixed" version is list.forall_mem_cons' but that's also no good for this example