How to deal with rewriting in types?

Stream: general

[Mario Weitzer]

I try to complete the proof of the following theorem but I'm already stuck at left_inv. The problem is that I can't find a way to use the fact heq. rw, simp_rw, conv, nothing seems to work .

Edit: just to clarify, this is Lean 3.

import data.zmod.basic

def Pi_append_equiv_prod (l1 l2 : list ℕ) :
  (Π (i : ℕ), zmod ((l1 ++ l2).nthd i 1)) ≃+*
  (Π (i : ℕ), zmod (l1.nthd i 1)) × (Π (i : ℕ), zmod (l2.nthd i 1)) :=
{ to_fun :=
  begin
    intro d,
    split,
    { intro i,
      by_cases hi : i < list.length l1,
      { rw ←list.nthd_append _ l2 _ _ hi,
        exact d i,},
      { exact 0,},},
    { intro i,
      rw [←nat.add_sub_cancel_left (list.length l1) i,
        ←list.nthd_append_right _ _ _ _ (nat.le_add_right _ _)],
      exact d (list.length l1 + i),},
  end,
  inv_fun :=
  begin
    rintro ⟨d1, d2⟩,
    intro i,
    by_cases hi : i < list.length l1,
    { rw list.nthd_append _ _ _ _ hi,
      exact d1 i,},
    { rw list.nthd_append_right _ _ _ _ (not_lt.mp hi),
      exact d2 (i - list.length l1),},
  end,
  left_inv :=
  begin
    intro d,
    funext i,
    dsimp only,
    split_ifs with hif,
    { rw [eq_mpr_eq_cast, eq_mpr_eq_cast, cast_cast, cast_eq],},
    { rw [eq_mpr_eq_cast, eq_mpr_eq_cast, eq_mpr_eq_cast, cast_cast, cast_cast],
      have heq : l1.length + (i - l1.length) = i,
      begin
        rw [←nat.add_sub_assoc (not_lt.mp hif), nat.add_sub_cancel_left],
      end,

      sorry,},
  end,
  right_inv :=
  begin
    intro d,
    sorry,
  end,
  map_mul' := sorry,
  map_add' := sorry,}

[Kyle Miller]

For left_inv, you can replace the sorry with apply eq_of_heq, rw [cast, rec_heq_iff_heq, heq]

[Patrick Massot]

Maybe I don't understand the weird statement involving lists, but that doesn't seem provable to me. It read like a Chinese remainder theorem without assumption.

[Mario Weitzer]

For some reason I don't have rec_heq_iff_heq but I used apply rec_heq_of_heq instead and it worked, thank you! I will think about what happened here and try to prove the remaining stuff.

[Kyle Miller]

Your mathlib must be older than february then: https://mathlib-changelog.org/theorem/heq_rec_iff_heq

[Yaël Dillies]

I don't think so, Patrick. I must say the statement is a bit weird, but it's basically saying that (zmod a₁ × ... × zmod aₘ × a_bunch_of_trivial_factors) × (zmod b₁ × ... × zmod bₙ × a_bunch_of_trivial_factors) is the same as zmod a₁ × ... × zmod aₘ × zmod b₁ × ... × zmod bₙ × a_bunch_of_trivial_factors.

[Mario Weitzer]

Patrick Massot
The point is that in the default case I use zmod 1 which is a singleton.

[Patrick Massot]

Ok good. From a distance it really looked like Chinese remainders without coprimeness asumptions, but I didn't take time to decipher it properly. Sorry about the noise!

[Mario Weitzer]

Yaël Dillies
Exactly, that's the idea. I know it's strange but I found no cleaner way to spilt a (de facto finite) Pi-product into a prod of two Pi-products. I guess I could make the Pi only index over the elements of the list l1 ++ l2 but I don't know how to do this properly. Use a finite set as the index set and use list.nth_le instead of list.nthd? This version might look strange but at least it's quite succinct.

[Yaël Dillies]

What's your end goal?

[Kyle Miller]

Is there an equiv version of docs3#fin.append ? That seems like it'd be better than using lists, and it's more general than a zmod-specific version.

[Mario Weitzer]

Yaël Dillies
This is a part of a larger theorem about equivalent rings (in my case it isn't zmods, I just used them here for a short working example). What I really need is exactly what you described, but without the "a_bunch_of_trivial_factors", so

Π (i = 1 ... n) R i ≃+* (Π (i = 1 ... m) R i) × (Π (i = m + 1 ... n) R i)

where the R i are comm_rings.

[Yaël Dillies]

Okay then I would highly suggest you use equivalences of the form (Π x : α ⊕ β, R x) ≃ (Π a : α, R (Sum.inl a)) × (Π b : β, R (Sum.inr b)). This is morally equivalent to what you're trying to do, but it's much more idiomatic for formalisation.

[Mario Weitzer]

I see, I will look into it. Thank you!

[Yaël Dillies]

!loogle (?a -> ?R) × (?b -> R) ≃ (?a ⊕ ?b -> R)

[Yaël Dillies]

@loogle (?a -> ?R) × (?b -> R) ≃ (?a ⊕ ?b -> R)

[loogle]

:exclamation: unknown identifier 'R'

[Yaël Dillies]

@loogle (?a -> ?R) × (?b -> ?R) ≃ (?a ⊕ ?b -> ?R)

[loogle]

:exclamation:

stuck at solving universe constraint
  imax (?u.15836743+1) ?u.15836734 =?= ?u.15836731+1
while trying to unify
  Sort (imax (?u.15836743 + 1) ?u.15836734) : Type (imax (?u.15836743 + 1) ?u.15836734)
with
  Type ?u.15836731 : Type (?u.15836731 + 1)

[Yaël Dillies]

@Joachim Breitner, I broke it :(

[Yaël Dillies]

Probably you're using Type* instead of Type _ somewhere?

[Eric Wieser]

Kyle Miller said:

Is there an equiv version of docs3#fin.append ? That seems like it'd be better than using lists, and it's more general than a zmod-specific version.

I think Reid Barton had one in their Lean 3 tuple PR.

[Mario Carneiro]

@loogle (?a -> (?R : Type _)) × (?b -> ?R) ≃ (?a ⊕ ?b -> ?R)

[loogle]

:search: docs#Equiv.sumArrowEquivProdArrow_symm_apply_inl, docs#Equiv.sumArrowEquivProdArrow_symm_apply_inr