Zulip Chat Archive

Stream: general

Topic: An error that appears after the last goal is proved


Riccardo Brasca (Nov 22 2021 at 10:51):

I am proving the following lemma

import ring_theory.adjoin.basic

variables (A B : Type*) [comm_ring A] [comm_ring B] [algebra A B]

open algebra

example (b : (adjoin A {b : B |  (n : ), b ^ n = 1})) :  b 
  adjoin A {b : (adjoin A {b : B |  (n : ), b ^ n = 1}) |  (n : ), b ^ n = 1} :=
begin
  cases b with b hb,
  refine adjoin_induction hb (λ b₁ hb₁, subset_adjoin _) (λ a, _) (λ x y hx hy, _)
    ((λ x y hx hy, _)),
  { obtain n, hn := hb₁,
    refine n, _⟩,
    simp only [ subalgebra.coe_eq_one, subalgebra.coe_pow],
    convert hn },
  { convert subalgebra.algebra_map_mem _ a,
    apply subtype.ext,
    simpa only [subalgebra.coe_algebra_map] },
  { convert subalgebra.add_mem _ hx hy,
    apply subtype.ext,
    simpa only [subalgebra.coe_add] },
  { convert subalgebra.mul_mem _ hx hy,
    apply subtype.ext,
    --the goal is ↑⟨x * y, hb⟩ = ↑(⟨x, hb⟩ * ⟨y, hb⟩), that can be proved by simpa only [subalgebra.coe_mul]
    }
end

The infoview shows me the last goal normally, but if I prove it, I get the error

type mismatch at application
  _x, hb
term
  hb
has type
  b  adjoin A {b : B |  (n : ), b ^ n = 1}
but is expected to have type
  (λ (x : B), x  adjoin A {b : B |  (n : ), b ^ n = 1}) _x

The infoview says the error is happening in line 7, that is the line with the statement (that was fine before the last goal was proved). Note that the same happens with any of the four goals produced by adjoin_induction: when I prove the last one I get the error. The same happens if I put sorry as proof of all the goals.

I've never seen such a behavior, so I don't really know what to do.

I agree that the statement of the lemma is weird, so let me add some context before people say "replace b : ↥(adjoin A {b : B | ∃ (n : ℕ), b ^ n = 1}) in the statement with (b : B) (hb : b ∈ (adjoin A {b : B | ∃ (n : ℕ), b ^ n = 1}))". What I really want to prove is that if B is the cyclotomic extension of A given by roots of unity of order T : set ℕ+ and S ⊆ T, then adjoin A { b : B | ∃ a : ℕ+, a ∈ S ∧ b ^ (a : ℕ) = 1 } is a cyclotomic extension of A given by roots of order S, so this is the real proof that doesn't work.

Kevin Buzzard (Nov 22 2021 at 10:56):

