Provably equal types

Stream: new members

[Lars Brünjes]

I have a family of types layer : \N -> Type and a family of functions f i k : layer i -> layer (i + k), for which I would like to show that it is transitive in the sense of f i (k + l) = f (i + k) l \o f i k. The problem is that this doesn't even type-check, because layer (i + (k + l)) and layer (i + k + l) are not definitionally equal. I can formulate my lemma using heterogenous equality, but I can't prove it.

Maybe it's necessary to understand how f is defined: I have a function step : layer n -> layer (n + 1), and I define f via induction on k, using step.

Anyway, when I try to prove my lemma, I get stuck when I try to use f i (k + l)l x == f (i + k) l (f i k x) to conclude that step (f i (k + l) x) == step (f (i + k) l (f i k x)). I have tried various "congruence" lemmas like congr_arg_heq, but nothing works so far.

A hint would be highly appreciated!

[Kevin Buzzard]

Yes, this is problematic in dependent type theory.

[Kevin Buzzard]

One trick is to make the sigma type Sigma n, layer n and define define functions parametrised just by k from this sigma type to itself.

[Kevin Buzzard]

One can also battle through the heq proof, but you should probably post a #mwe for this

[Lars Brünjes]

Thank you very much for the Sigma type idea - I'll give it a spin. If that won't work, I'll consider posting a #mwe.

[Kevin Buzzard]

There is an extensive thread about this issue here

[Lars Brünjes]

I'll have a look - thanks again! :smile:

[Kevin Buzzard]

I struggle through the heq proof, other people come up with tidier heq solutions and then Mario uses sigma types and it comes out much better.

[Eric Wieser]

I did some heq stuff very recently in branch#eric-wieser/direct_sum-ring

[Eric Wieser]

But found that actually sigma equality was better than heq for my use case, because proving that (x : layer j) == (y : layer i) doesn't hold on to the proof that i = j (as layer could be defined as a constant type for all indices)

[Kyle Miller]

I had the almost the same setup and the exact same problem, and I'd thought about using sigma types, but I decided it was easier to use indexed families of sets instead. You can convert this back into an indexed family of types in the end if you need it. One difference, though, was that I was specifically dealing with indexed families of finite types, so there were some reasons an indexed family of finsets was more convenient.

Here's how I encoded the family:
https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/konig2.lean#L11

[Lars Brünjes]

Thanks a lot for those hints!

[Lars Brünjes]

I managed to define my function for sigma types and also proved the desired "transitivity" property. Still struggling to translate that result back into the original heterogeneous equality - but I'm not sure I even need that. Maybe the statement on the level of sigma types is precisely what I really need...