Zulip Chat Archive

Stream: new members

Topic: Provably equal types


view this post on Zulip Lars Brünjes (Jan 29 2021 at 00:31):

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!

view this post on Zulip Kevin Buzzard (Jan 29 2021 at 00:32):

Yes, this is problematic in dependent type theory.

view this post on Zulip Kevin Buzzard (Jan 29 2021 at 00:33):

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.

view this post on Zulip Kevin Buzzard (Jan 29 2021 at 00:34):

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

view this post on Zulip Lars Brünjes (Jan 29 2021 at 00:35):

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.

view this post on Zulip Kevin Buzzard (Jan 29 2021 at 00:37):

There is an extensive thread about this issue here

view this post on Zulip Lars Brünjes (Jan 29 2021 at 00:40):

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

view this post on Zulip Kevin Buzzard (Jan 29 2021 at 00:42):

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.

view this post on Zulip Eric Wieser (Jan 29 2021 at 01:04):

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

view this post on Zulip Eric Wieser (Jan 29 2021 at 01:06):

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)

view this post on Zulip Kyle Miller (Jan 29 2021 at 01:32):

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

view this post on Zulip Lars Brünjes (Jan 29 2021 at 01:57):

Thanks a lot for those hints!

view this post on Zulip Lars Brünjes (Jan 29 2021 at 02:00):

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...


Last updated: May 09 2021 at 19:11 UTC