Yeah I've never seen that before. I wondered whether you had too many b's (i.e. you weren't proving what you thought you were proving, or something?) but I've changed a few and the error remains.

Kevin Buzzard (Nov 22 2021 at 10:58):

Maybe you've found a bug in a tactic?

Gabriel Ebner (Nov 22 2021 at 11:00):

This is typically the result of a buggy tactic. See for example https://github.com/leanprover-community/mathlib/issues/9805 for another interesting example. What happens is that the tactic produces a buggy proof term and Lean only notices this at the end when the kernel goes over the proof again.

Riccardo Brasca (Nov 22 2021 at 11:05):

Thank's. Using @adjoin_induction... the proof doesn't work anymore, so maybe I can just fix it. Let me see.

Riccardo Brasca (Nov 22 2021 at 11:14):

I think the problem comes from adjoin_induction: the initial goal, after cases b with b hb, is ⟨b, hb⟩ ∈ ... and so it's not exactly a goal about b. I don't know which p : B → Prop Lean decides to use in adjoin_induction (since there is no hb for a general b : B) but the bug (if there is one) is just the fact that it doesn't say immediately that there is a problem.

Kevin Buzzard (Nov 22 2021 at 11:33):

Here's a more minimised example:

import ring_theory.adjoin.basic

variables (A B : Type*) [comm_ring A] [comm_ring B] [algebra A B]

open algebra

example (b : (adjoin A {b : B |  (n : ), b ^ n = 1})) :  b 
  adjoin A {b : (adjoin A {b : B |  (n : ), b ^ n = 1}) |  (n : ), b ^ n = 1} :=
begin
  cases b with b hb,
  refine adjoin_induction hb (λ b₁ hb₁, subset_adjoin _) (λ a, _) (λ x y hx hy, _)
    ((λ x y hx hy, _)),
  sorry, sorry, sorry, sorry,
end

Kevin Buzzard (Nov 22 2021 at 11:44):

example (b : (adjoin A {b : B |  (n : ), b ^ n = 1})) :  b 
  adjoin A {b : (adjoin A {b : B |  (n : ), b ^ n = 1}) |  (n : ), b ^ n = 1} :=
begin
  cases b with b hb,
  exact adjoin_induction hb sorry sorry sorry sorry,
end

Kevin Buzzard (Nov 22 2021 at 11:50):

Dunno if this helps. @Riccardo Brasca is this the proof you expect to work? I tried to rephrase it (changing the lean but not the maths) and I broke a convert. The goal doesn't look true :-/

example (b : (adjoin A {b : B |  (n : ), b ^ n = 1})) :  b 
  adjoin A {b : (adjoin A {b : B |  (n : ), b ^ n = 1}) |  (n : ), b ^ n = 1} :=
begin
  cases b with b hb,
  let foo := (⟨b, hb : (adjoin A {b : B |  (n : ), b ^ n = 1})),
  convert (adjoin_induction hb (λ b₁ hb₁, _) (λ a, _) (λ x y hx hy, _) ((λ x y hx hy, _)) :
    foo  adjoin A {b : (adjoin A {b : B |  (n : ), b ^ n = 1}) |  (n : ), b ^ n = 1}),
  { obtain n, hn := hb₁,
    refine subset_adjoin n, _⟩,
    simp only [ subalgebra.coe_eq_one, subalgebra.coe_pow],
    convert hn, -- this closes the goal in the original proof
    sorry },
  { sorry },
  { sorry },
  { sorry }
end

Kevin Buzzard (Nov 22 2021 at 11:53):

example (b : (adjoin A {b : B |  (n : ), b ^ n = 1})) :  b 
  adjoin A {b : (adjoin A {b : B |  (n : ), b ^ n = 1}) |  (n : ), b ^ n = 1} :=
begin
  --cases b with b hb,
  refine adjoin_induction b.2 (λ b₁ hb₁, subset_adjoin _) (λ a, _) (λ x y hx hy, _)
    ((λ x y hx hy, _)),
  { obtain n, hn := hb₁,
    refine n, _⟩,
    simp only [ subalgebra.coe_eq_one, subalgebra.coe_pow],
    convert hn, -- no longer works
    sorry },
...

Kevin Buzzard (Nov 22 2021 at 11:54):

If you don't do the cases but just use b.1 and b.2, the proof breaks earlier. Is there a mathematical problem with the proof?

Riccardo Brasca (Nov 22 2021 at 11:57):

I now think that adjoin_induction is not the right strategy to prove the result, at least not directly: after cases we have b: B and hb : b ∈ adjoin A {b : B | ∃ (n : ℕ), b ^ n = 1} and the goal concerns both b and hb. Now, adjoin_induction acts on b, but keep the original hb, so it doesn't work.

Riccardo Brasca (Nov 22 2021 at 11:58):

I am not sure what is the best solution: find a different proof or make adjoin_induction act on hb too somehow.

Yakov Pechersky (Nov 22 2021 at 12:00):

What does the b on the RHS of the condition in the set builder in the starting goal refer to? I don't mean mathematically, but to Lean? The mwe might be clearer if there are more variable names and fewer possible name shadowing.

Riccardo Brasca (Nov 22 2021 at 12:01):

Voilà.

import ring_theory.adjoin.basic

variables (A B : Type*) [comm_ring A] [comm_ring B] [algebra A B]

open algebra

example (b : (adjoin A {β : B |  (n : ), β ^ n = 1})) :  b 
  adjoin A {β₁ : (adjoin A {β₂ : B |  (n : ), β₂ ^ n = 1}) |  (n : ), β₁ ^ n = 1} :=
begin
  cases b with b hb, --goal is ⟨b, hb⟩ ∈ adjoin A {β₁ : ↥(adjoin A {β₂ : B | ∃ (n : ℕ), β₂ ^ n = 1}) | ∃ (n : ℕ), β₁ ^ n = 1}
  exact adjoin_induction hb sorry sorry sorry sorry,
end

Yakov Pechersky (Nov 22 2021 at 12:01):

docs#algebra.adjoin_induction

Chris Birkbeck (Nov 22 2021 at 12:06):

When I was looking at this I wondered if maybe we should prove that adjoin is "idempotent" i.e. adjoin (adjoin A S) S = adjoin A S , but this isn't true as written as the algebra structures get messed up. But it felt like something like this is what we want. That said, this is probably just as annoying to prove

Yakov Pechersky (Nov 22 2021 at 12:11):

One issue is that the induction is proving something solely about b (inferring from hb) but the goal is about a subtype whose value is b. Do you have lemmas that simplify or change goals that are about being mem of adjoin of a subtype?

Riccardo Brasca (Nov 22 2021 at 12:12):

I am looking for them since 30 minutes. Is the following true?

import data.set.basic

example (ι : Type*) (S : set ι) (T : set S) (i : ι) (hi : i  S) (t : S) (ht : t  T)
  (hti : t = i) : (⟨i, hi : S)  T := sorry

Riccardo Brasca (Nov 22 2021 at 12:13):

I don't even care about adjoin (at least, not now), I don't know how to work with members of set of a subtype.

Riccardo Brasca (Nov 22 2021 at 12:15):

rw [← hti], says rewrite tactic failed, motive is not type correct λ (_a : ι), ⟨i, hi⟩ ∈ T = (⟨_a, hi⟩ ∈ T). That usually means I am missing something.

Riccardo Brasca (Nov 22 2021 at 12:16):

Mmm, simp [← hti, ht], proves it.

Riccardo Brasca (Nov 22 2021 at 12:22):

The point is that in the following

example (ι : Type*) (S : set ι) (i : ι) (hi : i  S) (T : set S) (H :  t  T, t = i) : (⟨i, hi : S)  T :=
begin
  obtain t, ht, hti := H,
  simp [ hti, ht],
end

in H there is no mention of hi, so it can (maybe) proved using adjoin_induction. I am trying.

Riccardo Brasca (Nov 22 2021 at 12:23):

Indeed no errors in

example (b : (adjoin A {β : B |  (n : ), β ^ n = 1})) :  b 
  adjoin A {β₁ : (adjoin A {β₂ : B |  (n : ), β₂ ^ n = 1}) |  (n : ), β₁ ^ n = 1} :=
begin
  cases b with b hb,
  suffices :  x  adjoin A {β₁ : (adjoin A {β₂ : B |  (n : ), β₂ ^ n = 1}) |
     (n : ), β₁ ^ n = 1}, x = b,
  { obtain x, hx, hxb := this,
    simp [ hxb, hx] },
  exact adjoin_induction hb sorry sorry sorry sorry,
end

But still four sorry :)

