Case-bashing `list.pairwise` with `simp`

Stream: general

[Eric Wieser]

Could this be a simp lemma?

lemma forall_or_imp {α : Type} {p : α → Prop} {q : α → Prop} {a : α} :
  (∀ (x : α), x = a ∨ q x → p x) ↔ p a ∧ ∀ (x : α), q x → p x :=
begin
  split; intros,

  have ra := a_1 a,
  simp at ra,
  exact ⟨ra, λ x qx, a_1 x (or.inr qx)⟩,
  cases a_2,
  cases a_1,
  { rw a_2, assumption },
  { cases a_1, solve_by_elim }
end

[Reid Barton]

try simp [or_imp_distrib]?

[Eric Wieser]

I think I need to take a step back here. Why is simp producing a less simple result than simp [-list.mem_cons_iff]?

attribute [simp] list.pairwise.nil

/--
Fails with:
⊢ (R i₁ i₂ ∧ R i₁ i₃) ∧ R i₂ i₃ ↔
    (∀ (a' : α), a' = i₂ ∨ a' = i₃ → R i₁ a') ∧ R i₂ i₃ -/
example {α : Type} {R : α → α → Prop} {i₁ i₂ i₃ : α} : (R i₁ i₂ ∧ R i₁ i₃) ∧ R i₂ i₃ ↔ [i₁, i₂, i₃].pairwise R :=
by simp

/-- succeeds, list.mem_cons_iff would not match the final goal anyway -/
example {α : Type} {R : α → α → Prop} {i₁ i₂ i₃ : α} : (R i₁ i₂ ∧ R i₁ i₃) ∧ R i₂ i₃ ↔ [i₁, i₂, i₃].pairwise R :=
by simp [-list.mem_cons_iff]

[Eric Wieser]

squeeze_simp reveals the difference is

 example {α : Type} {R : α → α → Prop} {i₁ i₂ i₃ : α} : (R i₁ i₂ ∧ R i₁ i₃) ∧ R i₂ i₃ ↔ [i₁, i₂, i₃].pairwise R :=
 by {
   simp only [list.not_mem_nil, and_true, forall_prop_of_false, list.pairwise.nil, forall_eq, not_false_iff, list.pairwise_cons, forall_true_iff,
-      list.mem_cons_iff, list.mem_singleton, and_self],
+      list.ball_cons],
 }

Is list.ball_cons somehow lower priority than list.mem_cons_iff?

[Reid Barton]

just a sanity check--forall_mem_cons is the same as ball_cons modulo binder types and being a simp lemma or not, right?

[Eric Wieser]

Let's check...: docs#list.forall_mem_cons, docs#list.ball_cons

[Eric Wieser]

It looks like the problem is that list.ball_cons is a simp lemma whose LHS is not in simp-normal form (it can be rewritten by docs#list.mem_cons_iff, which is another simp lemma)

[Eric Wieser]

Which presumably the linter misses because it's part of core and not mathlib?

[Reid Barton]

I'm a bit confused because I thought that simp generally operates from the outside in, so it should apply list.ball_cons before list.mem_cons_iff anyways

[Floris van Doorn]

I'm quite sure simp operates from the inside out.

[Floris van Doorn]

Yes, see e.g. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Simp.20normal.20form/near/188829903

[Eric Wieser]

So is the conclusion is that the lean core simp lemma is bad?

[Reid Barton]

Hmm, I see. Well, in any case this ordering is not something that can be affected by priorities.

[Eric Wieser]

I think the thing to do is:

• Remove the bad simp lemma from core
• Add the simp lemma I have above so that the lemma in core is just by simp anyway.

[Eric Wieser]

Will try next week

[Floris van Doorn]

I ran the simp_nf linter on core, here is the output:
https://github.com/leanprover-community/mathlib/runs/1167546135
I couldn't find the offending lemma in there (but maybe it's one of the other simp linters that finds it?)
If you are fixing core, it would be great if you also fix some of the other lemmas caught by the linter.

