Subtype property

Stream: general

[Floris van Doorn]

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

[Reid Barton]

How could you rewrite with it though?

[Reid Barton]

(2) also came up recently.

[Reid Barton]

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

[Reid Barton]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

If not, PR

[Reid Barton]

There's also

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

in data.subtype; are these duplicates?

[Floris van Doorn]

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

[Floris van Doorn]

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

[Reid Barton]

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

[Floris van Doorn]

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)

[Reid Barton]

I guess otherwise nothing would ever have the right form.

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Sorry.

[Yury G. Kudryashov]

UPD: no, it is defined in set/basic

[Reid Barton]

Well that might be, but it really exists!

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

Who will volunteer to do this?

[orlando]

@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

[Floris van Doorn]

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

[Mario Carneiro]

someday I will learn what it does