# Zulip Chat Archive

## 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]
[add_comm_group ι]
[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,
{ rw add_zero, },
{ sorry }, -- ⟨↑x_1, _⟩ == x_1
{ rw add_zero, },
{ 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 _,
repeat {rw add_zero},
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.rec`

in 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