Zulip Chat Archive

Stream: Is there code for X?

Topic: classicalize


view this post on Zulip Kyle Miller (Jan 29 2021 at 22:55):

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.)

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:09):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:10):

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

view this post on Zulip Kyle Miller (Jan 29 2021 at 23:26):

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.

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:29):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:29):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:30):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:31):

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

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:31):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:32):

in lambdas?

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:32):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:33):

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

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:33):

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

view this post on Zulip Kyle Miller (Jan 29 2021 at 23:33):

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.

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:33):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:33):

Yes it does

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:34):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:34):

what's the example?

view this post on Zulip Kyle Miller (Jan 29 2021 at 23:34):

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.)

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:35):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:35):

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

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:36):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:36):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:37):

But I'd like to see kyle's example

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:38):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:38):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:38):

you still have to use a tactic to fix things up

view this post on Zulip Kyle Miller (Jan 29 2021 at 23:38):

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

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:42):

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

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:43):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:44):

(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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:44):

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

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:45):

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.

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:45):

Maybe what I'm describing doesn't matter though

view this post on Zulip Kyle Miller (Jan 29 2021 at 23:46):

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.

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:47):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:49):

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

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:49):

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?

view this post on Zulip Kyle Miller (Jan 29 2021 at 23:50):

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.

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:50):

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

view this post on Zulip Eric Wieser (Jan 29 2021 at 23:51):

Thanks, I'd forgotten about priority

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:51):

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

view this post on Zulip Mario Carneiro (Jan 29 2021 at 23:55):

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

view this post on Zulip Kyle Miller (Jan 30 2021 at 00:08):

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?)

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:09):

I mean convert does this already

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:09):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:10):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:10):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:11):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:11):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:12):

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

view this post on Zulip Kyle Miller (Jan 30 2021 at 00:13):

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.

view this post on Zulip Kyle Miller (Jan 30 2021 at 00:16):

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.

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:16):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:21):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:27):

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

view this post on Zulip Kyle Miller (Jan 30 2021 at 00:29):

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.

view this post on Zulip Kyle Miller (Jan 30 2021 at 00:30):

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

view this post on Zulip Kyle Miller (Jan 30 2021 at 00:31):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:31):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:32):

This also works:

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:33):

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

view this post on Zulip Kyle Miller (Jan 30 2021 at 00:33):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:34):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:35):

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

view this post on Zulip Mario Carneiro (Jan 30 2021 at 00:36):

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

view this post on Zulip Kyle Miller (Jan 30 2021 at 00:39):

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

view this post on Zulip Johan Commelin (Jan 30 2021 at 05:40):

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?

view this post on Zulip Yury G. Kudryashov (Feb 02 2021 at 13:34):

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

view this post on Zulip Yury G. Kudryashov (Feb 02 2021 at 13:35):

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

view this post on Zulip Yury G. Kudryashov (Feb 02 2021 at 13:37):

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.

view this post on Zulip Yury G. Kudryashov (Feb 02 2021 at 13:37):

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

view this post on Zulip Eric Wieser (Feb 02 2021 at 13:46):

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

view this post on Zulip Gabriel Ebner (Feb 02 2021 at 13:52):

Don't we already have that linter?

view this post on Zulip Eric Wieser (Feb 02 2021 at 15:25):

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

view this post on Zulip Kyle Miller (Feb 02 2021 at 18:14):

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.

view this post on Zulip Eric Wieser (Feb 02 2021 at 18:25):

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

view this post on Zulip Eric Wieser (Feb 02 2021 at 18:26):

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

view this post on Zulip Kyle Miller (Feb 02 2021 at 18:26):

(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.)

view this post on Zulip Eric Wieser (Mar 01 2021 at 10:04):

I had a go at making this linter in #6485


Last updated: May 17 2021 at 15:13 UTC