Zulip Chat Archive

Stream: new members

Topic: derive fintype


view this post on Zulip 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.)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

The full (non-working) patch is https://github.com/Julian/lean-across-the-board/commit/e7c7531b1288e72d9e96b54373fa3d2008f5f52e#diff-8ddc75490aa5cdbfa06071ac71ab81708c32207a98cd5688fa4dcc74781b9cefR74-R76

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.

view this post on Zulip 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?

view this post on Zulip Julian Berman (Oct 25 2020 at 16:55):

Yes

view this post on Zulip Reid Barton (Oct 25 2020 at 16:57):

how about if you remove the . tactic stuff?

view this post on Zulip Reid Barton (Oct 25 2020 at 16:58):

I assume those fields are Props?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 25 2020 at 17:00):

nod yeah will try doing that

view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 25 2020 at 17:04):

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

view this post on Zulip Mario Carneiro (Oct 25 2020 at 17:09):

It doesn't handle this

view this post on Zulip Mario Carneiro (Oct 25 2020 at 17:09):

I didn't implement anything for propositional fields

view this post on Zulip Mario Carneiro (Oct 25 2020 at 17:11):

these are problematic because they don't have fintype instances

view this post on Zulip Mario Carneiro (Oct 25 2020 at 17:11):

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

view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 25 2020 at 17:13):

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

view this post on Zulip Julian Berman (Oct 25 2020 at 17:13):

terms of p are proofs right?

view this post on Zulip Julian Berman (Oct 25 2020 at 17:13):

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

view this post on Zulip Mario Carneiro (Oct 25 2020 at 17:13):

p is a proposition, its elements are proofs

view this post on Zulip Mario Carneiro (Oct 25 2020 at 17:13):

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

view this post on Zulip Julian Berman (Oct 25 2020 at 17:13):

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

view this post on Zulip Julian Berman (Oct 25 2020 at 17:14):

right ok cool

view this post on Zulip Mario Carneiro (Oct 25 2020 at 17:14):

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

view this post on Zulip Mario Carneiro (Oct 25 2020 at 17:14):

you could put plift p in instead

view this post on Zulip Reid Barton (Oct 25 2020 at 17:15):

clearly fin_enum is superior :upside_down:

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Oct 25 2020 at 17:19):

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

view this post on Zulip Julian Berman (Oct 25 2020 at 17:20):

@Reid Barton it does yes

view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 25 2020 at 17:26):

ah :( sorry

view this post on Zulip Reid Barton (Oct 25 2020 at 17:26):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 25 2020 at 18:09):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Oct 25 2020 at 18:13):

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

view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 25 2020 at 19:43):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Oct 25 2020 at 19:50):

Yeah, that bug is fixed in #4777

view this post on Zulip Julian Berman (Oct 25 2020 at 19:51):

ah awesome, ok gonna try it now thanks.

view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 25 2020 at 19:56):

(where I guess it figured out one field?)

view this post on Zulip Mario Carneiro (Oct 25 2020 at 20:03):

oh no that's a bug

view this post on Zulip Mario Carneiro (Oct 25 2020 at 20:03):

could you make a #mwe?

view this post on Zulip Julian Berman (Oct 25 2020 at 20:05):

Trying to.

view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Oct 25 2020 at 20:34):

ok, fixed in #4777

view this post on Zulip Julian Berman (Oct 25 2020 at 20:44):

Works, thank you!

view this post on Zulip 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)

view this post on Zulip Julian Berman (Oct 26 2020 at 02:27):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Julian Berman (Oct 26 2020 at 12:36):

OK I think if I follow what you told me this morning that that's now "fixed" about this example?

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 26 2020 at 13:19):

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

view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 26 2020 at 13:59):

Ahh ok I think I follow.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Oct 26 2020 at 14:14):

It's just like having two has_zero A instances

view this post on Zulip Mario Carneiro (Oct 26 2020 at 14:15):

the two zeros aren't necessarily the same

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip Julian Berman (Oct 26 2020 at 14:16):

it means literally get me an instance of that type?

view this post on Zulip Julian Berman (Oct 26 2020 at 14:16):

(one with that property)

view this post on Zulip Julian Berman (Oct 26 2020 at 14:16):

er, term, sorry

view this post on Zulip Mario Carneiro (Oct 26 2020 at 14:16):

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

view this post on Zulip Julian Berman (Oct 26 2020 at 14:16):

got it

view this post on Zulip Mario Carneiro (Oct 26 2020 at 14:16):

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

view this post on Zulip Mario Carneiro (Oct 26 2020 at 14:17):

you should try to avoid having duplicate instance arguments

view this post on Zulip Julian Berman (Oct 26 2020 at 14:17):

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

view this post on Zulip 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

view this post on Zulip Julian Berman (Oct 26 2020 at 14:19):

ok good

view this post on Zulip 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