Zulip Chat Archive

Stream: general

Topic: Subtype property


view this post on Zulip Floris van Doorn (May 14 2020 at 22:46):

Two related questions:
(1) Does the following lemma exist somewhere?

lemma subtype.property_coe {α} {p : α  Prop} (x : subtype p) : p x := x.2

It is important that this states p x, and not p x.1, so subtype.property doesn't work (I want to rewrite with this, and have ↑x instead of x.1 in my goal).

(2) Can I tell library_search to not work up to definitional equality (of semireducible definitions)? I am often trying to look for rewrite lemmas which are proven by rfl and then library_search is "too smart" and just tells me I can prove it by rfl or iff_refl _.

view this post on Zulip Reid Barton (May 14 2020 at 22:52):

How could you rewrite with it though?

view this post on Zulip Reid Barton (May 14 2020 at 22:53):

(2) also came up recently.

view this post on Zulip Reid Barton (May 14 2020 at 22:53):

https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/List.20lemmas/near/197053059

view this post on Zulip Reid Barton (May 14 2020 at 22:54):

For (1) something would need to beta-reduce p x, right? Does rw do that?

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 22:57):

(1) If p x = x ∈ s, then we have subtype.mem.

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 22:57):

If not, PR

view this post on Zulip Reid Barton (May 14 2020 at 23:01):

There's also

@[simp] lemma val_prop' {S : set α} (a : {a // a  S}) : a  S := a.property

in data.subtype; are these duplicates?

view this post on Zulip Floris van Doorn (May 14 2020 at 23:02):

In my example I had something like this:

import linear_algebra.basic

universe variables v w
variables {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (π : M [R] M)
example (x : π.ker) : π x = 0 :=
begin
  rw [linear_map.mem_ker.mp x.2] -- error: did not find ⇑π x.val
end

view this post on Zulip Floris van Doorn (May 14 2020 at 23:03):

I realized I could have redefined something earlier to get the more convenient hypothesis x ∈ π.ker.

view this post on Zulip Reid Barton (May 14 2020 at 23:03):

Oh I see, there is something between rw and the property.

view this post on Zulip Floris van Doorn (May 14 2020 at 23:05):

And yes, rw beta-reduces:

lemma subtype.prop {α} {p : α  Prop} (x : subtype p) : p x := x.2

example (z : ) (x : subtype (λ y, y = z)) : z = x :=
begin
  rw [x.prop]
end

(using x.2 doesn't work)

view this post on Zulip Reid Barton (May 14 2020 at 23:06):

I guess otherwise nothing would ever have the right form.

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 23:09):

I think that I wrote subtype.mem because I'd want it to have this name.

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 23:09):

Sorry.

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 23:09):

UPD: no, it is defined in set/basic

view this post on Zulip Reid Barton (May 14 2020 at 23:09):

Well that might be, but it really exists!

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 23:11):

I think that it should be moved to data.subtype, val_prop' should be removed, and coe_prop should be added.

view this post on Zulip Yury G. Kudryashov (May 14 2020 at 23:29):

Who will volunteer to do this?

view this post on Zulip orlando (May 14 2020 at 23:53):

@Floris van Doorn :

import linear_algebra.basic

universe variables v w
variables {R : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M] (π : M [R] M)
example (x : π.ker) : π x = 0 :=
begin
  erw [linear_map.mem_ker.mp x.2] --  i think erw work in some case
end

view this post on Zulip Floris van Doorn (May 15 2020 at 16:25):

I tend to forget that erewrite is a thing. That is a good to remember as back-up plan.

view this post on Zulip Mario Carneiro (May 15 2020 at 16:25):

someday I will learn what it does


Last updated: May 12 2021 at 04:19 UTC