Zulip Chat Archive

Stream: new members

Topic: Weird behavior of rw?


view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 17:48):

I'm trying to shorten the following proof:

lemma sqr_roots_one (x : ℝ) (p : x ^ 2 = 1) : x = 1 ∨ x = -1 := begin
cases le_total x 0,
right,
rw [neg_eq_iff_neg_eq.1],
rw [← sqrt_sqr (neg_le_neg h), pow_two, neg_mul_neg, ← pow_two, p, sqrt_one],
left, rw [← sqrt_sqr h, p, sqrt_one],
end

But when I try to combine the two adjacent rw tactics into one it doesn't work.

view this post on Zulip Chris Hughes (Sep 29 2018 at 17:55):

That's because rw [neg_eq_iff_neg_eq.1], solved your goal, but created a new one. rw [eq_neg_iff_eq_neg], should allow you to merge the goals.
Incidentally, here's the shortest proof

lemma sqr_roots_one (x : ) (p : x ^ 2 = 1) : x = 1  x = -1 :=
by rwa [pow_two, mul_self_eq_one_iff] at p

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 17:57):

Lol I feel like I searched for everything except mul_self :oh_no:

view this post on Zulip Johan Commelin (Sep 29 2018 at 18:00):

lemma sqr_roots_one (x : ) (p : x ^ 2 = 1) : x = 1  x = -1 :=
by rwa [mul_self_eq_one_iff, pow_two]

view this post on Zulip Chris Hughes (Sep 29 2018 at 18:02):

I think this is one area the library isn't entirely consistent. There's a mix of pow_two and mul_self.

view this post on Zulip Scott Olson (Sep 29 2018 at 18:05):

For the record I found this way that lets you write the original with a merged rw:

lemma sqr_roots_one (x : ) (p : x ^ 2 = 1) : x = 1  x = -1 := begin
cases le_total x 0,
right,
symmetry,
rw [neg_eq_iff_neg_eq,  sqrt_sqr (neg_le_neg h), pow_two, neg_mul_neg,  pow_two, p, sqrt_one],
left, rw [ sqrt_sqr h, p, sqrt_one],
end

view this post on Zulip Scott Olson (Sep 29 2018 at 18:08):

(Didn't work without symmetry first because of the way neg_eq_iff_neg_eq is written)

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 19:08):

This is probably a stupid question but how do I prove 2 \neq 0 in \com ?

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 19:09):

I noticed there is a theorem two_ne_zero that sounded promising but doesn't seem to work

view this post on Zulip Chris Hughes (Sep 29 2018 at 19:12):

I think it's two_ne_zero'. Not a stupid question.

view this post on Zulip Sebastian Zimmer (Sep 29 2018 at 19:20):

Thanks that worked. What is the difference between two_ne_zero and two_ne_zero'?

view this post on Zulip Scott Olson (Sep 29 2018 at 19:49):

Different typeclass requirements, I guess:

#check @two_ne_zero
-- two_ne_zero : ∀ {α : Type u_1} [_inst_1 : linear_ordered_field α], 2 ≠ 0

#check @two_ne_zero'
-- two_ne_zero' : ∀ {α : Type u_1} [_inst_1 : add_monoid α] [_inst_2 : has_one α] [_inst_3 : char_zero α], 2 ≠ 0

view this post on Zulip Chris Hughes (Sep 29 2018 at 19:55):

It's a core thing. Every linear ordered field has characteristic zero, but two_ne_zero is in core, so it can't be changed, and therefore we need a version for char_zero as well.


Last updated: May 15 2021 at 22:14 UTC