An error that appears after the last goal is proved

Stream: general

[Riccardo Brasca]

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]

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]

Maybe you've found a bug in a tactic?

[Gabriel Ebner]

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]

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

[Riccardo Brasca]

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]

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]

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]

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]

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]

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]

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]

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

[Yakov Pechersky]

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]

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]

docs#algebra.adjoin_induction

[Chris Birkbeck]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

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]

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]

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]

docs#subtype.eq

[Kevin Buzzard]

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]

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]

@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]

Yeah let me think about how to state it properly.

[Riccardo Brasca]

But I agree that it is a pain

[Yakov Pechersky]

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]

If I understood the desiratum correctly

[Yakov Pechersky]

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]

Right?

[Chris Birkbeck]

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]

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]

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]

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]

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]

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

[Riccardo Brasca]

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

[Chris Birkbeck]

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]

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]

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]

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

[Reid Barton]

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

[Chris Birkbeck]

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

[Chris Birkbeck]

Maybe it does and I'm just being slow

[Reid Barton]

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

[Chris Birkbeck]

Good point! let me see if this works

[Chris Birkbeck]

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]

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

[Riccardo Brasca]

Ah, that's exactly what we need

[Riccardo Brasca]

I'll PR a version for adjoin later today

[Riccardo Brasca]

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]

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

[Riccardo Brasca]

@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]

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

[Riccardo Brasca]

#10427

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Riccardo Brasca]

Thank's, I've golfed the proof.