Zulip Chat Archive

Stream: new members

Topic: subtype question


view this post on Zulip Anca Ciobanu (May 31 2019 at 11:44):

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.

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:46):

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

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:47):

ha ha, revert H, simp works :D

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:47):

This should be trivial

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:50):

I am totally confused

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:51):

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

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:51):

simp won't tell me how it did it!

view this post on Zulip Chris Hughes (May 31 2019 at 11:52):

It uses subtype.mk.inj_eq

view this post on Zulip Chris Hughes (May 31 2019 at 11:52):

I think

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:55):

? 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.

view this post on Zulip Mario Carneiro (May 31 2019 at 11:58):

cases

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:59):

cases H doesn't work!

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:59):

This is why we asked.

view this post on Zulip Mario Carneiro (May 31 2019 at 11:59):

you sure?

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:59):

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

view this post on Zulip Kevin Buzzard (May 31 2019 at 11:59):

What is an equatily?

view this post on Zulip Mario Carneiro (May 31 2019 at 11:59):

woah that's a new one

view this post on Zulip Mario Carneiro (May 31 2019 at 12:00):

I think you found the bug

view this post on Zulip Mario Carneiro (May 31 2019 at 12:01):

injection should work

view this post on Zulip Mario Carneiro (May 31 2019 at 12:04):

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

view this post on Zulip Mario Carneiro (May 31 2019 at 12:07):

you can also simp at H

view this post on Zulip Xindi Ai (May 31 2019 at 13:59):

(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.

view this post on Zulip Kevin Buzzard (May 31 2019 at 14:02):

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.

view this post on Zulip Floris van Doorn (May 31 2019 at 19:10):

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

view this post on Zulip Jesse Michael Han (May 31 2019 at 19:16):

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

Last updated: May 07 2021 at 00:30 UTC