How can one rewrite a type with an equivalent type?

Stream: Is there code for X?

[Mark Andrew Gerads]

In the following code, I have equal types, Fin (n₀ + 1) = Fin n.
image.png
My purpose is to rewrite the goal with h4, but the same types are not recognized as the same.
Thus I try to simp_rw [h₅] at h₄, to change the types to match, but the rewrite fails. rw also fails.

import Mathlib

opaque RuesDiff : ℕ → ℤ → ℂ → ℂ -- defined elsewhere

lemma RuesDiffMPeriodic (n : ℕ+) (m k : ℤ) : RuesDiff n m = RuesDiff n (m + k * n) := by
  sorry -- proved elsewhere but needed to prove DesiredLemma

lemma DesiredLemma (n : ℕ+) (m : ℤ) (z₀ z₁ : ℂ) : (∑ i : Fin ↑n, ∑ i_1 : Fin ↑n, if ↑↑n ∣ m - ↑↑i - ↑↑i_1 then RuesDiff n (↑↑i) z₀ * RuesDiff n (↑↑i_1) z₁ * ↑↑n else 0) / ↑↑n =
  ∑ k : Fin ↑n, RuesDiff n (↑↑k) z₀ * RuesDiff n (m - ↑↑k) z₁ := by
  rcases Nat.exists_eq_succ_of_ne_zero (PNat.ne_zero n) with ⟨n₀, h₃⟩
  have h₄ : ∀ (i i_1 : Fin (n₀ + 1)), ↑(n₀ + 1) ∣ m - ↑↑i - ↑↑i_1 ↔ i_1 = (m : Fin (n₀ + 1)) - i := by
    change ∀ (i i_1 : ZMod (n₀ + 1)), ↑(n₀ + 1) ∣ m - (i.val : ℤ) - (i_1.val : ℤ) ↔ i_1 = (m : ZMod (n₀ + 1)) - i
    intros i i_1
    rw [←ZMod.intCast_zmod_eq_zero_iff_dvd]
    simp only [ZMod.natCast_val, Int.cast_sub, ZMod.intCast_cast, ZMod.cast_id', id_eq]
    constructor
    · intros h₅
      have h₆ := congrArg (λ x => x + i_1) h₅
      simp only [sub_add_cancel, zero_add] at h₆
      exact h₆.symm
    · intros h₅
      rw [h₅]
      simp only [sub_self]
  simp only [Nat.succ_eq_add_one] at h₃
  simp_rw [← h₃] at h₄
  have h₅ : Fin (n₀ + 1) = Fin n := by exact congrArg Fin (id (Eq.symm h₃))
  simp_rw [h₅] at h₄ -- trying to rewrite the type Fin (n₀ + 1) with Fin ↑n, failing
  sorry

[Yaël Dillies]

Sorry, I started writing some code for your previous question but I ran out of time. Expect something either this morning or this evening

[Mark Andrew Gerads]

Thank you.

[Mark Andrew Gerads]

I believe change ∀ (i i_1 : Fin ↑n), ↑↑n ∣ m - ↑↑i - ↑↑i_1 ↔ i_1 = ↑m - i at h₄ should have worked, but it doesn't. Perhaps the 2 types are equal but not definitionally equal?

[Yaël Dillies]

Here is a sketch proof:

import Mathlib

open Finset

opaque f : ℕ → ℤ → ℂ → ℂ -- defined elsewhere

lemma f_periodic (n : ℕ) (m k : ℤ) : f n m = f n (m + k * n) := by
  sorry -- proved elsewhere but needed to prove DesiredLemma

lemma desired (n : ℕ) (m : ℤ) (z₀ z₁ : ℂ) :
    (∑ i : Fin n, ∑ j : Fin n, if ↑n ∣ m - i - j then f n i z₀ * f n j z₁ * n else 0) / n =
      ∑ k : Fin n, f n k z₀ * f n (m - k) z₁ := by
  obtain rfl | hn := eq_or_ne n 0
  · simp
  have : NeZero n := ⟨hn⟩
  calc
    _ = ∑ i : Fin n, ∑ j : Fin n, if ↑n ∣ m - i - j then f n i z₀ * f n j z₁ else 0 := by
      simp_rw [sum_div]; congr! 2 with i j; split_ifs <;> simp [hn]
    _ = ∑ i : Fin n, ∑ j : Fin n, if j = ↑m - i then f n i z₀ * f n j z₁ else 0 := by
      congr! 3 with i j
      sorry -- Easy
    _ = _ := by
      simp
      norm_cast
      congr! 2 with i
      sorry -- Use `f_periodic`

[Yaël Dillies]

It's not very clear to me that ∑ i : Fin n (as opposed to say ∑ i ∈ Ico (0 : ℤ) n) is the right choice.

[Mark Andrew Gerads]

I only used Fin n because that is what the Lean 3 code did (which I did not write). Perhaps avoiding Fin n would be easier, in which case, this lemma would work to finish the proof:

import Mathlib

open Complex Classical NormedSpace BigOperators Finset Real

opaque RuesDiff : ℕ → ℤ → ℂ → ℂ -- defined elsewhere

lemma RuesDiffMPeriodic (n : ℕ+) (m k : ℤ) : RuesDiff n m = RuesDiff n (m + k * n) := by
  sorry -- proved elsewhere but needed to prove DesiredLemma

lemma DesiredV2 (n : ℕ+) (m : ℤ) (z₀ z₁ : ℂ) : (∑ x ∈ range ↑n, ∑ x_1 ∈ range ↑n, if ↑↑n ∣ m - ↑x - ↑x_1 then RuesDiff n (↑x) z₀ * RuesDiff n (↑x_1) z₁ * ↑↑n else 0) / ↑↑n =
  ∑ k ∈ range ↑n, RuesDiff n (↑k) z₀ * RuesDiff n (m - ↑k) z₁ := by
  sorry

Your sketch proof looks nice, but I was unable to prove either sorry in it.
Do you perhaps know how to rewrite a type that is equal to another type, but not definitionally equal?

[Yaël Dillies]

I do, but if you have to do that you most likely went wrong earlier

[Mark Andrew Gerads]

I generalized this so that it is more worthy of being in Mathlib. I wrote 2 versions, one with Fin n and one with range n. I am biased towards the lemma using range n. What do you think?

import Mathlib

open Finset

lemma DesiredV1 {α β : Type} [Ring β] {n : ℕ} (m : ℤ) (z₀ z₁ : α) {f : ℤ → α → β} (f_periodic : ∀ (m₂ k : ℤ) , f m₂ = f (m₂ + k * n)) :
    (∑ i : Fin n, ∑ j : Fin n, if ↑n ∣ m - i - j then f i z₀ * f j z₁ else 0) = ∑ k : Fin n, f k z₀ * f (m - k) z₁ := by
  obtain rfl | hn := eq_or_ne n 0
  · simp only [univ_eq_empty, CharP.cast_eq_zero, zero_dvd_iff, sum_empty, sum_const_zero]
  have hnNot0 : NeZero n := ⟨hn⟩
  calc
    _ = ∑ i : Fin n, ∑ j : Fin n, if j = ↑m - i then f i z₀ * f j z₁ else 0 := by
      congr! 3 with i j x a
      constructor
      · intros h₃
        obtain ⟨w, hw⟩ := h₃
        have hw₂ := congrArg (λ (k : ℤ) => (k : Fin n) + x) hw
        simp only [Int.cast_sub, Int.cast_natCast, Fin.cast_val_eq_self, sub_add_cancel,
          Int.cast_mul, Fin.natCast_self, zero_mul, zero_add] at hw₂
        exact hw₂.symm
      · intros h₃
        rw [h₃]
        refine Int.dvd_sub_of_emod_eq ?_
        sorry
    _ = _ := by
      simp only [sum_ite_eq', mem_univ, ↓reduceIte]
      congr! 2 with i a
      sorry -- use f_periodic

lemma DesiredV2 {α β : Type} [Ring β] {n : ℕ} (m : ℤ) (z₀ z₁ : α) {f : ℤ → α → β} (f_periodic : ∀ (m₂ k : ℤ) , f m₂ = f (m₂ + k * n)) :
    (∑ i ∈ range n, ∑ j ∈ range n, if ↑n ∣ m - i - j then f i z₀ * f j z₁ else 0) = ∑ k ∈ range n, f k z₀ * f (m - k) z₁ := by
  simp only [sum_range]
  exact DesiredV1 m z₀ z₁ f_periodic

[Mark Andrew Gerads]

Stuck on this part that needs this example lemma:

import Mathlib

example (n : ℕ) (m : ℤ) (hnNot0 : NeZero n) (i : Fin n) : (m - ((i : ℕ) : ℤ)) % (n : ℤ) = (((m : Fin n) - i : ℕ) : ℤ) := by
  sorry

I think Mathlib is missing the relevant lemmas to solve this easily.

[Kevin Buzzard]

The counterargument is that you're trying to do arithmetic with three different types here and one wonders whether you could do with a redesign where you don't have to prove equalities that have 6 up-arrows in. You have Fin n and % n -- can I interest you in ZMod n or will this make things worse in other places?

[Kevin Buzzard]

PS I can't get the statement to compile as it stands -- can you add imports and some explicit coercions to make a #mwe ?

[Mark Andrew Gerads]

Hmm. ZMod might be easier. Is there something like sum_range that changes the sum from range n to be over ZMod n instead of Fin n?

[Kevin Buzzard]

If I've understood the question correctly you could try the following: I think you're trying to prove that an integer reduced mod n is the same thing as something lifted from Fin n to the integers possibly via the naturals. If this construction is a thing for you then you'll need a simpler lemma saying that given an integer, reducing it mod n with % is the same thing as casting it to ZMod n and then lifting back to the integers. Then you'll need facts about how reducing mod n is an additive group hom which will be there for the map to ZMod n but who knows if it's there for the map to Fin n.

One problem you seem to be facing is that you want to with work a type with n elements but then also constantly be moving between this type and a type like the integers. One of these maps is necessarily mathematically pathological and it will be a case of finding the right API for it.

[Mark Andrew Gerads]

I was following some Lean 3 code that used ZMod n in the first post of this thread, but ran into a problem of Type mismatch... The types were equal, but not definitionally equal, so the change command did not work, and I still don't know how to fix that sort of problem.

[Kevin Buzzard]

Right. Can you for example do everything with the integers? And something which you want to be in "Fin n" you can just add inequalities saying "I'm >= 0 and < n"? And something you want to be a natural can just be >= 0?

[Kevin Buzzard]

Then there are no types to mess things up

[Kevin Buzzard]

Equality of types is a poorly-behaved concept. It's the Achilles heel of dependent type theory. Your original question is "how do I tame it?" and one possible answer is "by redesigning, you might be able to avoid it"

[Kevin Buzzard]

All of our theory of complexes in homological algebra took many iterations to design because of issues caused by equality of types (which simply don't exist in the papers)

[Mark Andrew Gerads]

I will continue trying to get this proved. It is a shame that some things that are so obviously true are so difficult to prove to a computer.

[Mark Andrew Gerads]

I will consider how to prove this without Fin n and ZMod n, and see if the integers are enough.

[Kevin Buzzard]

There is an art to all of this. I learnt very early on that "just write down the things in any way which is mathematically correct" is not the best way to formalise stuff. As a professional mathematician I initially regarded it as a bit of an insult that I couldn't just express my ideas in any way I wanted and then expect calculations to be easy, but now I know a lot more about the area and I've realised that under the hood everything is far more of a chore than you might expect and that you have to treat the system with far more respect than my initial instincts.

[Kevin Buzzard]

The art is to formalise the theory in such a way that the calculations flow naturally and everything looks easy, and your example with 6 up-arrows in just smells to me like a design decision which made made things too hard. By the way I totally agree with your earlier claim that it might be the case that your goal is hard to do in Lean (right now it's hard for me to do because I can't even compile the question, so the ball is in your court here to make the #mwe). And one could argue that my proposed solution ("you shouldn't be asking that question anyway, this indicates that some earlier choices were poor") is not really an acceptable answer (it might be true in 2024 though).

[Mark Andrew Gerads]

This is my MWE, I made sure that It plugs in with the rest of my code.

import Mathlib

open Finset

lemma DesiredV2 {α β : Type} [Ring β] {n : ℕ} (m : ℤ) (z₀ z₁ : α) {f : ℤ → α → β} (f_periodic : ∀ (m₂ k : ℤ) , f m₂ = f (m₂ + k * n)) :
    (∑ i ∈ range n, ∑ j ∈ range n, if ↑n ∣ m - i - j then f i z₀ * f j z₁ else 0) = ∑ k ∈ range n, f k z₀ * f (m - k) z₁ := by
  sorry

[Mark Andrew Gerads]

This looks like a good start:

import Mathlib
set_option maxHeartbeats 0

open Finset

lemma DesiredV2 {α β : Type} [Ring β] {n : ℕ} (m : ℤ) (z₀ z₁ : α) {f : ℤ → α → β} (f_periodic : ∀ (m₂ k : ℤ) , f m₂ = f (m₂ + k * n)) :
    (∑ i ∈ range n, ∑ j ∈ range n, if ↑n ∣ m - i - j then f i z₀ * f j z₁ else 0) = ∑ k ∈ range n, f k z₀ * f (m - k) z₁ := by
  refine sum_congr rfl ?_
  intros x hx
  sorry

[Mark Andrew Gerads]

Nvm, that only works for n>0.

[Mark Andrew Gerads]

This looks like a correct start though:

import Mathlib
set_option maxHeartbeats 0

open Finset

lemma DesiredV2 {α β : Type} [Ring β] {n : ℕ} (m : ℤ) (z₀ z₁ : α) {f : ℤ → α → β} (f_periodic : ∀ (m₂ k : ℤ) , f m₂ = f (m₂ + k * n)) :
    (∑ i ∈ range n, ∑ j ∈ range n, if ↑n ∣ m - i - j then f i z₀ * f j z₁ else 0) = ∑ k ∈ range n, f k z₀ * f (m - k) z₁ := by
  obtain rfl | hn := eq_or_ne n 0
  · simp only [range_zero, CharP.cast_eq_zero, zero_dvd_iff, sum_empty, sum_const_zero]
  refine sum_congr rfl ?_
  intros k hk
  sorry

[Yaël Dillies]

I'm back to this, expect progress in a few tens of minutes

[Kevin Buzzard]

I can certainly believe that Yael can prove that theorem.

My instinct though is that either you state it like that and then also fill in a bunch of missing API, or you state it in a more friendly way and make it easier to prove. For example your definition of f_periodic looks like a nightmare to use. It's mathematically correct, sure! But if I ever want to use it I need to come up with k. Are you sure you can't get away with f : ZMod n -> alpha -> beta? Then you don't need the hypothesis at all. If i,j are in ZMod n rather than range n then \u n | m - i - j becomes i + j = mwhich is much easier to manipulate. And so on and so on.

[Kevin Buzzard]

You have an integer m but you only ever care about m mod n so maybe m : ZMod n is better. In other words you can strip out the integers completely from your lemma whilst still maintaining all of its mathematical meaning and now only having to do arithmetic in ZMod n and, crucially, you will have literally 0 up-arrows.

[Mark Andrew Gerads]

In my code, I also have

lemma RuesDiffMod (n : ℕ+) (m : ℤ) : RuesDiff n m = RuesDiff n (m % n) := by

Thus, we can change f_periodic like so:

import Mathlib
set_option maxHeartbeats 0

open Finset

lemma DesiredV3 {α β : Type} [Ring β] {n : ℕ} (m : ℤ) (z₀ z₁ : α) {f : ℤ → α → β} (f_periodic : ∀ (m₂ : ℤ) , f m₂ = f (m₂ % n)) :
    (∑ i ∈ range n, ∑ j ∈ range n, if ↑n ∣ m - i - j then f i z₀ * f j z₁ else 0) = ∑ k ∈ range n, f k z₀ * f (m - k) z₁ := by
  obtain rfl | hn := eq_or_ne n 0
  · simp only [range_zero, CharP.cast_eq_zero, zero_dvd_iff, sum_empty, sum_const_zero]
  refine sum_congr rfl ?_
  intros k hk
  calc
    _ = ∑ j ∈ range n, if j = (m - ↑k) % n then f (↑k) z₀ * f (↑j) z₁ else 0 := by
      congr! 2 with j hj
      sorry
    _ = f (↑k) z₀ * f ((m - ↑k) % n) z₁ := by
      sorry
    _ = _ := by
      exact Eq.symm (Mathlib.Tactic.LinearCombination.mul_pf rfl (congrFun (f_periodic (m - ↑k)) z₁))

I do see how this version is easier to work with.

[Yaël Dillies]

I mean, the better answer is to use the bespoke docs#Function.Periodic

[Mark Andrew Gerads]

I like @Kevin Buzzard 's idea of using {f : ZMod n → α → β}. To do so, I will need to refactor a function used basically everywhere in a 23.3 KiB file, but maybe that's for the best, if it doesn't break anything I can't fix. I will start refactoring a copy of the file.

[Mark Andrew Gerads]

The refactor is not going well. Stuff broke.

[Mark Andrew Gerads]

Instead of refactoring the whole file, I added a function {f : ZMod n → α → β} and showed it was equal to the original function. Now we can work directly in ZMod n as suggested by @Kevin Buzzard . Perhaps it will be easier this way.

import Mathlib

open Finset

lemma DesiredV4 {α β : Type} [Ring β] {n : ℕ} (m : ℤ) (z₀ z₁ : α) (f : ZMod n → α → β) :
    (∑ i ∈ range n, ∑ j ∈ range n, if ↑n ∣ m - i - j then f i z₀ * f j z₁ else 0) = ∑ k ∈ range n, f k z₀ * f (m - k) z₁ := by
  obtain rfl | hn := eq_or_ne n 0
  · simp only [range_zero, CharP.cast_eq_zero, zero_dvd_iff, sum_empty, sum_const_zero]
  refine sum_congr rfl ?_
  intros k hk
  sorry

[Kim Morrison]

Learn to love refactoring. :-)

[Mark Andrew Gerads]

I made progress, but am still unfamiliar with ZMod.

import Mathlib

open Finset

theorem extracted_1 (mk : ℤ) (n₀ : ℕ) : ↑(n₀ + 1) ∣ mk - ↑(↑mk : ZMod (n₀ + 1)).val := sorry

lemma DesiredV4 {α β : Type} [Ring β] {n : ℕ} (m : ℤ) (z₀ z₁ : α) (f : ZMod n → α → β) :
    (∑ i ∈ range n, ∑ j ∈ range n, if ↑n ∣ m - i - j then f i z₀ * f j z₁ else 0) = ∑ k ∈ range n, f k z₀ * f (m - k) z₁ := by
  obtain rfl | hn := eq_or_ne n 0
  · simp only [range_zero, CharP.cast_eq_zero, zero_dvd_iff, sum_empty, sum_const_zero]
  refine sum_congr rfl ?_
  intros k hk
  rcases Nat.exists_eq_succ_of_ne_zero hn with ⟨n₀, rfl⟩
  simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, sum_range]
  change (∑ i : ZMod (n₀ + 1), if ↑n₀ + 1 ∣ m - ↑k - ↑i.val then f (↑k) z₀ * f (i.val) z₁ else 0) = f (↑k) z₀ * f (↑m - ↑k) z₁
  have h₀ : ∀ (i : ZMod (n₀ + 1)), (n₀ : ℤ) + 1 ∣ m - ↑k - ↑i.val ↔ i = (m : ZMod (n₀ + 1)) - (k : ZMod (n₀ + 1)) := by
    intros i
    constructor
    · intros ha
      obtain ⟨w, hw⟩ := ha
      norm_cast
      have hw₂ := congrArg (λ (j : ℤ) => j + ↑i.val) hw
      simp only [ZMod.natCast_val, sub_add_cancel] at hw₂
      rw [hw₂]
      simp only [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_one, ZMod.natCast_self',
        zero_mul, ZMod.intCast_cast, ZMod.cast_id', id_eq, zero_add]
    · intros ha
      rw [ha]
      norm_cast
      exact extracted_1 (m - ↑k) n₀
  simp_rw [h₀]
  simp only [Nat.succ_eq_add_one, ZMod.natCast_val, ZMod.cast_id', id_eq, sum_ite_eq', mem_univ,
    ↓reduceIte]

[Mark Andrew Gerads]

Now all that remains is this very stubborn extracted goal:

import Mathlib

theorem extracted_1 (mk : ℤ) (n₀ : ℕ) : ↑(n₀ + 1) ∣ mk - ↑(↑mk : ZMod (n₀ + 1)).val := sorry

[Michael Stoll]

import Mathlib.Data.ZMod.Basic

theorem extracted_1 (mk : ℤ) (n₀ : ℕ) : ↑(n₀ + 1) ∣ mk - ↑(↑mk : ZMod (n₀ + 1)).val := by
  -- `apply?` ==>
  refine (ZMod.intCast_eq_intCast_iff_dvd_sub (↑(↑mk : ZMod (n₀ + 1)).val) mk (n₀ + 1)).mp ?_
  -- `simp?` ==>
  simp only [ZMod.natCast_val, ZMod.intCast_cast, ZMod.cast_intCast']

[Mark Andrew Gerads]

The final step is complete! Thank you all.
Now the question is should this be in Mathlib, and if so, what should it be called, and what file should it be in?

[Andrew Yang]

import Mathlib

open Finset

lemma ZMod.sum_univ_eq_sum_range {n : ℕ} [NeZero n] {α} [AddCommMonoid α] (f : ZMod n → α) :
    ∑ i : ZMod n, f i = ∑ i in range n, f i := by
  rw [← Fin.sum_univ_eq_sum_range]
  cases n
  · exact (neZero_zero_iff_false.mp ‹_›).elim
  · simp [ZMod]

lemma DesiredV4 {α β : Type} [Ring β] {n : ℕ} (m : ℤ) (z₀ z₁ : α) (f : ZMod n → α → β) :
    (∑ i ∈ range n, ∑ j ∈ range n, if ↑n ∣ m - i - j then f i z₀ * f j z₁ else 0) = ∑ k ∈ range n, f k z₀ * f (m - k) z₁ := by
  obtain rfl | hn := eq_zero_or_neZero n
  · simp only [range_zero, CharP.cast_eq_zero, zero_dvd_iff, sum_empty, sum_const_zero]
  simp_rw [← ZMod.intCast_eq_intCast_iff_dvd_sub, Int.cast_sub,
    Int.cast_natCast, ← fun x : ℕ ↦ ZMod.sum_univ_eq_sum_range
      (fun j : ZMod n ↦ if j = ↑m - x then f x z₀ * f j z₁ else 0)]
  simp only [← Finset.sum_filter, Finset.filter_eq', mem_univ, ↓reduceIte, sum_singleton]

I think we are missing the first lemma. DesiredV4 should follow relatively easily.

[Mark Andrew Gerads]

@Andrew Yang Great! Would you please add your lemma ZMod.sum_univ_eq_sum_range to Mathlib?

[Andrew Yang]

Unfortunately I don't have much time to PR now. It would be great if you can PR it for me (and make sure that we are really missing it and it's not me bad at searching). Or you would have to wait a day or two.

[Mark Andrew Gerads]

I suppose I am in no hurry. I don't even know which file it should go in.

[Michael Stoll]

@loogle Finset.sum, Finset.range, ZMod

[loogle]

:shrug: nothing found

[Michael Stoll]

So it's unlikely it already exists.
Finding an existing file for it is maybe not so easy, #minimize_imports says it needs both Mathlib.Data.Fintype.BigOperators and Mathlib.Data.ZMod.Defs, which are unlikely to be imported simultaneously in a suitably early file.

[Edward van de Meent]

remember to try #find_home for all your code-home-finding needs!