Kevin Buzzard (Nov 22 2021 at 12:25):

Oh nice! This feels like progress. With your earlier question, ⟨i, hi⟩ and t are equal because all proofs of a proposition are defeq. This works:

example (ι : Type*) (S : set ι) (T : set S) (i : ι) (hi : i  S) (t : S) (ht : t  T)
  (hti : t = i) : (⟨i, hi : S)  T :=
begin
  cases t,
  convert ht,
  exact hti.symm,
end

Kevin Buzzard (Nov 22 2021 at 12:26):

docs#subtype.eq

Kevin Buzzard (Nov 22 2021 at 12:27):

example (ι : Type*) (S : set ι) (T : set S) (i : ι) (hi : i  S) (t : S) (ht : t  T)
  (hti : t = i) : (⟨i, hi : S)  T :=
begin
  cases t,
  subst hti,
  exact ht,
end

subst is a really cool tactic.

Riccardo Brasca (Nov 22 2021 at 12:57):

This works

import ring_theory.adjoin.basic

variables (A B : Type*) [comm_ring A] [comm_ring B] [algebra A B]

open algebra

example (b : (adjoin A {β : B |  (n : ), β ^ n = 1})) :  b 
  adjoin A {β₁ : (adjoin A {β₂ : B |  (n : ), β₂ ^ n = 1}) |  (n : ), β₁ ^ n = 1} :=
