Confused by finiteness

Stream: new members

[Philippe Duchon]

I am confused about the various notions of finiteness (or is it by coercions?).

In the following example, hovering over the proof state tells me that fixedPoints f is indeed a Set α as I expected, so I don't understand why rewriting fails (there is a long error message but I don't understand it)

import Mathlib

open Function

theorem hcfp (α: Type) [Fintype α] [DecidableEq α] {f: α → α}
  (h: fixedPoints f = ∅) : Fintype.card (fixedPoints f) = 0 := by
  rw [h]
  sorry

In my original code f had type Equiv.Perm α so that there was an additional coercion to α → α, but this doesn't seem to be the source of the problem.

(Also, I notice there are two different symbols for coercions, ↑ and ⇑; I don't think I understand the difference between the two.)

[Kevin Buzzard]

(there is a long error message but I don't understand it)

Post it anyway! Plenty of people here will understand it!

Tactic `rewrite` failed: motive is not type correct:
  fun _a => Fintype.card ↑_a = 0

The answer is that you're in constructivist hell. If you're not a constructivist then you can use Nat.card instead of Fintype.card and then the rewrite works fine and you can solve the resulting goal with simp. Or are you specifically interested in a constructivist solution?

[Kevin Buzzard]

⇑ is speficially for coercion to functions (e.g. from a monoid homomorphism to a function), and ↑ is a generic coercion.

[Eric Wieser]

rw! (castMode := .all) [h] works

[Eric Wieser]

as does simp [h]

[Philippe Duchon]

Thanks!

I would certainly not define myself as a constructivist, but I was on the way to using Equiv.Perm.card_fixedPoints, which uses Fintype.card, so that was what I tried to use.

Good to know that simp [h] works - but it still looks a little like black magic to me.

[Kevin Buzzard]

Lean doesn't do magic and there's certainly an explanation, but it's technical. I believe that there is some extension of rw in the works that will simply work and not give you this obscure error.

[Aaron Liu]

I just remembered there's a better way to do this

import Mathlib

open Function

theorem hcfp (α : Type) [Fintype α] [DecidableEq α] {f : α → α}
    (h : fixedPoints f = ∅) : Fintype.card (fixedPoints f) = 0 :=
  Fintype.card_congr' (congrArg Set.Elem h)

[Antoine Chambert-Loir]

In what sense is it better?

[Aaron Liu]

I don't know

[Aaron Liu]

it just seemed like using the dedicated lemma would be better