products over `(fin n)`

Stream: Is there code for X?

[Michael Stoll]

The lemma below looks like it would be a reasonable thing to have. It is more or less equivalent to fin.prod_univ_cast_succ, but not exactly, so the proof below essentially is about showing that it's the same after all.
I strongly suspect that this can be done in a better (shorter/more efficient) way to do this. Any suggestions?
(The motivation is the idea of using each of the new lemmas fin.prod_univ_<number> introduced in #15684 to prove the next one.)

import algebra.big_operators.fin

open_locale big_operators

lemma fin.prod_univ_succ (n : ℕ) {M : Type*} [comm_monoid M] (f : (fin (n + 1)) → M) :
  ∏ (a : fin (n + 1)), f a = (∏ (a : fin n), f a) * f n :=
begin
  rw [fin.prod_univ_cast_succ],
  congr,
  ext,
  { rw [fin.coe_eq_cast_succ], },
  { symmetry,
    apply fin.eq_last_of_not_lt,
    rw [fin.coe_of_nat_eq_mod, nat.mod_eq_of_lt (lt_add_one n)],
    exact irrefl n, }
end

[Kyle Miller]

That reminds me, I had these is some unfinished project a while back and they seem like they could also be useful:

lemma prod_option {α : Type*} [fintype α] {β : Type*} [comm_monoid β] (f : option α → β) :
  ∏ (x : option α), f x = f none * ∏ (x : α), f (some x) :=
begin
  classical,
  have : {none} ⊆ (finset.univ : finset (option α)) := finset.subset_univ {none},
  rw [← finset.prod_sdiff this, mul_comm],
  congr' 1,
  { simp, },
  { have : finset.univ \ {none} = finset.univ.image (some : α → option α),
    { ext x,
      simp [option.eq_none_iff_forall_not_mem, eq_comm], },
    rw this,
    simp, },
end

lemma prod_fin_succ {α : Type*} [comm_monoid α] {n : ℕ} (f : fin n.succ → α) :
  ∏ (x : fin n.succ), f x = f 0 * (∏ (x : fin n), f (fin.succ_embedding _ x)) :=
begin
  let e := fin_succ_equiv n,
  rw fintype.prod_equiv e f (f ∘ e.symm),
  swap, { intro x, simp only [function.comp_app, equiv.symm_apply_apply], },
  rw [prod_option],
  refl,
end

(Disclaimer: I haven't checked if they still compile or if there are missing definitions.)

[Eric Wieser]

Am I mising something about your fin.prod_univ_succ? Isn't the only difference n vs fin.last n?

[Yaël Dillies]

Agreed with Eric. What you want is already called docs#fin.prod_univ_succ !

[Kevin Buzzard]

I don't think so -- Michael wants to pull off the last term, and what Yael is linking to pulls off the first term.

[Yaël Dillies]

Then docs#fin.prod_univ_cast_succ, or even docs#fin.prod_univ_succ_above for the general case.

[Yaël Dillies]

My point is that we have all versions already.

[Junyan Xu]

Yes with these it's pretty easy

import algebra.big_operators.fin
open_locale big_operators
lemma prod_univ_succ (n : ℕ) {M : Type*} [comm_monoid M] (f : fin (n + 1) → M) :
  ∏ (a : fin (n + 1)), f a = (∏ (a : fin n), f a) * f n :=
by simp_rw [fin.prod_univ_cast_succ, fin.coe_eq_cast_succ, fin.coe_nat_eq_last]

[Michael Stoll]

If there are no objections, I'll add prod_univ_succ in #15684 and change the proofs of the fin.prod_univ_<n> lemmas to fit the pattern by {rw [prod_univ_succ <n-1>, prod_univ_seven], refl} (which seems to be slighly faster than what @Junyan Xu suggested in a comment there).

[Junyan Xu]

You mean by {rw [prod_univ_succ, prod_univ_<n-1>], refl}? Sounds good.

[Yaël Dillies]

But... fin.prod_univ_succ_cast already is the lemma you want, modulo two rewrites because you didn't quite use the same form.

[Michael Stoll]

One of the rewrites is under the product, which makes it less friendly.
I also find my version more natural.

[Michael Stoll]

BTW, fin.prod_univ_succ already exists (it peels of f f 0), so I'll rename to fin.prod_univ_succ'.

[Yaël Dillies]

Yes, this is what I've been saying all along. If you really want to add your version, you should name it fin.prod_univ_coe or fin.prod_univ_coe_succ.

[Junyan Xu]

Actually by { rw [prod_univ_cast_succ, prod_univ_three], refl } etc. also works. They're defeq when you give explicit numbers! So no need of the new lemma after all.

[Michael Stoll]

OK, so I'll use that. Thanks!

[Eric Wieser]

Is one of these simp normal?

[Eric Wieser]

I feel like the current version with cast_succ is much better than the double coercion being suggested

[Eric Wieser]

Does the double coercion simplify to the former already?

[Junyan Xu]

docs#fin.prod_univ_cast_succ is simpler than the proposed lemma according to the simp lemma docs#fin.coe_eq_cast_succ.

[Eric Wieser]

Note that #15738 contains a single lemma ((fin_vec.sum_eq f).symm) that proves all these statements for any given n

[Yaël Dillies]

Eric, is this what all the reflection fuss is about in Coq?

[Eric Wieser]

That's what I was referring to, but I'm not certain I'm using the term correctly

[Michael Stoll]

Eric Wieser said:

Note that #15738 contains a single lemma ((fin_vec.sum_eq f).symm) that proves all these statements for any given n

I see the line

example [has_add α] [has_zero α] (a : fin 3 → α) : sum a = a 0 + a 1 + a 2 := rfl

there, which seems to indicate that with the definition of sum there, one gets a definitional equality.

[Michael Stoll]

In any case, I've now included the more efficient proofs in #15684.
I hope this PR can be merged now...

[Michael Stoll]

Since I need the n = 8 case in number_theory.legendre_symbol.gauss_sum and would like to get on with the Legendre Symbol refactor, I think it makes sense to have these lemmas for the time being. After #15738 is merged, they can probably be removed again (but perhaps there should some info in the docstrings of fin.prod_univ_two and fin.sum_univ_two explaining how to get these statements for larger n) and the proof that uses fin.sum_univ_eight can be modified.