Zulip Chat Archive

Stream: general

Topic: Rewritten instances


Sebastian Ullrich (Sep 11 2019 at 16:34):

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 (Sep 11 2019 at 16:50):

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 (Sep 12 2019 at 07:52):

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 (Sep 12 2019 at 08:09):

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 (Sep 12 2019 at 08:32):

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 (Sep 12 2019 at 08:35):

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 (Sep 12 2019 at 08:36):

Works with rw as well

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

Sebastian Ullrich (Sep 12 2019 at 08:52):

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 (Sep 12 2019 at 16:46):

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

Sebastian Ullrich (Sep 12 2019 at 21:48):

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


Last updated: Dec 20 2023 at 11:08 UTC