derive fintype

Stream: new members

[Julian Berman]

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]

@[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]

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]

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]

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.

[Reid Barton]

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?

[Julian Berman]

Yes

[Reid Barton]

how about if you remove the . tactic stuff?

[Reid Barton]

I assume those fields are Props?

[Julian Berman]

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]

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]

nod yeah will try doing that

[Reid Barton]

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

[Julian Berman]

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

[Mario Carneiro]

It doesn't handle this

[Mario Carneiro]

I didn't implement anything for propositional fields

[Mario Carneiro]

these are problematic because they don't have fintype instances

[Mario Carneiro]

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

[Mario Carneiro]

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

[Julian Berman]

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

[Julian Berman]

terms of p are proofs right?

[Julian Berman]

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

[Mario Carneiro]

p is a proposition, its elements are proofs

[Mario Carneiro]

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

[Julian Berman]

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

[Julian Berman]

right ok cool

[Mario Carneiro]

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

[Mario Carneiro]

you could put plift p in instead

[Reid Barton]

clearly fin_enum is superior :upside_down:

[Mario Carneiro]

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]

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]

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]

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

[Julian Berman]

@Reid Barton it does yes

[Mario Carneiro]

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

[Julian Berman]

ah :( sorry

[Reid Barton]

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

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Julian Berman]

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]

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]

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

[Mario Carneiro]

Yeah, that bug is fixed in #4777

[Julian Berman]

ah awesome, ok gonna try it now thanks.

[Julian Berman]

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]

(where I guess it figured out one field?)

[Mario Carneiro]

oh no that's a bug

[Mario Carneiro]

could you make a #mwe?

[Julian Berman]

Trying to.

[Julian Berman]

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]

ok, fixed in #4777

[Julian Berman]

Works, thank you!

[Julian Berman]

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]

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

[Mario Carneiro]

@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]

@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]

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

[Julian Berman]

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

[Julian Berman]

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]

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

[Mario Carneiro]

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]

Ahh ok I think I follow.

[Julian Berman]

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]

It's just like having two has_zero A instances

[Mario Carneiro]

the two zeros aren't necessarily the same

[Mario Carneiro]

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]

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]

it means literally get me an instance of that type?

[Julian Berman]

(one with that property)

[Julian Berman]

er, term, sorry

[Mario Carneiro]

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

[Julian Berman]

got it

[Mario Carneiro]

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

[Mario Carneiro]

you should try to avoid having duplicate instance arguments

[Julian Berman]

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

[Mario Carneiro]

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

[Julian Berman]

ok good

[Julian Berman]

thanks that makes a lot more sense now