rw can't match this

Stream: general

[Kenny Lau]

@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))

[Kenny Lau]

hmm, the situation is quite complicated

[Simon Hudon]

Question?

[Kenny Lau]

I've filled in more holes

[Kenny Lau]

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))

[Kenny Lau]

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))

[Kenny Lau]

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

[Kenny Lau]

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

[Simon Hudon]

What are you trying to do?

[Kenny Lau]

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

[Simon Hudon]

What is the rule that you're using?

[Kenny Lau]

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

[Simon Hudon]

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

[Simon Hudon]

And where does to_has_mem come from?

[Kenny Lau]

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

[Kenny Lau]

(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 })

[Kenny Lau]

class has_zmem extends has_mem α α

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

[Simon Hudon]

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

[Kenny Lau]

thanks