Cast exercise

Stream: new members

[Nicolò Cavalleri]

I am still very bad at proofs involving cast. Can I prove something like this?

example {α : Type*} {β : Type*} {γ : Type*} (h1 : (α × γ) = (β × γ)) (h2 : α = β) (a : α) (g : γ) :
  (cast h1 (a, g)).fst = cast h2 a := sorry

[Eric Rodriguez]

I'd really avoid type equality and focus on equivs if you can

[Nicolò Cavalleri]

What do you mean exactly?

[Kevin Buzzard]

h1 : (α × γ) = (β × γ) is an evil hypothesis.

[Kevin Buzzard]

Equality of types is like equality of objects in category theory -- it should be avoided if possible.

[Nicolò Cavalleri]

What does evil hypothesis mean? In my specific case I have a proof of both h1 and h2, so that should not be a problem

[Nicolò Cavalleri]

I am pretty sure I cannot avoid type equality

[Eric Wieser]

by { subst h2, refl }

[Nicolò Cavalleri]

Thank you very much!!

[Eric Wieser]

For someone more familiar with type equality - is this statement provable?

lemma prod_right_injective {α β γ} (h : (α × β) = (α × γ)) : β = γ :=
begin
  sorry
end

[Kevin Buzzard]

this is a pathological question

[Kevin Buzzard]

lol an interesting special case is \a = empty

[Kevin Buzzard]

@Nicolò Cavalleri here's some philosophy https://ncatlab.org/nlab/show/principle+of+equivalence but remember this: if you want to make your own mathlib in Lean 4 then you could make it so that nat = int was true, or you could make it so that it was unprovable, and all the proofs would still work, so there is something irrelevant about the question which as a mathematician you would not expect.

[Eric Wieser]

Which would look something like

def weird_int := nat

def weird_int.to_int (n : weird_int) : int : if nat.even n then n / 2 else -1 - n/2

instance : add_comm_group weird_int := equiv.add_comm_group sorry

[Mario Carneiro]

Eric Wieser said:

For someone more familiar with type equality - is this statement provable?

lemma prod_right_injective {α β γ} (h : (α × β) = (α × γ)) : β = γ :=
begin
  sorry
end

It's not disprovable, but the cardinality model falsifies it if you set α = β = empty and γ = unit

[Eric Wieser]

I don't really get what you mean by falsifies it. You mean it's false in a model where = iff equiv?

[Mario Carneiro]

yes

[Kevin Buzzard]

Set theory is the same -- you can ask if the quaternion $37\pi^2+i+k$ equals the Riemann Sphere $S^1$ in set theory. The answer is "it's unlikely, but in theory it could happen".

[Mario Carneiro]

even if you assume alpha is nonempty it's still false in the cardinality model with α = β = nat and γ = unit

[Mario Carneiro]

Actually, in set theory the answer is usually answerable (and false)

[Kevin Buzzard]

but what about independent developments with their own tricks?

[Mario Carneiro]

the "in theory it could happen" is quantifying over possible concrete implementations of the concepts

[Mario Carneiro]

for any particular implementation the question is a well defined "junk theorem"

[Kevin Buzzard]

oh sure

[Kevin Buzzard]

you just make a type theory on top of your set theory

[Mario Carneiro]

lean just makes most junk statements either type incorrect or independent