Zulip Chat Archive

Stream: general

Topic: Hard but obvious lemma


view this post on Zulip Chris Hughes (Jun 22 2018 at 23:10):

How to prove this? I don't need it, I'm just curious.

example {α β : Sort u} {γ : α  Sort v} {δ : β  Sort v} {f : Π a, γ a} {g : Π b, δ b}
  {a : α} {b : β} (hfg : f == g) (hab : a == b) : f a == g b :=

view this post on Zulip Simon Hudon (Jun 22 2018 at 23:14):

I think there’s a meta theorem that says it can’t be proved in DTT

view this post on Zulip Simon Hudon (Jun 22 2018 at 23:14):

@Mario Carneiro

view this post on Zulip Chris Hughes (Jun 22 2018 at 23:18):

In that case, same question for

example {α β : Sort u} {γ δ : Sort v} {f : α  γ} {g : β  δ}
  {a : α} {b : β} (hfg : f == g) (hab : a == b) : f a == g b

view this post on Zulip Simon Hudon (Jun 22 2018 at 23:28):

I think you would need an equality α = β and γ = δ for this to be provable. Then, you can deduce f = g. I saw the theorem in a talk by Cody Roux. If I remember correctly, when you want to prove f x₀ .. xᵢ = g y₀ .. yᵢ, from x₀ == y₀ .. xᵢ == yᵢ, you need f = g for the statement to be provable.

view this post on Zulip Mario Carneiro (Jun 23 2018 at 02:48):

Leo has a whole paper on how he works around the unprovability of this theorem

view this post on Zulip Mario Carneiro (Jun 23 2018 at 02:48):

(co-authored with Cody IIRC)

view this post on Zulip Mario Carneiro (Jun 23 2018 at 02:50):

Although I think the actual unprovability is only folklore, I don't know an explicit proof although there is probably a way to modify the set model to get it

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:50):

He basically generates all the relevant theorems right? I think that's what congr does for heq goals

view this post on Zulip Mario Carneiro (Jun 23 2018 at 02:51):

yes, he's implemented a tactic meta-theorem for the version you stated


Last updated: May 12 2021 at 23:13 UTC