Interpreting `motive is not type correct`

Stream: general

[nrs]

Error: application type mismatch
  @Fintype.card (Fin2 _a) (inst✝ x)
argument
  inst✝ x
has type
  Fintype (sig.toP.β x) : Type
but is expected to have type
  Fintype (Fin2 _a) : Type

In the code below, I'm getting the motive is not type error above. What does the notation _a in Fin2 _a mean, and why does Lean expect Fin2 _a instead of sig.toP.β x here?

structure P where
  α : Type
  β : α -> Type

structure Signature where
  symbols : Type
  arity : symbols -> Nat

def Signature.toP : Signature -> P
| ⟨sy, ar⟩ => ⟨sy, (fun n : Nat => Fin2 n) ∘ ar⟩

def P.toSignature (F : P) [(a : F.α) -> Fintype (F.β a)] : Signature :=
 ⟨F.α, fun a => Fintype.card (F.β a)⟩

def FintFin2Card : (n : Nat) -> Fintype.card (Fin2 n) = n := by
  intro n
  induction' n with n ih
  · simp +ground
  · rw [Fintype.card, Finset.univ, Fintype.elems, Fin2.instFintype]
    simp
    rwa [Fintype.card, Finset.univ] at ih

def inverse1 {sig : Signature} [(a : sig.toP.α) → Fintype (sig.toP.β a)]: P.toSignature (Signature.toP sig) = sig := by
  rw [P.toSignature]
  simp!
  congr! with x
  rw [<- FintFin2Card (sig.arity x)] -- error here

[Kyle Miller]

You're quoting just part of the error message — the entire error message explains this. Could you say what about the error message is unclear?

[nrs]

From what I understand, it means that the greater expression depends on the piece I'm trying to rewrite, but doesn't a rewrite just unfold an expression? I'd expect my rewrite to just also rewrite those other parts that depend on the smaller part I'm trying to rewrite

[nrs]

I don't understand the message very well, suggestions/resources on how rewriting works more in depth also work! reading more closely did clear up the part on the notation _a however

[nrs]

In case this helps someone,

def inverse1 {sig : Signature} [(a : sig.toP.α) → Fintype (sig.toP.β a)]: P.toSignature (Signature.toP sig) = sig := by
  rw [P.toSignature]
  simp!
  congr! with x
  have := FintFin2Card (sig.arity x)
  convert this

closes the goal, but I have no clue why we have to take this route. I got to this by trying exact this first, seeing a different typeclass synthesized between the goal and this and thinking convert might automatically determine their exact differences. Any explanations for why the problem occurred (and why convert works without generating new goals) would be highly appreciated, the totality of context is given by the code above

[Ruben Van de Velde]

Guessing based on the partial code you pasted: Fintype contains a list (well, Finset) of elements of the type, so there can be different instances with different underlying lists, but convert can deal with that

[nrs]

ah that makes a lot of sense, I encountered a similar phenomenon when proving FintFin2Card, it seems Fin doesn't have the same issue (or automation works a bit better for it). thanks for the reply!

[Kevin Buzzard]

convert knows about Subsingleton.elim and these data-carrying typeclasses like Fintype often have subsingleton instances associated with them.

[Ruben Van de Velde]

I think convert may have specific code for Fintype, but the high-level idea is the same: convert says "this is a dumb goal, I'll handle it"

[nrs]

Kevin Buzzard said:

convert knows about Subsingleton.elim and these data-carrying typeclasses like Fintype often have subsingleton instances associated with them.

I see, the subsingleton in question here is Finset.univ, right?

[Kyle Miller]

@Ruben Van de Velde All convert knows about Fintype is Subsingleton.elim, like Kevin said. However, it uses docs#Lean.Meta.FastSubsingleton and docs#FastSubsingleton.helim so it doesn't get bogged down with the general Subsingleton class. (The subsingleton tactic can be used to handle lingering expensive subsingleton goals.)

[Kyle Miller]

nrs said:

I see, the subsingleton in question here is Finset.univ, right?

Not quite, it would be the Fintype instance itself. As a consequence any two Finset.univs for the same type are equal.

[Ruben Van de Velde]

Okay, then I was just confused :)

[Kyle Miller]

nrs said:

doesn't a rewrite just unfold an expression?

Let's take a look at all of the error message. The very first part is explaining the motive:

tactic 'rewrite' failed, motive is not type correct:
  fun _a ↦ Fintype.card (Fin2 _a) = _a

Call this m. The rest of the error message explains that rewriting by LHS = RHS works by trying to find an m where m LHS is the current goal. If it's possible to find such an m, then rewriting can replace the goal with m RHS. However, rewrite's algorithm to come up with a motive failed — the motive is failing to typecheck.

"Just" unfolding would be to replace a constant with the body of the definition. Your FintFin2Card would not be considered to be unfolding anything. (If your theorems are definitional equalities, the dsimp tactic is a way to do such rewrites, "definitional simp".)

[Kyle Miller]

If you do

def inverse1 {sig : Signature} [(a : sig.toP.α) → Fintype (sig.toP.β a)]: P.toSignature (Signature.toP sig) = sig := by
  rw [P.toSignature]
  simp!
  congr! with x
  exact FintFin2Card (sig.arity x)

instead of convert FintFin2Card (sig.arity x), it reveals

type mismatch
  FintFin2Card (sig.arity x)
has type
  @Fintype.card (Fin2 (sig.arity x)) (Fin2.instFintype (sig.arity x)) = sig.arity x : Prop
but is expected to have type
  @Fintype.card (Fin2 (sig.arity x)) (inst✝ x) = sig.arity x : Prop

In particular, you somehow have two different Fintype instances. This can be hard to avoid (hence why we have tactics like convert/congr!).

[Kyle Miller]

If you use convert FintFin2Card (sig.arity x) using 0 you can see the initial goal it sets up, which it passes to congr!. The option set_option trace.congr! true gives an idea of the steps it uses.

[nrs]

I see! that makes a lot of sense, thank you very much for taking the time! the congr! trace option in particular is super useful

[Violeta Hernández]

I'd also like to point out the nuclear option: subst will never fail, so if all else doesn't work, you can prove an auxiliary lemma of the form a = b -> ... and apply it to whatever you want to prove.

[nrs]

Violeta Hernández said:

I'd also like to point out the nuclear option: subst will never fail, so if all else doesn't work, you can prove an auxiliary lemma of the form a = b -> ... and apply it to whatever you want to prove.

strikingly subst fails in the above case, even thought this and the goal have the exact same type

def inverse1 {sig : Signature} : P.toSignature (Signature.toP sig) = sig := by
  rw [P.toSignature]
  simp!
  congr! with x
  --convert (FintFin2Card (sig.arity x))
  have := FintFin2Card (sig.arity x)
  subst this

[nrs]

I wanted to ask in fact if anyone knows how to change a goal f x = y into a goal to @f x z = y where z is an argument previously implicit? in this case it would have permitted seeing that the goal was hiding an implicit argument that made rewriting fail

[Kyle Miller]

set_option pp.explicit true

[nrs]

thank you!!

[Kyle Miller]

With Violeta's suggestion, it never fails if it's the sort of hypothesis that subst can handle

[Kyle Miller]

It has to be an equality with a variable on at least one side.