Rewritten instances

Stream: general

[Sebastian Ullrich]

I'm sure this is an issue that people here have to solve all the time, but I'm not aware of the current best practices, if they do exist:
When simplifying a term, an instance argument dependent on the term (e.g. the decidable_pred instance when rewriting the predicate of a list.filter) might also get rewritten. This can prevent further rewrites because the inferred and given instances don't match.

example (xs : list ℕ) : xs.filter (λ x, ¬true) = [] :=
by simp only [not_true]; rw filter_false

I can think of a few workarounds, but how do you usually deal with that?
/cc @Marc Huisinga

[Sebastian Ullrich]

Oh, bad example because @Chris Hughes actually did use non-instance implicit parameters in filter_false for exactly this reason I suppose. But all the other lemmas on filter are still using [decidable_pred p] parameters.

[Chris Hughes]

This is usually quite painful.

fintype is another class for which this comes up a lot. Mixing up classical and non classical decidable instances is also a problem.

Usually the way I deal with it, is to either use non-instance implicit parameters like with filter_false. Sometimes you can work around it using congr and convert, as in the following examples. This can obviously still be quite inconvenient though.

import data.list

open list

lemma filter_false' {α : Type*} (l : list α) : l.filter (λ _, false) = [] := filter_false _

example (xs : list ℕ) : xs.filter (λ x, ¬true) = [] :=
by simp only [not_true]; convert filter_false' xs

example (xs : list ℕ) : xs.filter (λ x, ¬true) = [] :=
by simp only [not_true]; rw ← filter_false' xs; congr

Another way of dealing with it is to just make the functions classical. The ring structure on polynomial now no longer requires a decidable_eq instance for reasons like this.

I don't think there's a nice way of dealing with this at the moment.

[Chris Hughes]

This stuff is actually a big barrier to finite group theory right now. There are a few congrs in group_theory/sylow.lean

[Sebastian Ullrich]

Thanks Chris. I believe the best solution would be for tactics like rw and simp to delay inferring class instance metavariables until after unification. But that should perhaps not be the default behavior, and of course would need to be changed in core. What one could write in mathlib is a tactic that re-infers all class instance arguments in the goal.

[Chris Hughes]

This delayed class instance already happens sometimes right? I'm not sure if this is a bug, but

example : (0 : ℕ) = @has_zero.zero ℕ ⟨1⟩ :=
begin
  refl, --goals accomplished
end

[Chris Hughes]

Works with rw as well

example : (1 : ℕ) = 1 + @has_zero.zero ℕ ⟨1⟩ :=
begin
  rw add_zero,
end

[Sebastian Ullrich]

Huh, curious. Unification inside the tactic stops before it discovers the type error. But as the proof term in the error message shows, it did not actually rewrite with add_zero :) . And the class instance trace shows that it did infer add_monoid nat

[Simon Hudon]

How big a change to core would that be? Maybe we should add that to 3.5.0 or 3.5.1

[Sebastian Ullrich]

I believe it would be a pretty big change, and I still don't know if it would actually be a good idea.