begin
  cases b with b hb,
  suffices :  x  adjoin A {β₁ : (adjoin A {β₂ : B |  (n : ), β₂ ^ n = 1}) |
     (n : ), β₁ ^ n = 1}, x = b,
  { obtain x, hx, hxb := this,
    simp [ hxb, hx] },
  refine adjoin_induction hb (λ b₁ hb₁, _) (λ a, _) (λ b₁ b₂, _) (λ b₁ b₂, _),
  { obtain n, hb₁ := hb₁,
    refine ⟨⟨b₁, subset_adjoin n, hb₁⟩⟩, _⟩,
    simp only [exists_prop, and_true, eq_self_iff_true, subtype.coe_mk],
    refine subset_adjoin n, _⟩,
    rw [ subalgebra.coe_eq_one, subalgebra.coe_pow],
    convert hb₁ },
  { refine ⟨⟨algebra_map A B a, subalgebra.algebra_map_mem _ _⟩, _⟩,
    simp only [exists_prop, set_like.coe_mk, and_true, eq_self_iff_true],
    convert subalgebra.algebra_map_mem _ a },
  { simp only [and_imp, exists_prop, forall_exists_index],
    intros x hxmem hxb y hymem hyb,
    refine ⟨⟨x + y, subalgebra.add_mem _ (by simp) (by simp)⟩, _, _⟩⟩,
    { simp_rw [ subalgebra.coe_add],
      exact subalgebra.add_mem _ hxmem hymem },
    { simp_rw [hxb, hyb],
      refl } },
  { simp only [and_imp, exists_prop, forall_exists_index],
    intros x hxmem hxb y hymem hyb,
    refine ⟨⟨x * y, subalgebra.mul_mem _ (by simp) (by simp)⟩, _, _⟩⟩,
    { simp_rw [ subalgebra.coe_mul],
      exact subalgebra.mul_mem _ hxmem hymem },
    { simp_rw [hxb, hyb],
      refl } }
end

Riccardo Brasca (Nov 22 2021 at 12:58):

@Chris Birkbeck if you find a reasonable way to state that adjoin is idempotent I think that a similar proof should work too.

Chris Birkbeck (Nov 22 2021 at 12:59):

Yeah let me think about how to state it properly.

Riccardo Brasca (Nov 22 2021 at 13:00):

But I agree that it is a pain

Yakov Pechersky (Nov 22 2021 at 14:23):

import ring_theory.adjoin.basic

variables {A : Type*} [comm_semiring A] {S : set A}

open algebra

