Zulip Chat Archive

Stream: new members

Topic: a ∈ tt_ctx → b ∉ tt_ctx → a ≠ b


view this post on Zulip Guilherme Espada (Mar 11 2021 at 19:18):

Where tt_ctx is a finmap.

I'm guessing this is done with congruence, however, I don't know the exact procedure to solve this, and library_search doesn't find anything (maybe I'm stating it wrong?)

view this post on Zulip Ruben Van de Velde (Mar 11 2021 at 19:24):

rintros ha hb rfl, contradicton

view this post on Zulip Ruben Van de Velde (Mar 11 2021 at 19:25):

Or longer, intros ha hb heq, rw heq at ha, exact hb ha,

view this post on Zulip Guilherme Espada (Mar 11 2021 at 19:33):

First version works, but what does the rfl at the end do?
(the second version doesn't seem to work on my end)

view this post on Zulip Eric Wieser (Mar 11 2021 at 19:34):

It rewrites with a=b

view this post on Zulip Ruben Van de Velde (Mar 11 2021 at 19:36):

Try now - I was rewriting in the wrong direction. rintro rfl does intro heq, subst a

view this post on Zulip Guilherme Espada (Mar 11 2021 at 19:41):

Thank you! now I understand it!

view this post on Zulip Marcus Rossel (Mar 12 2021 at 09:25):

ne_of_mem_of_not_mem


Last updated: May 08 2021 at 04:14 UTC