classicalize

Stream: Is there code for X?

[Kyle Miller]

It seems the best practice is to write lemmas to be as permissive as possible with which decidable instances they accept. But within proofs this can cause issues when you use classical since it makes things harder to rewrite, etc., from there being multiple non-defeq instances around. I was wondering if there were something like a "classicalize" tactic that could replace all decidable instances in the goal or a hypothesis with their classical.prop_decidable counterparts.

(More generally, there could be a "canonicalize" tactic to take every term of a singleton type and replace it with a canonical term, perhaps as defined by inhabited.)

[Mario Carneiro]

this doesn't really work, because classical.prop_decidable et al is the least canonical kind of typeclass, it almost never agrees with other instances

[Mario Carneiro]

The general approach used by simp is to "canonicalize" typeclass instances, meaning that you replace whatever instance is there with the one that typeclass inference would find in the current context. This has a higher chance of being coherent with other choices

[Kyle Miller]

Ok, so as a followup, would it be possible to have a macro that could take a definition or lemma and classicalize it? An example use would be

rw (classicalize! foo)

to make a version of foo that would be compatible with a purely classical context.

[Eric Wieser]

The case I ran into recently was resolved by changing [decidable p] arguments in the lemma with {_ : decidable p} - the latter unified with the instance in the goal, while the former found a different instance. A tactic to generate modified lemmas like this on the fly might also help

[Mario Carneiro]

lemmas should be written in a context which is strictly more general than all uses, so I don't understand what you mean

[Mario Carneiro]

Ah, right that's a fault of the elaborator. The error it gives when unification and typeclass inference don't match isn't particularly useful for users

[Mario Carneiro]

I don't think generating lemmas on the fly is ever a good idea though

[Eric Wieser]

Does the elaborator use typeclass resolution to fill [] args in lambdas?

[Mario Carneiro]

in lambdas?

[Mario Carneiro]

it uses typeclass resolution to fill in [] args in lemmas

[Mario Carneiro]

this can later cause a unification error, but it doesn't know how to back this out so it just causes an error

[Eric Wieser]

I mean something like (\lam x [decidable (p x)], sorry) y

[Kyle Miller]

There are many cases where some of the decidable instances are computed from the others. I ran into a case with fintype.subtype recently -- this is almost always the correct instance, but in the classical context it was not correct and I had to use convert instead of a more straightforward rewrite.

[Eric Wieser]

Does the second argument I didn't pass get inferred?

[Mario Carneiro]

Yes it does

[Eric Wieser]

So a tactic could generate a wrapper lambda for a lemma with different argument binding rules?

[Mario Carneiro]

what's the example?

[Kyle Miller]

I think Eric is thinking about something I had in mind with classicalize!, which would be that it doesn't generate modified lemmas, but instead creates a lambda wrapper whose type is classicalized. (Edit: I hit enter right as Eric mentioned wrappers.)

[Mario Carneiro]

You can also insert (id _) for typeclass instance arguments to suppress inference

[Mario Carneiro]

but you have to know that they are going to be problematic

[Eric Wieser]

I was envisaging a weaker version of what Kyle suggests that just disables typeclass lookup for decidable args, without entering @/_ hell

[Mario Carneiro]

I mean literally (id _), you don't actually have to specify anything

[Mario Carneiro]

But I'd like to see kyle's example

[Eric Wieser]

rw (fixelab! bad_lemma x) instead of rw @bad_lemma _ _ _ (id _) _ x

[Mario Carneiro]

also it's not clear to me how this is better than convert

[Mario Carneiro]

you still have to use a tactic to fix things up

[Kyle Miller]

It's basic, but I just wanted to rewrite with common_neighbors_symm first, and it got me thinking:
https://github.com/leanprover-community/mathlib/blob/master/src/combinatorics/simple_graph/basic.lean#L384

[Eric Wieser]

I think the cause there is maybe lemmas with [decidable foo] which actually need [decidable bar] and derive the connection implicitly

