reducing the index of a type

Stream: general

[Simon Andreys]

I'm having some trouble because the compiler doesn't recognize that for some type T n with an index n in a group, we have T (n+k+l)=T (n+(k+l)) (for some variables n, l, k, I suppose that it works fine when we fix n,l,k as explicit numbers). I guess this is a common problem with a standard solution, what is generally done in this case ? Should I compose by some canonical bijection between T (n+k+l) and T (n+(k+l)) , or is there a more subtle solution ?

Here is a mwe with the type fin n :

import tactic

namespace mwe

variables (m n k : nat)
def f: fin n→ fin (n+k) := λ i,begin  rcases i with ⟨ val, ineq⟩, exact fin.mk (val+k) (by linarith), end --makes the sum i->i+k and changes the type.
lemma composition_f : (f (n+k) m)∘ (f n k)= f n (k+n)

end mwe

which gives me the error

type mismatch at application
  f (n + k) m ∘ f n k = f n (k + n)
term
  f n (k + n)
has type
  fin n → fin (n + (k + n))
but is expected to have type
  fin n → fin (n + k + m)

In a more complex case with type adjoin_root I get a deterministic timeout, I suppose the compiler gets stuck trying to figure out some way to match the types.

[Johan Commelin]

Yes, this is a common problem. And it is very annoying.

[Johan Commelin]

Two possible solutions are: make everything terms of a sigma type \Sig g : G, T g, or do as you suggest, and compose with a canonical bijection. The latter happens quite often in the category library. You would have to start treating T as a "functor" on a groupoid. (You don't need to use the category lib for this, but you should be aware that the code is forcing you into this "functorial" direction.)

[Simon Andreys]

I took me some time figuring out what was causing the timeout ! I'll try the functorial workaround, I understand it better than the sigma type solution.

[Simon Andreys]

Moreover, thinking of this as a functor from the group seen as a category to the set category or the ring category makes me feel better, for some reason.

[Johan Commelin]

If you search for heq in this chat, you'll find other solutions being discussed.

[Johan Commelin]

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/heq.20alternative/near/210378589 is quite interesting

[Sebastien Gouezel]

Also, in your mwe you have a typo (k + n should be k + m in the error message).

[Simon Andreys]

Indeed, I've edited it (I've checked that the error message doesn't change other than the n-> m). @Johan Commelin nice, I understand better the sigma type solution now, although this "path" business is still obscure for me. I feel like the solutionC : Π {n : ℕ}, vector α n → ι is not flexible enough (mostly because of Reid Barton's saying "the purpose of C is to hide the problematic type index, so it can't appear in the result type of C") but I don't yet understand the implications here.

[Yakov Pechersky]

In this particular case, you can use fin.cast

[Yakov Pechersky]

So could you phrase your lemma to include cast?

[Simon Andreys]

@Yakov Pechersky okay that would be the particular case of the "canonical bijection" solution. However I wrote this only to illustrate by a minimal working example, my problem is actually on quotients of ring by some ideals. So what I need is some ideal.quotient.cast function.

[Simon Andreys]

I just defined a function quotient_cast : {I J: ideal R} (iej: I=J) : I.quotient →+* J.quotient together with two "trivial" lemmas, one taking care of the reflexive equality I=I and the other one taking care of the transitivity of equality with I=J and J=K. I used ideal.quotient_map and I had to dsimp definitions for the lemmas... I feel like there could be a more general function "cast" defined on any indexed type, with the same two lemmas. Maybe it already exists somewhere in category theory ?

[Johan Commelin]

Note that very often, these kind of "congr" lemmas are special cases of generally useful ones. For example if I <= J, then you also get such a map...

[Kevin Buzzard]

Johan raises an important point. Sets are modelled internally as functions to Prop, and even if two sets I and J are equal but not definitionally equal, proving $I\subseteq J$ is still easy.

[Simon Andreys]

True, I should make it more general with I <= J. Using ideal.quotient.mk instead of ideal.quotient_map will probably make the proof of the lemmas more natural...

[Johan Commelin]

@Simon Andreys but the more general version will undoubtly already be there, somewhere in mathlib.

[Simon Andreys]

I've been looking for it, but it seems to be well hidden... I found submodule.quot_equiv_of_eq for the weak version of the quotient by two equal submodule (and there seems to be no attached lemmas), but the closest thing I found for ring morphisms is ideal.quotient_map... I may be looking at the wrong place or searching for the wrong names.