Difficulty with dependent rewrites

Stream: general

[Eric Wieser]

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]

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

[Eric Wieser]

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

[Eric Wieser]

Replace add_comm_monoid with add_comm_group

[Gabriel Ebner]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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]

if you see eq.recin the goal, backtrack immediately

[Eric Wieser]

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

[Eric Wieser]

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

[Kenny Lau]

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]

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

[Eric Wieser]

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]

Which is alarming, because that violates proof invariance?

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

Or is it too specific?

[Eric Wieser]

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]

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]

Opened #4810 with some lemmas to help out.