Zulip Chat Archive

Stream: new members

Topic: Statements that require a previous result


view this post on Zulip Markus Himmel (Feb 09 2020 at 13:31):

How do you state something that only makes sense using some previous result? Consider the following MWE:

section
parameters {A : Type} {B : Type}

def f : A  A := id
def g : B  B := id

lemma A_eq_B : A = B := sorry
lemma does_not_typecheck : f = g := sorry -- this one is problematic

end

The lemma generates the error "type mismatch at application f = g term has type B → B but is expected to have type A → A". What would be the correct way to state this lemma in Lean that somehow uses the fact that A = B?

view this post on Zulip Mario Carneiro (Feb 09 2020 at 13:33):

There are two ways, neither very good. You can use f == g to assert that f and g have the same type, or you can use eq.rec to convert one type to the other

view this post on Zulip Mario Carneiro (Feb 09 2020 at 13:35):

section
parameters {A : Type} {B : Type}

def f : A  A := id
def g : B  B := id

lemma A_eq_B : A = B := sorry
example : f == g := by cases A_eq_B; refl
example : (eq.rec_on A_eq_B f : B  B) = g := by cases A_eq_B; refl

end

view this post on Zulip Mario Carneiro (Feb 09 2020 at 13:35):

But the real answer is: don't do this

view this post on Zulip Mario Carneiro (Feb 09 2020 at 13:36):

in your real example it might be warranted, but in this example it's clearly a bad idea

view this post on Zulip Mario Carneiro (Feb 09 2020 at 13:41):

There is an easy cases; refl proof in this case because f and g are the same function, but in real examples the proof would be harder

view this post on Zulip Markus Himmel (Feb 09 2020 at 14:29):

Thank you for the answer. I experimented with eq.rec_on, and while I was able to prove the lemma that inspired this question, I ran into problems when trying to apply the lemma (as you predicted). However I am working with categories and found a solution using eq_to_hom where all the instances of eq_to_hom cancel out nicely.

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 16:58):

Equality of types is a hairy thing. In your example you'd be better off knowing that if A=B then there's a map from A to B, and using this map instead of all these heq workarounds

view this post on Zulip Kevin Buzzard (Feb 09 2020 at 17:00):

At one point when doing basic group theory I had two equal normal subgroups of a group and I wanted to identify the quotients. I did it by writing down maps both ways between them instead of trying to use =


Last updated: May 08 2021 at 18:17 UTC