Zulip Chat Archive

Stream: general

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


Eric Wieser (Sep 25 2020 at 16:15):

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 (Sep 25 2020 at 16:18):

try simp [or_imp_distrib]?

Eric Wieser (Sep 25 2020 at 16:21):

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 (Sep 25 2020 at 16:26):

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 (Sep 25 2020 at 16:48):

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 (Sep 25 2020 at 16:49):

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

Eric Wieser (Sep 25 2020 at 16:51):

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 (Sep 25 2020 at 16:51):

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

Reid Barton (Sep 25 2020 at 16:54):

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 (Sep 25 2020 at 18:03):

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

Floris van Doorn (Sep 25 2020 at 18:04):

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

Eric Wieser (Sep 25 2020 at 19:49):

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

Reid Barton (Sep 25 2020 at 19:54):

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

Eric Wieser (Sep 25 2020 at 21:05):

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 (Sep 25 2020 at 21:06):

Will try next week

Floris van Doorn (Sep 25 2020 at 22:48):

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 (Sep 25 2020 at 22:48):

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 (Sep 25 2020 at 22:54):

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 (Sep 25 2020 at 23:47):

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

Mario Carneiro (Sep 25 2020 at 23:48):

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 (Sep 25 2020 at 23:48):

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 (Sep 25 2020 at 23:49):

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

Floris van Doorn (Sep 26 2020 at 08:11):

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 (Sep 26 2020 at 09:16):

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

Mario Carneiro (Sep 26 2020 at 12:53):

@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 (Sep 26 2020 at 12:54):

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 (Sep 26 2020 at 12:55):

I think list.ball_cons is the lemma in question

Reid Barton (Sep 26 2020 at 12:56):

 #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 (Sep 26 2020 at 12:56):

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

Reid Barton (Sep 26 2020 at 12:56):

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

Reid Barton (Sep 26 2020 at 12:57):

Exactly

Eric Wieser (Sep 26 2020 at 12:58):

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 (Sep 26 2020 at 13:00):

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 (Sep 26 2020 at 13:00):

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

Eric Wieser (Sep 26 2020 at 13:01):

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

Mario Carneiro (Sep 26 2020 at 13:01):

attribute [-simp] list.ball_cons

Mario Carneiro (Sep 26 2020 at 13:02):

actually you might not be able to

Mario Carneiro (Sep 26 2020 at 13:02):

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

Eric Wieser (Sep 26 2020 at 13:11):

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 (Sep 26 2020 at 13:24):

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 (Sep 26 2020 at 20:56):

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 (Sep 26 2020 at 21:35):

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?


Last updated: Dec 20 2023 at 11:08 UTC