Zulip Chat Archive

Stream: general

Topic: rw can't match this


view this post on Zulip Kenny Lau (Mar 15 2018 at 20:10):

@has_mem.mem.{u u} α α
    (@zfc.has_zmem.to_has_mem.{u} α (@zfc.has_comprehension.to_has_zmem.{u} α has_comprehension))
    ?m_1
    (@zfc.comprehension.{u} α has_comprehension ?m_2 ?m_3)
@has_mem.mem.{u u} α α (@zfc.has_zmem.to_has_mem.{u} α (@zfc.has_zmem.mk.{u} α to_has_mem)) x
    (@zfc.comprehension.{u} α has_comprehension infinity (λ (x : α), false))

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:11):

hmm, the situation is quite complicated

view this post on Zulip Simon Hudon (Mar 15 2018 at 20:12):

Question?

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:13):

I've filled in more holes

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:13):

now rw can't match this:

@has_mem.mem.{u u} α α
    (@zfc.has_zmem.to_has_mem.{u} α (@zfc.has_comprehension.to_has_zmem.{u} α has_comprehension))
    x
    (@zfc.comprehension.{u} α has_comprehension infinity (λ (x : α), false))

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:13):

where the goal contains:

@has_mem.mem.{u u} α α (@zfc.has_zmem.to_has_mem.{u} α (@zfc.has_zmem.mk.{u} α to_has_mem)) x
    (@zfc.comprehension.{u} α has_comprehension infinity (λ (x : α), false))

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:14):

If I'm analyzing correctly, it would be a failure to match this with this:

@zfc.has_comprehension.to_has_zmem.{u} α has_comprehension
@zfc.has_zmem.mk.{u} α to_has_mem

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:14):

@Simon Hudon question: do you see any way to fix it?

view this post on Zulip Simon Hudon (Mar 15 2018 at 20:15):

What are you trying to do?

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:16):

rewrite hx : x ∈ comprehension infinity (λ (x : α), false)

view this post on Zulip Simon Hudon (Mar 15 2018 at 20:17):

What is the rule that you're using?

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:18):

∀ A p x, x ∈ comprehension A p ↔ x ∈ A ∧ p x

view this post on Zulip Simon Hudon (Mar 15 2018 at 20:20):

Why do you have (@zfc.has_zmem.mk.{u} α to_has_mem)?

view this post on Zulip Simon Hudon (Mar 15 2018 at 20:21):

And where does to_has_mem come from?

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:21):

I'm in the middle of a structure doing things like this

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:21):

(has_zempty : has_zempty α :=
  { emptyc := @@comprehension has_comprehension infinity (λ x, false),
    empty_not_zmem := λ x hx, begin simp [∅] at hx, rw [@@zmem_comprehension_iff has_comprehension infinity (λ (x : α), false) x] at hx, end })

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:22):

class has_zmem extends has_mem α α

class has_zempty extends has_zmem α, has_emptyc α :=
(empty_not_zmem : ∀ x, x ∉ (∅:α))

view this post on Zulip Simon Hudon (Mar 15 2018 at 20:22):

Try extracting

{ emptyc := @@comprehension has_comprehension infinity (λ x, false),
    empty_not_zmem := λ x hx, begin simp [] at hx, rw [@@zmem_comprehension_iff has_comprehension infinity (λ (x : α), false) x] at hx, end })

into a separate definition

view this post on Zulip Kenny Lau (Mar 15 2018 at 20:29):

thanks


Last updated: May 13 2021 at 18:26 UTC