[Floris van Doorn]

I'm now running other linters also on core (but not the ones that produce output in mathlib): https://github.com/leanprover-community/mathlib/runs/1168317987

[Bryan Gin-ge Chen]

Looks like you'll want to remove the -T100000 here https://github.com/leanprover-community/mathlib/blob/master/.github/workflows/build.yml#L54

[Mario Carneiro]

I don't think we should remove any involved simp lemmas

[Mario Carneiro]

It's not ideal, but I think it is better to have a non-confluent set of simp lemmas than to have a weak set

[Mario Carneiro]

the real problem here is that we use \forall x \in l, p x to represent the operator one might write as all p l

[Mario Carneiro]

This operator is in some sense dual to list.mem, defined using and instead of or

[Floris van Doorn]

The simp_nfdoes not check confluence, but whether other simp lemmas first simplify a subexpression of the LHS before this simp lemma has a chance of firing. Therefore, all positives of the simp_nf lemmas are simp lemmas that never fire. See https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%20form

[Eric Wieser]

Never fire unless the overlapping lemma is excluded via -, as in my example

[Mario Carneiro]

@Floris van Doorn I'm not exactly sure who you are responding to, but it is not true that list.mem_cons_iff' never fires. It is non-confluent but the LHS is in simp normal form

[Mario Carneiro]

the problem is that while the LHS of list.mem_cons_iff' itself is in simp normal form, there are instantiations of the LHS (with simp normal terms) that are not in simp normal form

[Reid Barton]

I think list.ball_cons is the lemma in question

[Reid Barton]

 #print list.bex_cons /- Left-hand side simplifies from
  ∃ (x : α) (H : x ∈ a :: l), p x
to
  ∃ (x : α), (x = a ∨ x ∈ l) ∧ p x
using
  [exists_prop, list.mem_cons_iff]
Try to change the left-hand side to the simplified term!
 -/
#print list.ball_cons /- simp can prove this:
  by simp only [list.mem_cons_iff, list.forall_mem_cons']
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
 -/

[Mario Carneiro]

oh, that's just list.mem_cons_iff by another name

[Reid Barton]

maybe the "simp can prove this" linter caught it first?

[Reid Barton]

Exactly

[Eric Wieser]

Mario Carneiro said:

oh, that's just list.mem_cons_iff by another name

Can we remove one of the names to make this less confusing?

[Mario Carneiro]

To be fair, this is a cross-repo simp incoherence, so it's not like we can point a finger at any particular lemma

[Mario Carneiro]

we could unset the simp attribute from those lemmas in data.list.basic

[Eric Wieser]

That's a good idea- what's the syntax for removing an attribute?

[Mario Carneiro]

attribute [-simp] list.ball_cons

[Mario Carneiro]

actually you might not be able to

[Mario Carneiro]

I don't think that works for non-local unsets

[Eric Wieser]

Reid Barton said:

just a sanity check--forall_mem_cons is the same as ball_cons modulo binder types and being a simp lemma or not, right?

Opened #4279 to make this obvious from the source code

[Eric Wieser]

Eric Wieser said:

Could this be a simp lemma?

@[simp]
lemma forall_eq_or_imp {α : Type} {p : α → Prop} {q : α → Prop} {a : α} :
  (∀ (x : α), x = a ∨ q x → p x) ↔ p a ∧ ∀ (x : α), q x → p x := sorry

Opened #4281 to find out.

[Floris van Doorn]

Mario Carneiro said:

Floris van Doorn I'm not exactly sure who you are responding to, but it is not true that list.mem_cons_iff' never fires. It is non-confluent but the LHS is in simp normal form

I was responding to you, under the assumption you were responding to me. :-)
I agree that we should not remove simp lemmas just to keep things confluent, but we should remove simp lemmas in core flagged by the linter.

[Eric Wieser]

What's the right way to deal with core having a simp lemma from A -> C and mathlib introducing two new ones from A -> B and B -> C? Put both new lemmas in core? Remove the annotation retroactively in mathlib?