Zulip Chat Archive

Stream: general

Topic: Difficulty with dependent rewrites


view this post on Zulip 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.

view this post on Zulip Gabriel Ebner (Oct 27 2020 at 11:31):

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

view this post on Zulip Eric Wieser (Oct 27 2020 at 11:31):

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

view this post on Zulip Eric Wieser (Oct 27 2020 at 11:32):

Replace add_comm_monoid with add_comm_group

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Oct 27 2020 at 11:40):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Oct 28 2020 at 11:08):

if you see eq.recin the goal, backtrack immediately

view this post on Zulip Eric Wieser (Oct 28 2020 at 11:09):

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

view this post on Zulip Eric Wieser (Oct 28 2020 at 11:12):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Oct 28 2020 at 11:36):

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

view this post on Zulip 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]

view this post on Zulip Eric Wieser (Oct 28 2020 at 11:49):

Which is alarming, because that violates proof invariance?

view this post on Zulip Eric Wieser (Oct 28 2020 at 11:50):

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

view this post on Zulip Eric Wieser (Oct 28 2020 at 12:09):

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

view this post on Zulip Eric Wieser (Oct 28 2020 at 12:09):

Or is it too specific?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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