## Stream: general

### Topic: Should list.pairwise.nil be marked simp

#### Eric Wieser (Sep 25 2020 at 12:15):

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 (Sep 25 2020 at 12:35):

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

LGTM

#### Reid Barton (Sep 25 2020 at 12:46):

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

#### Eric Wieser (Sep 25 2020 at 13:00):

Presumably I should prefer the pairwise_nil spelling for consistency?

#### Eric Wieser (Sep 25 2020 at 13:04):

Ah, nevermind, I'll just match chain

#4254

#### Eric Wieser (Sep 25 2020 at 15:52):

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 (Sep 25 2020 at 15:52):

simp should do that?

#### Eric Wieser (Sep 25 2020 at 15:54):

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

#### Mario Carneiro (Sep 25 2020 at 15:54):

Oh, you need a simp lemma for forall_mem

#### Mario Carneiro (Sep 25 2020 at 15:54):

in theory forall_mem_cons should trigger

#### Eric Wieser (Sep 25 2020 at 15:55):

It seems that list.mem_cons_iff triggers instead

#### Eric Wieser (Sep 25 2020 at 15:56):

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

#### Mario Carneiro (Sep 25 2020 at 15:56):

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 (Sep 25 2020 at 15:57):

list.pairwise.nil will be included automatically shortly

#### Eric Wieser (Sep 25 2020 at 15:57):

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

#### Mario Carneiro (Sep 25 2020 at 15:58):

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

#### Eric Wieser (Sep 25 2020 at 15:59):

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

yes

#### Mario Carneiro (Sep 25 2020 at 15:59):

it's not a simp lemma though

#### Eric Wieser (Sep 25 2020 at 15:59):

Oh, that's what I missed

#### Eric Wieser (Sep 25 2020 at 15:59):

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

#### Mario Carneiro (Sep 25 2020 at 16:00):

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

Last updated: May 11 2021 at 00:31 UTC