Statements that require a previous result

Stream: new members

[Markus Himmel]

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?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

But the real answer is: don't do this

[Mario Carneiro]

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

[Mario Carneiro]

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

[Markus Himmel]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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 =