subtype question

Stream: new members

[Anca Ciobanu]

example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
  (H : (⟨x, hx⟩ : {x : X // P x}) = ⟨y, hy⟩ ) : x = y := sorry

How do you prove this? I tried induction H and I seemed to lose my hypothesis.

[Kevin Buzzard]

ha ha! Induction H seems to leave you in an unprovable state! What's going on there?

[Kevin Buzzard]

ha ha, revert H, simp works :D

[Kevin Buzzard]

This should be trivial

[Kevin Buzzard]

I am totally confused

[Kevin Buzzard]

set_option trace.simplify.rewrite true
example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
  (H : (⟨x, hx⟩ : {x : X // P x}) = ⟨y, hy⟩ ) : x = y :=
begin
  revert H,
  simp,
  /-
  0. [simplify.rewrite] [imp_self]: x = y → x = y ==> true
  -/
end

[Kevin Buzzard]

simp won't tell me how it did it!

[Chris Hughes]

It uses subtype.mk.inj_eq

[Chris Hughes]

I think

[Kevin Buzzard]

? This says <x,hx>=<y,hy> = (x = y) so now I have to jump through some hoops to make this. Anca is in tehe middle of a tactic proof and has H : <x,hx>=<y,hy> and we just want x=y.

[Mario Carneiro]

cases

[Kevin Buzzard]

cases H doesn't work!

[Kevin Buzzard]

This is why we asked.

[Mario Carneiro]

you sure?

[Kevin Buzzard]

example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
  (H : (⟨x, hx⟩ : {x : X // P x}) = ⟨y, hy⟩ ) : x = y :=
begin
  cases H,
  /-
  cases tactic failed, unexpected failure when introducing auxiliary equatilies
  -/

end

[Kevin Buzzard]

What is an equatily?

[Mario Carneiro]

woah that's a new one

[Mario Carneiro]

I think you found the bug

[Mario Carneiro]

injection should work

[Mario Carneiro]

the term proof is subtype.no_confusion H id or subtype.mk.inj H

[Mario Carneiro]

you can also simp at H

[Xindi Ai]

(I am new to Lean so please excuse my style)
I ran into a similar problem before and what I roughly did was

def mysubtype (X : Type) (P : X → Prop) : Type := {x : X // P x}

def myfun (X : Type) (P : X → Prop): mysubtype X P → X
|⟨x, hx⟩ := x

lemma mylemma (X : Type) (P : X → Prop) (x : X) (hx : P x): myfun X P ⟨x, hx⟩ = x := rfl

example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
  (H : (⟨x, hx⟩ : mysubtype X P) = ⟨y, hy⟩ ) : x = y :=
congr_arg (myfun X P) H

Seems to be a bit of a detour though.

[Kevin Buzzard]

Seems to be a bit of a detour though.

Yes! That was the annoying thing. I was showing an undergraduate how to use Lean and then this came up, and all of a sudden the whole thing looked far more complicated than it should have been.

[Floris van Doorn]

injection H is probably the best way to so this. Another possibility is congr_arg subtype.val H

[Jesse Michael Han]

laziest solution:

example (X : Type) (P : X → Prop) (x y : X) (hx : P x) (hy : P y)
  (H : (⟨x, hx⟩ : {x : X // P x}) = ⟨y, hy⟩ ) : x = y :=
begin
  library_search
  -- exact subtype.mk.inj H
end