Stream: new members

Topic: derive fintype

Julian Berman (Oct 25 2020 at 15:08):

I am trying to prove that a dependent type ("move") is finite, and found derive fintype. When I try to use it, I get cases tactic failed, unexpected failure when introducing auxiliary equalities -- I assume this is because just adding it to my structure is trying to prove fintype move, which is indeed not true, I want it to derive fintype (move b) for a fixed thing.

Is there something else I can do to still use that helper or should I give up on derive fintype and prove finiteness without it (something I'm not having much success doing either but at least I know what the proof should look like.)

Julian Berman (Oct 25 2020 at 15:09):

@[derive fintype, nolint has_inhabited_instance]
structure move :=
(start_square : m × n)
(end_square : m × n)
(occupied_start : b.contents.occupied_at start_square . tactic.exact_dec_trivial)
(unoccupied_end : ¬ b.contents.occupied_at end_square . tactic.exact_dec_trivial)


is what the type looks like, though it's taking me a bit to make that a #mwe

Julian Berman (Oct 25 2020 at 15:33):

OK trying to use refine derive_fintype.mk_fintype _ _ _, isn't getting me much further so probably I've done something else wrong I guess. Never mind the above will try to put something self contained together if I can't figure it out.

Reid Barton (Oct 25 2020 at 16:32):

It might be easier to guess what's going on with at least the declarations of what appear to be variables m, n, b

Julian Berman (Oct 25 2020 at 16:53):

Yeah apologies... m and n are

variables {m n : Type}
variables [fintype m] [fintype n] [decidable_eq m] [decidable_eq n]


b is another struct... a  board m n ι K which is what's making it hard to reproduce on a smaller example. When I try with some other contrived derived type I seem to be able to make derive fintype work regardless.

which I just took a break from again to recharge, but if anything looks obviously wrong there lemme know. Otherwise going to take another crack at it later.

Reid Barton (Oct 25 2020 at 16:55):

The documentation for fintype deriving says that it will assume fintype instances on any type variables of the structure, so that seems okay. Does it work if you delete the last two fields of move?

Yes

Reid Barton (Oct 25 2020 at 16:57):

how about if you remove the . tactic stuff?

Reid Barton (Oct 25 2020 at 16:58):

I assume those fields are Props?

Julian Berman (Oct 25 2020 at 16:58):

It also works on e.g.:

import data.fintype.basic
import tactic.derive_fintype

variables {m n : Type}
variables [fintype m] [fintype n] [decidable_eq m] [decidable_eq n]

structure bar
(z : ℕ)

variable (b : bar 7)

@[derive fintype]
structure foo
(x : m × n)
(y : m × n)
(h : b = b . tactic.exact_dec_trivial)


which was my attempt to extract

Reid Barton (Oct 25 2020 at 16:59):

I see. Sometimes it's easier to put everything needed in a new file and then start whittling away at it until it no longer breaks, rather than trying to build up from scratch while guessing the key features

Julian Berman (Oct 25 2020 at 17:00):

nod yeah will try doing that

Reid Barton (Oct 25 2020 at 17:01):

But anyways it seems like your original usage is within the scope of what the derive handler is currently supposed to do

Julian Berman (Oct 25 2020 at 17:04):

OK that's good, glad to have the sanity check, appreciated.

Mario Carneiro (Oct 25 2020 at 17:09):

It doesn't handle this

Mario Carneiro (Oct 25 2020 at 17:09):

I didn't implement anything for propositional fields

Mario Carneiro (Oct 25 2020 at 17:11):

these are problematic because they don't have fintype instances

Mario Carneiro (Oct 25 2020 at 17:11):

because fintype p for p : Prop is already not well typed

Mario Carneiro (Oct 25 2020 at 17:13):

actually, looking at the code again, it seems that we only need a fintype instance on the iterated Sigma' type

Julian Berman (Oct 25 2020 at 17:13):

if you'll allow me to say something naive just to check my understanding...

Julian Berman (Oct 25 2020 at 17:13):

terms of p are proofs right?

Julian Berman (Oct 25 2020 at 17:13):

and there's proof equivalence that I've seen referenced before?

Mario Carneiro (Oct 25 2020 at 17:13):

p is a proposition, its elements are proofs

Mario Carneiro (Oct 25 2020 at 17:13):

it's obviously a fintype in the mathematical sense, there is only zero or one element

Julian Berman (Oct 25 2020 at 17:13):

so even if they're infinite, one could regard them as finite

right ok cool

Mario Carneiro (Oct 25 2020 at 17:14):

but fintype : Type u -> Type u so p doesn't fit in there

Mario Carneiro (Oct 25 2020 at 17:14):

you could put plift p in instead

Reid Barton (Oct 25 2020 at 17:15):

clearly fin_enum is superior :upside_down:

Mario Carneiro (Oct 25 2020 at 17:17):

This should probably be addressed in fintype but it's a question of where to draw the line, as you might argue that finset or multiset or list should accept Sort u as well

Mario Carneiro (Oct 25 2020 at 17:17):

However, given that the proof method relies on inferring instances for Sigma' it might be possible to fix this with a few extra instances

Mario Carneiro (Oct 25 2020 at 17:19):

Specifically, Sigma' h : p, a h is a fintype if a h is, and Sigma' x : A, p x is a fintype if A is, where p is a prop

Reid Barton (Oct 25 2020 at 17:19):

@Julian Berman Didn't you say that your foo example worked though?

Julian Berman (Oct 25 2020 at 17:20):

@Reid Barton it does yes

Mario Carneiro (Oct 25 2020 at 17:25):

I was confused about this for a bit until I realized that foo there has three parameters and no fields

ah :( sorry

Reid Barton (Oct 25 2020 at 17:26):

I noticed that about bar (because of bar 7) but missed it for foo!

Mario Carneiro (Oct 25 2020 at 17:27):

and if you put the := in the right place you get the expected error:

failed to synthesize type class instance for
⊢ fintype (Σ' (x y : m × n), b = b)


Julian Berman (Oct 25 2020 at 17:27):

that's still slightly different than the one in my real code which blows up harder and doesn't even show me a failed to synthesize type class message

Mario Carneiro (Oct 25 2020 at 18:09):

#4777 adds some tweaks to make sure that this use case is supported

Mario Carneiro (Oct 25 2020 at 18:10):

but it would be good to know what error you are seeing in case it's not handled

Mario Carneiro (Oct 25 2020 at 18:13):

btw the instances on psigma for props are already there, src#psigma.fintype_prop_left

Mario Carneiro (Oct 25 2020 at 18:14):

the reason the example above isn't finding it is because the prop has to be decidable and equality on bar 7 is not registered as decidable

Julian Berman (Oct 25 2020 at 19:43):

Oh amazing, thanks. Will give that commit a shot.

Julian Berman (Oct 25 2020 at 19:44):

The error I get at the minute is really the above -- cases tactic failed, unexpected failure when introducing auxiliary equalities with no further detail

Julian Berman (Oct 25 2020 at 19:45):

I don't know what sigma' and psigma are yet to understand the other thing you told me :), but will see if I can follow after staring a bit

Julian Berman (Oct 25 2020 at 19:48):

Actually I guess I can show you the error by pushing and letting CI fail, so can do that...

Mario Carneiro (Oct 25 2020 at 19:50):

Yeah, that bug is fixed in #4777

Julian Berman (Oct 25 2020 at 19:51):

ah awesome, ok gonna try it now thanks.

Julian Berman (Oct 25 2020 at 19:56):

OK that indeed now gives me a clearer error, now I get:

[lean] [E] exact tactic failed, type mismatch, given expression has type
m × n
but is expected to have type
Σ' (end_square : m × n)
(occupied_start :
auto_param (b.contents.occupied_at ?m_1)
(name.mk_string "exact_dec_trivial" (name.mk_string "tactic" name.anonymous)))
(unoccupied_end :
auto_param (¬b.contents.occupied_at end_square)
(name.mk_string "exact_dec_trivial" (name.mk_string "tactic" name.anonymous))),
unit


Julian Berman (Oct 25 2020 at 19:56):

(where I guess it figured out one field?)

Mario Carneiro (Oct 25 2020 at 20:03):

oh no that's a bug

Mario Carneiro (Oct 25 2020 at 20:03):

could you make a #mwe?

Trying to.

Julian Berman (Oct 25 2020 at 20:19):

OK I think this is reasonably minimal hopefully:

import tactic.derive_fintype

variables (m : Type) [fintype m]
structure board := (contents : m × m → m)

variables (b : board m)

@[derive fintype]
structure move :=
(start_square : m × m)
(occupied_start : b.contents start_square = b.contents start_square)


Mario Carneiro (Oct 25 2020 at 20:34):

ok, fixed in #4777

Julian Berman (Oct 25 2020 at 20:44):

Works, thank you!

Julian Berman (Oct 26 2020 at 02:27):

Found another bug here if you're not tired of me already. I think minimal repro is:

import tactic.derive_fintype

@[derive fintype]
structure foo4 (m n : Type) (b : m → ℕ) :=
(x : m × n)
(y : m × n)
(h : b x.1 = b y.1)

variables (m n : Type)
variable (b : m → ℕ)

@[derive fintype]
structure foo5 extends (foo4 m n b) :=
(h2 : to_foo4 = to_foo4)


Julian Berman (Oct 26 2020 at 02:27):

(Seems it doesn't like the to_foo4 in particular.)

Mario Carneiro (Oct 26 2020 at 05:20):

@Julian Berman This one is not a bug. The fintype deriver assumes that the fintype instance has the form (fintype on all type args -> fintype on inductive), but for propositions you need decidable_eq, and even if you derive decidable_eq on foo4 it still will have to assume that m and n have decidable_eq, which is not implied by fintype. So you have to state the correct assumptions manually, although you can still use the tactic to prove it:

@[derive [fintype, decidable_eq]]
structure foo4 (m n : Type) (b : m → ℕ) :=
(x : m × n)
(y : m × n)
(h : b x.1 = b y.1)

variables (m n : Type) [fintype m] [fintype n]
variable (b : m → ℕ)

structure foo5 extends (foo4 m n b) :=
(h2 : to_foo4 = to_foo4)

instance foo5.fintype [decidable_eq m] [decidable_eq n] : fintype (foo5 m n b) :=
by tactic.mk_fintype_instance


Julian Berman (Oct 26 2020 at 12:29):

@Mario Carneiro Apologies I think I slightly oversimplified the example, just to be sure, it's this one (which even with that manual declaration produces the error I see in my real code, shown at the bottom here):

import tactic.derive_fintype

variables (m n : Type) [fintype m] [decidable_eq m]
variables [fintype n] [decidable_eq n]

structure board := (contents : m × n → m)

variables {m n}
variables (b : board m n)

@[derive [fintype, decidable_eq]]
structure foo4 :=
(x : m × n)
(y : m × n)
(h : b.contents = b.contents)

structure foo5 extends foo4 b :=
(h2 : to_foo4 = to_foo4)

instance foo5.fintype [decidable_eq m] [decidable_eq n] : fintype (foo5 b) :=
by tactic.mk_fintype_instance


produces:

[lean] [E] synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
λ (a b : n), _inst_6 a b
inferred
λ (a b : n), _inst_4 a b
——————————————————————————————————————————————————————————————————————————————
[lean] [E] synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
λ (a b : n), _inst_6 a b
inferred
λ (a b : n), _inst_4 a b


Julian Berman (Oct 26 2020 at 12:29):

Let me see if I understand enough about what you explained to see whether that's still my fault.

Julian Berman (Oct 26 2020 at 12:38):

And now that error message is saying what... derive_fintype figured out how to make a fintype instance, but the one it made isn't equal enough to the one fintype wants? Is that saying I need foo5 to be decidable_eq too.. let's see.

Mario Carneiro (Oct 26 2020 at 13:19):

You now have two decidable_eq assumptions, since you've got it in the variables

Mario Carneiro (Oct 26 2020 at 13:52):

you can actually use

instance foo5.fintype : fintype (foo5 b) :=
by tactic.mk_fintype_instance


or go back to the simple form

@[derive fintype]
structure foo5 extends foo4 b :=
(h2 : to_foo4 = to_foo4)


with this version

Julian Berman (Oct 26 2020 at 13:59):

Ahh ok I think I follow.

Julian Berman (Oct 26 2020 at 14:09):

Yeah that indeed works perfectly again, I guess I didn't realize having [decidable_eq m] twice wasn't "idempotent", probably my understanding of precisely what that does is still too hazy, sorry for the noise, and thanks again.

Mario Carneiro (Oct 26 2020 at 14:14):

It's just like having two has_zero A instances

Mario Carneiro (Oct 26 2020 at 14:15):

the two zeros aren't necessarily the same

Mario Carneiro (Oct 26 2020 at 14:15):

In this case, the two decidable instances are equal, because decidable is a subsingleton, but they aren't definitionally equal and the tactic is picking the wrong one up from typeclass inference

Julian Berman (Oct 26 2020 at 14:15):

ahh ok that I think is my misunderstanding -- I thought [decidable_eq m] means "make sure m is a type for which instances have decidable equality"

Julian Berman (Oct 26 2020 at 14:16):

it means literally get me an instance of that type?

Julian Berman (Oct 26 2020 at 14:16):

(one with that property)

er, term, sorry

Mario Carneiro (Oct 26 2020 at 14:16):

yes, it's literally an extra argument to the instance

got it

Mario Carneiro (Oct 26 2020 at 14:16):

You can #print foo5.fintype to see all the instance arguments that are going into it

Mario Carneiro (Oct 26 2020 at 14:17):

you should try to avoid having duplicate instance arguments

Julian Berman (Oct 26 2020 at 14:17):

what do you do in your case? where you want 2 has_zeros?

Mario Carneiro (Oct 26 2020 at 14:18):

why would you ever want that? That's just asking for trouble to notate two distinct elements with the same notation

ok good

Julian Berman (Oct 26 2020 at 14:19):

thanks that makes a lot more sense now

Last updated: May 15 2021 at 00:39 UTC