Zulip Chat Archive

Stream: new members

Topic: Equality in `prod`


view this post on Zulip Marcus Rossel (Dec 30 2020 at 17:24):

I have a proof that (n, m) = (x, y). How can I get a proof from this, that (n = x) ∧ (m = y)?

view this post on Zulip Bryan Gin-ge Chen (Dec 30 2020 at 17:25):

You should be able to rewrite with docs#mk.inj_iff.

view this post on Zulip Sebastien Gouezel (Dec 30 2020 at 17:26):

lemma foo {α β : Type*} (x m : α) (y n : β) (h : ((x, y) : (α × β)) = (m, n)) :
  x = m  y = n :=
begin
  simpa using h,
end

view this post on Zulip Rob Lewis (Dec 30 2020 at 17:28):

More importantly, to find the answer on your own:

example {α} (a b c d : α) (h : (a, b) = (c, d)) : a = c  b = d :=
by library_search     -- prod.mk.inj h

view this post on Zulip Mario Carneiro (Dec 30 2020 at 22:47):

I would suggest cases h though

view this post on Zulip Mario Carneiro (Dec 30 2020 at 22:48):

injection h does more directly what you are looking for, but if those variables are actually variables and not expressions then cases h will perform the substitution of one for the other in your goal

view this post on Zulip Eric Wieser (Dec 30 2020 at 23:48):

Link for the lazy: tactic#injection

view this post on Zulip Marcus Rossel (Mar 05 2021 at 15:59):

I don't understand how to use injection. E.g.:

structure s :=
  (a : int)
  (b : nat)

example {x x' : s} (h : x = x') : true :=
begin
  injection h,
  -- injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor
end

So how can I add the hypothesis x.a = x'.a and x.b = x'.b?

view this post on Zulip Yakov Pechersky (Mar 05 2021 at 16:01):

Tag with ext:

@[ext]
structure s := ...

and write an ext_iff

view this post on Zulip Eric Wieser (Mar 05 2021 at 16:03):

example {x x' : s} (h : x = x') : true :=
begin
  cases x,
  cases x',
  injection h,
  sorry
end

view this post on Zulip Eric Wieser (Mar 05 2021 at 16:03):

But @Yakov Pechersky is correct that @[ext] will probably do what you're actually trying to do

view this post on Zulip Marcus Rossel (Mar 05 2021 at 16:05):

Indeed: @[ext] causes invalid definition, a declaration named 's.ext_iff' has already been declared when trying to declare it manually.

view this post on Zulip Eric Wieser (Mar 05 2021 at 16:06):

s.mk.inj is also close to what you want, and exists even without ext

view this post on Zulip Marcus Rossel (Mar 08 2021 at 18:39):

How does this work for inequalities? E.g:

@[ext] structure thing := (a : ) (b : )

example (t t' : thing) (hₙ : t  t') (hₑ : t.a = t'.a) : t.b  t'.b :=
  sorry

view this post on Zulip Johan Commelin (Mar 08 2021 at 18:41):

@Marcus Rossel

intro h,
apply_assumption,
ext,
assumption'

view this post on Zulip Johan Commelin (Mar 08 2021 at 18:41):

(I didn't test this)

view this post on Zulip Marcus Rossel (Mar 08 2021 at 18:42):

This does indeed work, but I don't understand it yet. I'll have to read up on the tactics.

view this post on Zulip Ruben Van de Velde (Mar 08 2021 at 18:46):

TIL apply_assumption (though apply hₙ might be clearer)

view this post on Zulip Johan Commelin (Mar 08 2021 at 18:52):

/me was to lazy to copy the unicode symbols (-;


Last updated: May 17 2021 at 23:14 UTC