Zulip Chat Archive

Stream: new members

Topic: equality/inequality in subtype


view this post on Zulip Heather Macbeth (Dec 29 2020 at 17:53):

What is the idiomatic way to do something like this?

import data.set.basic

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a  s) (h : b  a) : b  a, ha :=
sorry

I can think of a couple of ways:

import data.set.basic

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a  s) (h : b  a) : b  a, ha :=
begin
  intros h',
  apply h,
  rw h',
  refl,
end

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a  s) (h : b  a) : b  a, ha :=
begin
  intros h',
  apply h,
  cases h',
  refl,
end

but I feel like it ought to be a one-liner?

view this post on Zulip Kevin Buzzard (Dec 29 2020 at 17:59):

mt jumps you a step:

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a  s) (h : b  a) : b  a, ha :=
mt begin intro h2, rw h2, refl end h

but there's still that rewrite.

view this post on Zulip Kevin Buzzard (Dec 29 2020 at 18:00):

example {E : Type*} (s : set E) (a : E) (b : s) (ha : a  s) (h : b  a) : b  a, ha :=
mt (by {rintro rfl, refl}) h

view this post on Zulip Patrick Massot (Dec 29 2020 at 18:01):

by {  rintro h, rfl⟩, exact h rfl }

view this post on Zulip Patrick Massot (Dec 29 2020 at 18:01):

Oh Kevin had the same cheating idea.

view this post on Zulip Kevin Buzzard (Dec 29 2020 at 18:02):

rintro rfl is a really good way to hide rewrites

view this post on Zulip Patrick Massot (Dec 29 2020 at 18:02):

(hiding the rw in rintro)

view this post on Zulip Patrick Massot (Dec 29 2020 at 18:02):

:big_smile:

view this post on Zulip Patrick Massot (Dec 29 2020 at 18:02):

And none of this is really answering the initial question.

view this post on Zulip Heather Macbeth (Dec 29 2020 at 18:03):

Patrick Massot said:

by {  rintro h, rfl⟩, exact h rfl }

I like this one, I think it's good enough. But I was hoping that there was something slick, like maybe a fancy use of norm_cast.

view this post on Zulip Kenny Lau (Dec 29 2020 at 18:03):

import data.set.basic

lemma idiomatic {E : Type*} (s : set E) (a : E) (b : s) (ha : a  s) (h : b  a) : b  a, ha :=
subtype.ne_of_val_ne h

view this post on Zulip Patrick Massot (Dec 29 2020 at 18:04):

Using an already proven lemma is always the ultimate cheating.

view this post on Zulip Heather Macbeth (Dec 29 2020 at 18:05):

Somehow library_search doesn't find that for me?

view this post on Zulip Patrick Massot (Dec 29 2020 at 18:05):

It may be because of the negation bug in library_search

view this post on Zulip Eric Wieser (Dec 29 2020 at 22:31):

docs#subtype.ne_of_val_ne is defeq but not syntactically eq, which is probably why library_search is of no help


Last updated: May 18 2021 at 17:44 UTC