Permutation groups - coercions from nat to (fin n)

Stream: new members

[Antoine Chambert-Loir]

Imagine the context is (n:ℕ) [hn:5 ≤ n] and you want to introduce basic cycles in the finite permutation group equiv.perm (fin n) on fin n, using the notation c[…] introduced in docs#concrete_cycle. What would you type ?
If I type something like c[0,1,2], what I get is (of course) an object in equiv.perm ℕ, which is not what I want.

[Kevin Buzzard]

<= is not a class and so [hn : 5 <= n] will not put 5 <= n into the typeclass system (because it won't ever go in there)

[Kevin Buzzard]

But the answer to your question is to use "type ascriptions" (I think this is what they're called). Either you don't write 0, you write (0 : fin 5), or you write (c[0,1,2] : equiv.perm (fin 5)).

[Antoine Chambert-Loir]

Thanks. Now, this works if I enter

  let c₁ := (c[0,1,2] : equiv.perm (fin(5))),

but not at all if I enter

  let c₂ := (c[0,1,2] : equiv.perm (fin(n))),

for a reason I can well understand: Lean cannot prove [0,1,2].nodup meaning that if 5 <= n, then the cycle (list) [0,1,2] has no duplicates. I could try to prove this, but what puzzles me even more is that it refuses

  let c₃ := ([0,1,2] : list (fin(n))),

complaining that it cannot prove has_one (fin n).

[Kevin Buzzard]

fin 0 doesn't have a one

[Antoine Chambert-Loir]

I see. I can get the following workaround. Since I have 5 <= n, I have 5 distinct elements in fin n.
Is there a standard way I can get 5 such elements and name them, say a,b,c,d,e ? Does this requires tactic programming ?

[Johan Commelin]

I think that will quickly get messy. You need a concise way of expressing that the elements are all pairwise unequal. And a concise way of using that assumption when you need it.

[Johan Commelin]

I didn't test it, but what happens if you replace n by n+5 in your example?

[Johan Commelin]

Then Lean might figure out without help that [0,1,2,3,4].nodup holds.

[Antoine Chambert-Loir]

This is marvelous !
And exactly in line with a similar comment of @Kevin Buzzard on the Euler's product formula thread. Thank you ! https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Proof.20of.20Euler's.20product.20formula.20for.20totient/near/261388726

[Johan Commelin]

@Antoine Chambert-Loir You can convert 5 ≤ n into ∃ k, n = k + 5 using something like nat.exists_eq_add_of_le.

[Johan Commelin]

So you can do obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le h5 (where h5 is the name of the 5 ≤ n assumption)

[Eric Wieser]

This overlaps with something I was thinking about yesterday... Should we replace instance fin.has_zero : has_zero (fin n.succ) with instance : fin.has_zero [fact (0 < n)] : has_zero (fin n)?

[Eric Wieser]

We have the fact instance globally as docs#succ_pos''

[Eric Wieser]

I guess we can't replace it as the instance is in core while the fact is not, but we can add another instance and the two will be defeq