example {x : A} : x  adjoin (adjoin A S) S  x  adjoin A S :=
begin
  split,
  { intro hx,
    refine adjoin_induction hx _ _ _ _,
    { intros y hy,
      exact subalgebra.algebra_map_mem _ _ },
    { rintro r, hr⟩,
      exact subalgebra.algebra_map_mem _ _ },
    { intros x y,
      exact subalgebra.add_mem _ },
    { intros x y,
      exact subalgebra.mul_mem _ } },
  { intro hx,
    refine adjoin_induction hx _ _ _ _,
    { intros y hy,
      let y' : adjoin A S := y, subalgebra.algebra_map_mem _ _⟩,
      exact subalgebra.algebra_map_mem _ y' },
    { intro r,
      let r' : adjoin A S := r, subalgebra.algebra_map_mem _ _⟩,
      exact subalgebra.algebra_map_mem _ r' },
    { intros x y,
      exact subalgebra.add_mem _ },
    { intros x y,
      exact subalgebra.mul_mem _ } }
end

Yakov Pechersky (Nov 22 2021 at 14:23):

If I understood the desiratum correctly

Yakov Pechersky (Nov 22 2021 at 14:28):

Ah, it needs to be:

variables {A B : Type*} [comm_semiring A] [comm_semiring B] [algebra A B] {S : set B}

open algebra

lemma adjoin_idem {x : B} : x  adjoin (adjoin A S) S  x  adjoin A S :=

Yakov Pechersky (Nov 22 2021 at 14:28):

Right?

Chris Birkbeck (Nov 22 2021 at 14:35):

Ah yes that would work! I was trying to figure out how to state it as an equality of subalgebras, but element-wise would be enough

Chris Birkbeck (Nov 22 2021 at 15:05):

Here is a proof (I cheated and used some tidy's as you'll see):

variables {A B : Type*} [comm_semiring A] [comm_semiring B] [algebra A B] {S : set B}

open algebra

lemma adjoin_idem {x : B} : x  adjoin (adjoin A S) S  x  adjoin A S :=
begin
  split,
  { intro hx,
    refine adjoin_induction hx _ _ _ _,
    { intros y hy,
      intros t H, cases H, induction H_h, intros t_1 H, cases H, induction H_h, dsimp at *, simp at *, cases H_w_1, solve_by_elim,},
    { rintro r, hr⟩,
      assumption, },
    { intros x y,
      exact subalgebra.add_mem _ },
    { intros x y,
      exact subalgebra.mul_mem _ } },
  { intro hx,
    refine adjoin_induction hx _ _ _ _,
    { intros y hy,
    intros t H, cases H, induction H_h, intros t_1 H, cases H, induction H_h, dsimp at *, simp at *, cases H_w_1, solve_by_elim, },
    { intro r,
     let r' := algebra_map A (adjoin A s) r,
      exact subalgebra.algebra_map_mem _ r'},
    { intros x y,
      exact subalgebra.add_mem _ },
    { intros x y,
      exact subalgebra.mul_mem _ } }
end

Chris Birkbeck (Nov 22 2021 at 15:27):

Ah actually maybe this isn't enough (at least no immediately), since its not the same S in both cases for this goal.

Yakov Pechersky (Nov 22 2021 at 15:27):

Something like this?

lemma adjoin_idem' {x : adjoin A S} :
  x  adjoin A {b : adjoin A S | (b : B)  S}  (x : B)  adjoin A S :=

Yakov Pechersky (Nov 22 2021 at 15:28):

lemma adjoin_idem' {x : adjoin A S} :
  x  adjoin A {b : adjoin A S | (b : B)  S}  (x : B)  adjoin A S :=
begin
  split,
  { intro hx,
    refine adjoin_induction hx _ _ _ _,
    { rintro y hy _ R, rfl⟩,
      rintro _ hR, rfl⟩,
      simp only [set.union_subset_iff, set.mem_set_of_eq] at hR,
      simpa using hR.right hy },
    { sorry },
    { intros x y,
      exact subalgebra.add_mem _ },
    { intros x y,
      exact subalgebra.mul_mem _ } },
  { intro hx,
    refine adjoin_induction hx _ _ _ _,
    { rintro y hy _ R, rfl⟩,
      rintro _ hR, rfl⟩,
      simp only [set.union_subset_iff, set.mem_set_of_eq] at hR,
      sorry },
    { intro r,
      sorry },
    { intros x y,
      simp },
    { intros x y,
      simp } }
end

example (b : (adjoin A {β : B |  (n : ), β ^ n = 1})) :  b 
  adjoin A {β₁ : (adjoin A {β₂ : B |  (n : ), β₂ ^ n = 1}) |  (n : ), β₁ ^ n = 1} :=
begin
  convert adjoin_idem'.mpr _,
  { simp [subtype.ext_iff] },
  { exact b.prop }
end

Riccardo Brasca (Nov 22 2021 at 15:32):

If you want to play with the real life theorem, it is here.

Riccardo Brasca (Nov 22 2021 at 15:32):

It is sorry free, but it can surely be golfed.

Chris Birkbeck (Nov 22 2021 at 17:02):

Yakov Pechersky said:

lemma adjoin_idem' {x : adjoin A S} :
  x  adjoin A {b : adjoin A S | (b : B)  S}  (x : B)  adjoin A S :=
begin
  split,
  { intro hx,
    refine adjoin_induction hx _ _ _ _,
    { rintro y hy _ R, rfl⟩,
      rintro _ hR, rfl⟩,
      simp only [set.union_subset_iff, set.mem_set_of_eq] at hR,
      simpa using hR.right hy },
    { sorry },
    { intros x y,
      exact subalgebra.add_mem _ },
    { intros x y,
      exact subalgebra.mul_mem _ } },
  { intro hx,
    refine adjoin_induction hx _ _ _ _,
    { rintro y hy _ R, rfl⟩,
      rintro _ hR, rfl⟩,
      simp only [set.union_subset_iff, set.mem_set_of_eq] at hR,
      sorry },
    { intro r,
      sorry },
    { intros x y,
      simp },
    { intros x y,
      simp } }
end

example (b : (adjoin A {β : B |  (n : ), β ^ n = 1})) :  b 
  adjoin A {β₁ : (adjoin A {β₂ : B |  (n : ), β₂ ^ n = 1}) |  (n : ), β₁ ^ n = 1} :=
begin
  convert adjoin_idem'.mpr _,
  { simp [subtype.ext_iff] },
  { exact b.prop }
end

Ok this works, so I just need to make it sorry-free...

Reid Barton (Nov 22 2021 at 17:11):

Isn't this all some Galois insertion thing? (According to the docstring, adjoin A S is the smallest A-algebra containing S, so an A-algebra contains adjoin A S iff it contains S and therefore adjoin A (adjoin A S) = adjoin A S)
If you want to prove it manually, seems a better strategy is docs#algebra.adjoin_le_iff not induction

Chris Birkbeck (Nov 22 2021 at 17:12):

The issue is that adjoin (adjoin A S) S= adjoin A S isnt quite true as the algebra structures dont match. One is an A-algebra while the other is an adjoin A S-algebra.

Chris Birkbeck (Nov 22 2021 at 17:15):

Ah but maybe what you wrote is different to what I'm thinking of.

Reid Barton (Nov 22 2021 at 17:16):

Aha I didn't notice you were talking about a different thing

Chris Birkbeck (Nov 22 2021 at 17:17):

Hm yeah, but can't figure out if what you're suggesting would work.

Chris Birkbeck (Nov 22 2021 at 17:18):

Maybe it does and I'm just being slow

Reid Barton (Nov 22 2021 at 17:18):

The original question only contains things of the form adjoin A _

Chris Birkbeck (Nov 22 2021 at 17:20):

Good point! let me see if this works

Chris Birkbeck (Nov 22 2021 at 19:42):

Riccardo Brasca said:

If you want to play with the real life theorem, it is here.

Ok so I got the other version working. But its more like I anti-golfed it (at least its a bit more general now).

Eric Wieser (Nov 23 2021 at 04:55):

Is it possible you're after an induction principle like the primed docs#submonoid.closure_induction'?

Riccardo Brasca (Nov 23 2021 at 10:09):

Ah, that's exactly what we need

Riccardo Brasca (Nov 23 2021 at 10:10):

I'll PR a version for adjoin later today

Riccardo Brasca (Nov 23 2021 at 11:16):

Looking at the proof of docs#closure_induction' it seems they used the same trick I proposed here (replace the statement by some ∃...) :sunglasses:

Chris Birkbeck (Nov 23 2021 at 11:28):

Yeah its a good trick, I tried for ages yesterday to do it without it, but in the end just gave up.

Riccardo Brasca (Nov 23 2021 at 12:16):

@Chris Birkbeck I've golfed your adjoin_idem here. If you agree I am going to PR it, it can be in same PR as adjoin_induction'.

Chris Birkbeck (Nov 23 2021 at 12:18):

Oh great, it looks much better now! I'm happy for this to be PR'd

Riccardo Brasca (Nov 23 2021 at 12:24):

#10427

Yakov Pechersky (Nov 23 2021 at 12:34):

BTW the RHS of the iff is not necessary. It's just x.prop

Yakov Pechersky (Nov 23 2021 at 12:35):

So if you have "x : adjoin R s" then you can just directly prove the LHS

Riccardo Brasca (Nov 23 2021 at 13:13):

Thank's, I've golfed the proof.


Last updated: Dec 20 2023 at 11:08 UTC