Zulip Chat Archive

Stream: general

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


view this post on Zulip 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?

view this post on Zulip Scott Morrison (Sep 25 2020 at 12:35):

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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 12:41):

LGTM

view this post on Zulip Reid Barton (Sep 25 2020 at 12:46):

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

view this post on Zulip Eric Wieser (Sep 25 2020 at 13:00):

Presumably I should prefer the pairwise_nil spelling for consistency?

view this post on Zulip Eric Wieser (Sep 25 2020 at 13:04):

Ah, nevermind, I'll just match chain

view this post on Zulip Eric Wieser (Sep 25 2020 at 13:07):

#4254

view this post on Zulip 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₃?

view this post on Zulip Mario Carneiro (Sep 25 2020 at 15:52):

simp should do that?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 15:54):

Oh, you need a simp lemma for forall_mem

view this post on Zulip Mario Carneiro (Sep 25 2020 at 15:54):

in theory forall_mem_cons should trigger

view this post on Zulip Eric Wieser (Sep 25 2020 at 15:55):

It seems that list.mem_cons_iff triggers instead

view this post on Zulip Eric Wieser (Sep 25 2020 at 15:56):

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

view this post on Zulip 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

view this post on Zulip Eric Wieser (Sep 25 2020 at 15:57):

list.pairwise.nil will be included automatically shortly

view this post on Zulip Eric Wieser (Sep 25 2020 at 15:57):

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

view this post on Zulip Mario Carneiro (Sep 25 2020 at 15:58):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 25 2020 at 15:59):

yes

view this post on Zulip Mario Carneiro (Sep 25 2020 at 15:59):

it's not a simp lemma though

view this post on Zulip Eric Wieser (Sep 25 2020 at 15:59):

Oh, that's what I missed

view this post on Zulip Eric Wieser (Sep 25 2020 at 15:59):

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

view this post on Zulip 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