Help with build fail

Stream: general

[Adam Topaz]

I'm trying to diagnose why the changes in the following commit cause a failure when building mathlib:
https://github.com/leanprover-community/mathlib/commit/28d057cf6be53bc816e0cb56176589cf720944d0

The error appears in the proof of src#multiset.ndunion_le

[Adam Topaz]

Any help / suggestions would be greatly appreciated!

[Kevin Buzzard]

On that branch, one can hack finset_ops.lean a bit:

...(line 132)
theorem ndunion_le_add (s t : multiset α) : ndunion s t ≤ s + t :=
quotient.induction_on₂ s t $ λ l₁ l₂, (union_sublist_append _ _).subperm

-- hack starts here

-- remove instances which are breaking stuff
local attribute [-instance] semilattice_sup.to_directed_order
local attribute [-instance] semilattice_inf.to_codirected_order

--set_option trace.simplify.rewrite true
-- take proof apart
theorem ndunion_le {s t u : multiset α} : ndunion s t ≤ u ↔ s ⊆ u ∧ t ≤ u :=
multiset.induction_on s (by simp)
(begin
  intros a s hs,
  suffices : ndinsert a (s.ndunion t) ≤ u ↔ (a ∈ u ∧ s ⊆ u) ∧ t ≤ u,
    simpa,
  rw [ndinsert_le, hs],
  -- ⊢ (s ⊆ u ∧ t ≤ u) ∧ a ∈ u ↔ (a ∈ u ∧ s ⊆ u) ∧ t ≤ u
  -- goal now pure logic
  simp [and_comm, and.left_comm], -- succeeds
end)

The issue seems to be using simp [and_comm, and.left_comm] to solve the pure logic statement (s ⊆ u ∧ t ≤ u) ∧ a ∈ u ↔ (a ∈ u ∧ s ⊆ u) ∧ t ≤ u.

With your branch's instances removed with those local attribute [-instance] lines, using trace.simplify.rewrite true you can see that simp finds the following proof of the logic statement:

0. [simplify.rewrite] [and_comm]: (s ⊆ u ∧ t ≤ u) ∧ a ∈ u ==> a ∈ u ∧ s ⊆ u ∧ t ≤ u
0. [simplify.rewrite] [and.left_comm]: a ∈ u ∧ s ⊆ u ∧ t ≤ u ==> s ⊆ u ∧ a ∈ u ∧ t ≤ u
0. [simplify.rewrite] [and_comm]: a ∈ u ∧ s ⊆ u ==> s ⊆ u ∧ a ∈ u
0. [simplify.rewrite] [and_comm]: (s ⊆ u ∧ a ∈ u) ∧ t ≤ u ==> t ≤ u ∧ s ⊆ u ∧ a ∈ u
0. [simplify.rewrite] [and.left_comm]: t ≤ u ∧ s ⊆ u ∧ a ∈ u ==> s ⊆ u ∧ t ≤ u ∧ a ∈ u
0. [simplify.rewrite] [and_comm]: t ≤ u ∧ a ∈ u ==> a ∈ u ∧ t ≤ u
0. [simplify.rewrite] [and.congr_left_iff]: s ⊆ u ∧ a ∈ u ∧ t ≤ u ↔ s ⊆ u ∧ a ∈ u ∧ t ≤ u ==> a ∈ u ∧ t ≤ u → (s ⊆ u ↔ s ⊆ u)
0. [simplify.rewrite] [iff_self]: s ⊆ u ↔ s ⊆ u ==> true
0. [simplify.rewrite] [and_imp]: a ∈ u ∧ t ≤ u → true ==> a ∈ u → t ≤ u → true
0. [simplify.rewrite] [implies_true_iff]: t ≤ u → true ==> true
0. [simplify.rewrite] [implies_true_iff]: a ∈ u → true ==> true

Now if we comment out one of the local attribute [-instance] lines (i.e. add one of your new instances), simp gives up earlier in the process: it does this

