cast subtype

Stream: new members

[Bjørn Kjos-Hanssen]

I feel like this is true, but apparently cast is unpredictable... does anyone know how to prove it?

example { α : Type} {P Q : α → Prop} (a:α) (h₁ : P a) (h₂ : Q a)
(h₃ : { a : α // P a} = {a : α // Q a}):
cast h₃ (⟨a,h₁⟩) = (⟨a,h₂⟩)
    := sorry

[Yaël Dillies]

No this is definitely unprovable.

[Yaël Dillies]

It's good to remember the "cardinality model" of Lean, where types are equal iff they have the same cardinality. Here, {a // P a} and {a // Q a} could have the same cardinality without having P = Q. In the case where P ≠ Q, the cast could possibly not be the identity, even just on {a | P a ∧ Q a}.

[Bjørn Kjos-Hanssen]

So even if α is Fin 2 it won't be provable?

[Yaël Dillies]

If α := Fin 2, then it is provable since from {a // P a} = {a // Q a} you can derive that the number of elements satisfying P is the same as the number of elements satisfying Q, and since a satisfies both, it must be that P = Q. So you can substitute that in and then your result is easy.

[Yaël Dillies]

Yeah, your lemma is provable iff α has at most two elements.

[Bjørn Kjos-Hanssen]

Thanks, makes sense. Anyway, it turned that I only needed this:

example {α β: Type} (u₁ u₂ : β) {P : β → α → Prop} (a:α)
(h₁ : P u₁ a) (h₂ : P u₂ a) (hu : u₁ = u₂)
(h₃ : {a // P u₁ a} = {a // P u₂ a}):
cast h₃ (⟨a,h₁⟩) = (⟨a,h₂⟩)
    := by {
      subst hu
      exact rfl
    }