derangements mwe and questions

Stream: new members

[Henry Swanson]

Hi everyone, I'm new to Lean, and after going through the tutorials, I thought I'd try to tackle the formula for the number of derangements (freek 88).

The informal argument is pretty straightforward (show an equivalence between derangements(n+2) and derangements on smaller sets), but building that equivalence is proving to be way more verbose than I expected. I'm starting to wonder whether I'm going about this "against the grain" of Lean. I suspect that I am, but I'd love to hear what advice more experienced folks can offer.

I've got a MWE written up (it's just what I have minus all the extra lemmas I didn't need to use): https://pastebin.com/UbjGTp7U

Since that's pretty long, here's the specific questions I have:

• when should i be using fintype vs finset? I figure the advantage of finset is that I can use plain-old-equality, and not have to juggle subtypes around like in lemma derangement_ignore_two_cycle, right? If that's the case, I think finset is probably more appropriate here.
• how do i make members of {x : perm T // some_predicate} behave like functions? I have to append .val to use them as functions, and I'm not sure how to make that conversion happen automatically. Lines 320 and 321 are particularly awful.
• I have a lot of trouble getting rw to rewrite things, particularly when coercions are involved. This is probably more an art than a science, but are there any rough guidelines that'd help? For example, on line 209, I have to swap the goal and a hypothesis, and then contrapose, because a plain rewrite gave me motive errors.
• Lastly, I'm quite stuck on showing fintype.card {k : fin(n+2) // k ≠ 0 ∧ k ≠ m.succ } = n. It's easy with finsets, but I haven't a clue with fintypes. Maybe that's more evidence the former is more appropriate?

[Johan Commelin]

@Henry Swanson Welcome. Your first observation on fintype vs finset sounds right.

[Johan Commelin]

For point two, you want to create an instance of has_coe_to_fun for derangements.

[Johan Commelin]

For point three. Sometimes simp [hyp] will be able to avoid the motive errors. If not, then you might need to refactor parts of the setup. Or live with the DTT pain (-;

[Johan Commelin]

For point 4: I agree. My gut instinct would be to move it to a question about finsets as soon as possible.

[Johan Commelin]

Line 25: := begin exact bla_bla end is the same as := bla_bla

[Johan Commelin]

I've briefly looked through the rest of the code, and I agree with you that it looks like finset will be easier to work with.

[Eric Wieser]

For your last point, just construct an equiv to fin n

[Henry Swanson]

@Johan Commelin On one hand, it's nice to know my intuition was okay, but on the other, this means I have a lot of rewriting to do :) In any case, thank you!
@Eric Wieser I futzed around with pred_above for a while, but the fact that I can't pass in any element of the domain (it only takes elements of the codomain) made it kinda messy; I'll see if I can get that working again!

[Eric Wieser]

You should be able to go via card {k : fin n.succ // k ≠ m} = n, which may or may not be easiee