0. [simplify.rewrite] [and_comm]: (s ⊆ u ∧ t ≤ u) ∧ a ∈ u ==> a ∈ u ∧ s ⊆ u ∧ t ≤ u
0. [simplify.rewrite] [and.left_comm]: a ∈ u ∧ s ⊆ u ∧ t ≤ u ==> s ⊆ u ∧ a ∈ u ∧ t ≤ u
0. [simplify.rewrite] [and_comm]: a ∈ u ∧ s ⊆ u ==> s ⊆ u ∧ a ∈ u

⊢ s ⊆ u ∧ a ∈ u ∧ t ≤ u ↔ (s ⊆ u ∧ a ∈ u) ∧ t ≤ u

and then it stops.

So that's why it's breaking, and as for why the behaviour of simp is changing I'll have to defer to someone else.

[Kevin Buzzard]

PS I cannot minimise any further. Stuff like

example (α : Type*) (s t u : multiset α) (a : α) :
  (s ⊆ u ∧ t ≤ u) ∧ a ∈ u ↔ (a ∈ u ∧ s ⊆ u) ∧ t ≤ u :=
by simp [and_comm, and.left_comm]

works fine with or without the new instances: simp continues along the path above and solves the goal.

[Kevin Buzzard]

Aah, I tell a lie! Decidable equality on alpha is the key.

local attribute [-instance] semilattice_sup.to_directed_order
local attribute [-instance] semilattice_inf.to_codirected_order

example (α : Type*) [decidable_eq α] (s t u : multiset α) (a : α) :
  (s ⊆ u ∧ t ≤ u) ∧ a ∈ u ↔ (a ∈ u ∧ s ⊆ u) ∧ t ≤ u :=
by simp [and_comm, and.left_comm]

This works (on the branch, in finset_ops.lean), but commenting out the -instance lines (i.e. putting the new instances back) makes simp fail.

[Kevin Buzzard]

Here's a version which works on master. The instance changes the behaviour of simp (and in particular stops the example from working). With the instance, simp does nothing. Without it, it solves the goal.

import data.multiset

universe u

@[priority 100]  -- see Note [lower instance priority]
instance semilattice_sup.to_directed_order (α) [semilattice_sup α] : directed_order α :=
⟨λ i j, ⟨i ⊔ j, le_sup_left, le_sup_right⟩⟩

set_option trace.simplify.rewrite true

example (α : Type*) [decidable_eq α] (s t u : multiset α) (a : α) :
  s ⊆ u ∧ a ∈ u ∧ t ≤ u ↔ (s ⊆ u ∧ a ∈ u) ∧ t ≤ u :=
by simp [and_comm, and.left_comm]

[Adam Topaz]

Thanks @Kevin Buzzard ! this is really helpful. Just to add to the mystery, the simp fails in this code as well:

import data.multiset

universe u

@[priority 0]  -- see Note [lower instance priority]
instance semilattice_sup.to_directed_order (α) [semilattice_sup α] : directed_order α :=
⟨λ i j, ⟨i ⊔ j, le_sup_left, le_sup_right⟩⟩

set_option trace.simplify.rewrite true

example (α : Type*) [decidable_eq α] (s t u : multiset α) (a : α) :
  s ⊆ u ∧ a ∈ u ∧ t ≤ u ↔ (s ⊆ u ∧ a ∈ u) ∧ t ≤ u :=
by simp [and_comm, and.left_comm]

[Adam Topaz]

Well, I wanted to add this codirected_order class and associated instances as part of #7982 but more and more similar issues kept popping up.

So I've reworked the code for #7982 to (naturally) avoid these instances for now. Nevertheless, I think we should add codirected_order and the associated instances as some point in the future.

Ping @Kyle Miller

[Kyle Miller]

With a small_category instance from a codirected_order, would it conflict with the small_category instance that directed_order gives?

[Adam Topaz]

The category instance comes from the preorder structure, and I think the two would be defeq already at the level of preorders, right?