## Stream: general

### Topic: Difficulty with dependent rewrites

#### Eric Wieser (Oct 27 2020 at 11:27):

I'm struggling to prove this trivial-but-dependently-typed statement:

import algebra.direct_sum
import algebra.algebra.basic
import algebra.algebra.subalgebra
import algebra.group.pi

open_locale direct_sum

variables
(R : Type*) (A : Type*) (ι : Type*)
[comm_ring R]
[ring A]
[algebra R A]
[decidable_eq ι]
[Π (x : A), decidable (x ≠ 0)]
(submodules : ι → submodule R A)

-- probably should be in mathlib somewhere?
instance submodule.decidable_zero (S : submodule R A) (x : S) : decidable (x ≠ 0) :=
decidable.rec_on (infer_instance : decidable ((x : A) ≠ 0))
(λ hfalse, decidable.is_false $by simp * at *) (λ htrue, decidable.is_true$ by simp * at *)

example
(a : ⨁ (i : ι), ↥(submodules i)) :

a.sum (λ i ai, direct_sum.of (λ i, submodules i) (i + 0) ⟨↑ai, by simp [submodule.coe_mem, add_zero]⟩) = a :=
begin
sorry
end


I can't work out how to rewrite i + 0 = 0 and the ⟨↑ai, _⟩ = ai at the same time.

#### Gabriel Ebner (Oct 27 2020 at 11:31):

The snippet doesn't compile for me with current mathlib.

#### Eric Wieser (Oct 27 2020 at 11:31):

Oh damn, this is based off local changes and the ever-delayed #3490

#### Eric Wieser (Oct 27 2020 at 11:32):

Replace add_comm_monoid with add_comm_group

#### Gabriel Ebner (Oct 27 2020 at 11:35):

I still get failed to synthesize type class instance for Π (i : ι), add_comm_group ((λ (i : ι), ↥(submodules i)) i) even on your branch.

#### Eric Wieser (Oct 27 2020 at 11:35):

Hmm, even then it doesn't work. Will iterate a bit in the web editor and report back when it compiles

#### Eric Wieser (Oct 27 2020 at 11:40):

Ok, fixed. Needed semirings promoted to rings, and a decideable instance in my local file

#### Eric Wieser (Oct 27 2020 at 12:17):

I can make some progress with

begin
suffices : a.sum (λ i ai, direct_sum.of (λ i, submodules i) i ai) = a,
{ convert this,
ext,
rw direct_sum.of,
rw direct_sum.of,
simp,
congr,
ext,
simp,
congr,
{ sorry },  -- ⟨↑x_1, _⟩ == x_1
{ simp, },
{ sorry },  -- _ == ?m_1
},
simp [direct_sum.of, dfinsupp.sum_single],
sorry -- dfinsupp.sum_single didn't match?
end


but i'm stuck on all three sorries

#### Eric Wieser (Oct 28 2020 at 11:07):

Down to one sorry with

-- paste the above preamble here
begin
convert dfinsupp.sum_single,
rotate, -- get the instance arguments out of the way
apply_instance,
apply_instance,
{
ext i si i',
simp [direct_sum.of],  -- I can't make this simp only
congr,
ext h,
subst h,
cases si,
simp only [submodule.coe_mk],
have : si_val = (⟨si_val, by {rw add_zero, exact si_property}⟩ : submodules (i + 0)) := by simp,
conv_rhs {rw this},
convert submodule.coe_eq_coe.mpr _,
recover, -- !!!
rotate,
exact si_property,
dsimp, -- this succeeds but has no visible change to the goal state!
sorry, -- eq.rec ⟨si_val, _⟩ _ = ⟨si_val, si_property⟩
},
end


Anyone have any ideas? Neither finish, tidy, or refl work.

#### Kenny Lau (Oct 28 2020 at 11:08):

if you see eq.recin the goal, backtrack immediately

#### Eric Wieser (Oct 28 2020 at 11:09):

simp [direct_sum.of] is the line that introduced the eq.rec

#### Eric Wieser (Oct 28 2020 at 11:12):

Is eq.rec in the goal better or worse than == (heq)?

#### Kenny Lau (Oct 28 2020 at 11:36):

import algebra.direct_sum
import algebra.algebra.basic
import algebra.algebra.subalgebra
import algebra.group.pi

open_locale classical direct_sum

variables
(R : Type*) (A : Type*) (ι : Type*)
[comm_ring R] [ring A] [algebra R A]
[add_comm_group ι] (S : ι → submodule R A)

-- -- probably should be in mathlib somewhere?
-- instance submodule.decidable_zero (S : submodule R A) (x : S) : decidable (x ≠ 0) :=
-- decidable.rec_on (infer_instance : decidable ((x : A) ≠ 0))
--   (λ hfalse, decidable.is_false $by simp * at *) -- (λ htrue, decidable.is_true$ by simp * at *)

theorem as_sum (x : ⨁ (i : ι), S i) :
x.sum (λ i xi, direct_sum.of (λ i, S i) (i + 0) ⟨xi, (add_zero i).symm ▸ xi.2⟩) = x :=
begin
convert @dfinsupp.sum_single ι (λ i, S i) _ _ _ x,
ext1 i, ext1 xi,
have aux : ∀ k = i, direct_sum.of (λ i, S i) k ⟨xi, H.symm ▸ xi.2⟩ =
direct_sum.of (λ i, S i) i xi,
{ intros k H, subst H, cases xi, refl },
exact aux (i + 0) _
end


#### Kenny Lau (Oct 28 2020 at 11:36):

so the solution to eq.rec is generalize until you're left with variables not expressions

#### Eric Wieser (Oct 28 2020 at 11:49):

It looks like the key difference between your proof and mine is your use of (add_zero i).symm ▸ xi.2 and not by simp [submodule.coe_mem, add_zero]

#### Eric Wieser (Oct 28 2020 at 11:49):

Which is alarming, because that violates proof invariance?

#### Eric Wieser (Oct 28 2020 at 11:50):

Ah, I guess the elaborator is unfolding your proof but not mine

#### Eric Wieser (Oct 28 2020 at 12:09):

Would it make sense for your aux to be in mathlib?

#### Eric Wieser (Oct 28 2020 at 12:09):

Or is it too specific?

#### Eric Wieser (Oct 28 2020 at 12:31):

Perhaps

lemma dfinsupp.single_eq {β : ι → Type} [∀ i, has_zero(β i)] (i k) (xi : β i) (xk : β k) (h : k = i) (hx : xi == xk):
dfinsupp.single k xk = dfinsupp.single i xi :=
begin
subst h,
congr,
exact eq_of_heq (heq.symm hx),
end


#### Eric Wieser (Oct 28 2020 at 13:50):

Combined with

lemma submodule.heq {S T : submodule R A} (s : S) (t : T) (h' : S = T) : s == t ↔ ((s : A) = t):=
begin
subst h',
exact iff.symm (iff.trans submodule.coe_eq_coe ⟨heq_of_eq, eq_of_heq⟩),
end


#### Eric Wieser (Oct 28 2020 at 14:48):

Opened #4810 with some lemmas to help out.

Last updated: May 16 2021 at 05:21 UTC