[Eric Wieser]

Then you end up trying to apply the lemma to a case with a direct decidable bar instance not derived from a decidable foo (eg classical.dec), and it doesn't match

[Mario Carneiro]

(Kyle Miller) I don't think that's a very good example. You have to prove s = t -> fintype.card s = fintype.card t and that's a job for congr/convert

[Mario Carneiro]

rw just can't handle that because of the dependent argument

[Eric Wieser]

In your code that comes up all over the place where the lemmas assume G.adj is decidable but the statement requires neighbourset is decidable.

[Eric Wieser]

Maybe what I'm describing doesn't matter though

[Kyle Miller]

Yeah, it was a choice to focus only on G.adj being decidable, since we don't have any applications where it the decidability of G.neighbor_set would be any different. This is certainly the proximal issue, and I agree this isn't the best example.

[Mario Carneiro]

In your example the default instance should still go through the "indirect" route though, i.e. deriving decidability of G.neighbor_set from G.adj which is classical

[Mario Carneiro]

I think there is some value in a convert_rw which tries to rewrite given a lemma that only kind of matches the goal, with the difference being proved by convert / given as a subgoal, although I don't know how the interface would work there

[Eric Wieser]

If I write my own lemma about card (G.neighbor_set v w) with classical open, won't I get the direct instance and find myself unable to rewrite with Kyle's indirect lemma?

[Kyle Miller]

I still think it would be nice if there were some way to have a strong form of classical where decidability can be made to matter an epsilon amount. Maybe crw (for classical_rw) would be more manageable than a convert_rw.

[Mario Carneiro]

I don't think so; you have a lemma saying G.neighbor_set is decidable if G.adj is and that should take priority because the classical instance is the lowest priority

[Eric Wieser]

Thanks, I'd forgotten about priority

[Mario Carneiro]

@Kyle Miller the easiest way to achieve that is to take these decidability arguments out of the statements

[Mario Carneiro]

I tried using simp on your lemma and it applied docs#finset.filter_congr_decidable , which appears to be addressing your issue

[Kyle Miller]

This lemma isn't really my issue -- that lemma only reminded me how conflicting decidable instances occasionally show up and how it ideally is something you shouldn't have to think about in a classical context. What I'm hoping by starting this discussion is to maybe find low-cost ways that might reduce this friction in general. (With the Lean-is-a-videogame metaphor, matching up decidable instances inside proofs where it's pretty much irrelevant isn't good game design and isn't very satisfying. Can we improve the game loop here?)

[Mario Carneiro]

I mean convert does this already

[Mario Carneiro]

I really don't see what you're looking for

[Mario Carneiro]

It's not nothing, because the terms exist, there is some stuff happening

[Mario Carneiro]

if you want the terms to not exist you have to change the statements

[Mario Carneiro]

and then anyone who uses decidability or dec_trivial will not be able to use it

[Mario Carneiro]

maybe you don't, but finite graph theory does seem like the place where it would come up

[Mario Carneiro]

certainly when you are proving that the konigsberg graph has more than two vertices with odd degree it's nice to just dec_trivial that

[Kyle Miller]

With convert you have to set things up differently with how you write the tactic proof. It takes some restructuring in a way that makes you think about how there are decidable instances. If you are somehow able to make every decidable instance the classical.prop_decidable one automatically, then you wouldn't have to think about it.

I know you can do this all with convert, and I use convert. It's just worth thinking about how the user experience could be improved.

[Kyle Miller]

Mario Carneiro said:

if you want the terms to not exist you have to change the statements

You might say this word is where I disagree, since the system might be able to change them for you when you're in a proof. I'm willing to accept such a system might be too onerous to use in practice given the way Lean works.

[Mario Carneiro]

I mean the lemma has to be a different lemma about a different object

[Mario Carneiro]

But again, this is what convert does. In order for this to work you have to know the crazy instance you have and the other crazy instance you want, and rw only knows one side of the picture

