Zulip Chat Archive

Stream: new members

Topic: rw duplicates an hypothesis


view this post on Zulip Riccardo Brasca (Nov 22 2020 at 15:37):

In the following example

import ring_theory.roots_of_unity
import field_theory.minimal_polynomial

variables {K : Type*} [field K] {n : } {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n)

open polynomial

include n μ h hpos

lemma primitive_root_is_integral : is_integral  μ := sorry

lemma test (hn : n = 1) : minimal_polynomial (primitive_root_is_integral h hpos) = X - 1 :=
begin
  rw hn at h, --it creates another h
  simp at h, --now the second h is μ = 1
  sorry,
end

when I use rw hn at h, it creates a new hypothesis h, keeping also the old one. I think because h is hidden in the goal, that is displayed as minimal_polynomial _ = X - 1. In any case I don't know how to use this, rw h doesn't work. I also created a new hypothesis muone : μ = 1 to be sure that I am using the correct one, but rw muone says

rewrite tactic failed, motive is not type correct
  λ (_a : K), minimal_polynomial _ = X - 1 = (minimal_polynomial _ = X - 1)

How can I use that μ = 1? Thank you!

Note that I know how to prove that the minimal polynomial of 1 : K is X - 1, that's not the problem.

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 15:44):

subst hn might work, as might simp [hn] at *. But they might not (I'm not at a computer right now)

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 15:44):

You're right that lean demands that h is preserved because it's in the goal

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 15:48):

when you get that motive error, simplest work around is to use simp_rw

view this post on Zulip Filippo A. E. Nuccio (Nov 22 2020 at 15:48):

So what you want to prove is that the minimal polynomial of the 11-st root of unity is X-1 right?

view this post on Zulip Riccardo Brasca (Nov 22 2020 at 15:49):

subst does exactly what I want, thank you @Kevin Buzzard ! I have to understand what is the difference between rw and subs...

view this post on Zulip Filippo A. E. Nuccio (Nov 22 2020 at 15:51):

and how do you close the goal, finally?

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 15:51):

subst hn says "completely rip out n from the entire local context all in one go and replace all occurrences with 1". rw hn at h rewrites only at h, and then tries to clear the old h but the clear fails because h is still being used somewhere.

view this post on Zulip Riccardo Brasca (Nov 22 2020 at 15:52):

@Filippo A. E. Nuccio The point is that I need to prove it stated like that (it is indeed one step in a more interesting lemma, and morally the easy step, I was surprised to get stuck on it).

view this post on Zulip Filippo A. E. Nuccio (Nov 22 2020 at 15:52):

Riccardo Brasca said:

Filippo A. E. Nuccio The point is that I need to prove it stated like that (it is indeed one step in a more interesting lemma, and morally the easy step, I was surprised to get stuck on it).

Yes, yes, I got that: I was trying to understand the statement. But I got that your point was about rw versus subst. At any rate, how do you finish with @Kevin Buzzard 's suggestion?

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 15:53):

Yakov's suggestion works in situations where the subst trick doesn't, because the subst trick only works if the hypothesis is <variable> = ... or ... = <variable>

view this post on Zulip Riccardo Brasca (Nov 22 2020 at 15:55):

simp_rw hn at h has the same effect as rw hn at h, it creates another h.

view this post on Zulip Riccardo Brasca (Nov 22 2020 at 15:56):

simp_rw muone indeed does not give any error, and the goal becomes minimal_polynomial _ = X - 1. If I go on the underscore VS Code says λ {x : K}, is_integral ℤ x, that confuses me...

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 15:57):

Nothing wrong with having another h

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 15:58):

The simplified h will be after the unsimplified one, so it will be the one lean uses in rewrites etc

view this post on Zulip Filippo A. E. Nuccio (Nov 22 2020 at 15:59):

Riccardo Brasca said:

simp_rw muone indeed does not give any error, and the goal becomes minimal_polynomial _ = X - 1. If I go on the underscore VS Code says λ {x : K}, is_integral ℤ x, that confuses me...

This happened also with your code, no? Well, at least the first part

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 15:59):

You can also make a new hypothesis with "have newh : is_primitive_root mu 1 := by..."

view this post on Zulip Kevin Buzzard (Nov 22 2020 at 15:59):

You should maybe rewrite at h |-

view this post on Zulip Yakov Pechersky (Nov 22 2020 at 16:00):

You'll also need to rw at hpos

view this post on Zulip Riccardo Brasca (Nov 22 2020 at 16:14):

Maybe I am confused, but it seems that subst is the only way I found to make μ disappears (replaced by 1) from the goal.

import ring_theory.roots_of_unity
import field_theory.minimal_polynomial

variables {K : Type*} [field K] {n : } {μ : K} (h : is_primitive_root μ n) (hpos : 0 < n)

open polynomial

include n μ h hpos

lemma primitive_root_is_integral : is_integral  μ := sorry

lemma test (hn : n = 1) : minimal_polynomial (primitive_root_is_integral h hpos) = X - 1 :=
begin
  have muone : μ = 1 := sorry,
--  simp_rw muone, --goal says λ {x : K}, is_integral ℤ x
--  subst muone, --goal says is_integral ℤ 1
end

view this post on Zulip Filippo A. E. Nuccio (Nov 22 2020 at 16:16):

But how do you intend to prove the result? I still haven't understood the problem with two h

view this post on Zulip Riccardo Brasca (Nov 22 2020 at 16:19):

The two h was not a real problem, just something looked weird to me. Once the goal becomes to prove that the minimal polynomial of 1 is X - 1 it's OK, see #5062. The problem was that I wasn't able to modify the goal, even knowing μ = 1, the goal was still about the minimal polynomial of μ.

view this post on Zulip Filippo A. E. Nuccio (Nov 22 2020 at 16:19):

Ah, I see now.


Last updated: May 16 2021 at 21:11 UTC