[Mario Carneiro]

by the way, this proof works for your example:

lemma card_common_neighbors_le_degree_right [decidable_rel G.adj] (v w : V) :
  fintype.card (G.common_neighbors v w) ≤ G.degree w :=
begin
  simp_rw common_neighbors_symm G v w,
  convert G.card_common_neighbors_le_degree_left w v
end

[Kyle Miller]

I'm not sure what you're objecting to here. Here is what I'm thinking again just to put it in one place: it's convenient having lemmas that accept general decidable instances, but inside a proof you don't care what they are, so you could have a mechanism to transform the goal into the the classical form, and have another mechanism to wrap terms in a classical form. Now supposing that this can be made to work, rw and friends work fine, more or less.

[Kyle Miller]

And I could have sworn I had tried simp_rw and it didn't work...

[Kyle Miller]

Ah, it needs all three arguments. Hadn't considered that.

[Mario Carneiro]

I'm not sure if there is an option to stop simp_rw from applying its argument repeatedly

[Mario Carneiro]

This also works:

begin
  have := G.card_common_neighbors_le_degree_left w v,
  simp [common_neighbors_symm] at this ⊢, convert this
end

[Mario Carneiro]

simpa doesn't quite work because it needs the convert at the end

[Kyle Miller]

What's the mechanism that makes simp handle add_comm? Does it not apply to other commutativity lemmas?

[Mario Carneiro]

it puts a total order on terms and doesn't use commutativity-looking lemmas if they make the term go up in the order

[Mario Carneiro]

I think the definition of "commutativity-looking" is that the rhs is a substitution instance of the lhs

[Mario Carneiro]

simp can handle it just fine, I think simp_rw is just in a loop, which defeats simp's handling

[Kyle Miller]

I need to do simp only [G.common_neighbors_symm v] to get it to work, rather than simp only [G.common_neighbors_symm]

[Johan Commelin]

Mario Carneiro said:

simp can handle it just fine, I think simp_rw is just in a loop, which defeats simp's handling

If the term order were global, then this loops wouldn't be a problem either, right?

[Yury G. Kudryashov]

Properly written lemmas should work with classical out of the box.

[Yury G. Kudryashov]

My rule of thumb: require all the decidable instances that are used in the type (not in the proof) of a lemma/def.

[Yury G. Kudryashov]

I mean, even if I have [decidable_eq α] [decidable_eq β] but the definition/lemma uses [decidable_eq (α × β)], then it's better to add this as an argument.

[Yury G. Kudryashov]

This way lemma works both in classical and non-classical contexts.

[Eric Wieser]

Would a linter rule saying "every decidable term in a lemma statement must be a bound variable" work?

[Gabriel Ebner]

Don't we already have that linter?

[Eric Wieser]

docs#linter.decidable_classical only checks for unecessary decidable assumptions, not missing ones

[Kyle Miller]

Eric Wieser said:

Would a linter rule saying "every decidable term in a lemma statement must be a bound variable" work?

Would that include always being explicit about decidability even for types like nat? I remember there being a post where the nat decidable instances caused a conflict in a classical setting.

Previously I suggested a tactic/macro to classicalize instances in a term, but perhaps it would be more useful having a tactic called exactD, where what exactD t would do is generalize all the decidable instances in the type of t and then do exact. But I think it would be nice if there were some way when writing a lemma to indicate that you want the decidable instances to be generalized -- it's bookkeeping I can do, but it's nice leaving what's purely mechanical to computers.

[Eric Wieser]

I think maybe even for nat that would be a good idea

[Eric Wieser]

Although the only way to really find out is write the linter and see which of its suggestions look harmful

[Kyle Miller]

(Regarding the point I can hear Mario already saying that exactD is basically convert: the idea would be that this would let you work with terms without a goal or needing to specify the desired generalized type. Not arguing that it's definitely useful, but it seems better at least than the original ideas I was proposing.)

[Eric Wieser]

I had a go at making this linter in #6485