Properties of products

Stream: Is there code for X?

[Michael Stoll]

Is a version of the following in mathlib?

import data.list.big_operators
namespace list

lemma prod_prop {α : Type*} [monoid α] {l : list α} {P : α → Prop}
  (h₁ : P 1) (h₂ : ∀ a ∈ l, P a) (h₃ : ∀ a b : α, P a → P b → P (a * b)) : P l.prod :=
begin
  induction l with hd tl ih,
  { simp only [prod_nil, h₁], },
  { simp only [prod_cons],
    exact h₃ _ _ (h₂ _ (mem_cons_self _ _)) (ih (λ a ha, h₂ a $ mem_cons_of_mem _ ha)), }
end

There is docs#list.prod_hom_rel, which looks somewhat related, but is different...

[Junyan Xu]

I think it's easy enough to construct a submonoid from the hypotheses and apply docs#submonoid.list_prod_mem .

[Michael Stoll]

Thanks. I'll look at this tomorrow.

[Yakov Pechersky]

import data.list.basic

namespace list

lemma prod_prop {α : Type*} [monoid α] {l : list α} {P : α → Prop}
  (h₁ : P 1) (h₂ : ∀ a ∈ l, P a) (h₃ : ∀ a b : α, P a → P b → P (a * b)) : P l.prod :=
foldl_rec_on l _ _ ‹_› $ λ _ _ _ hy, h₃ _ _ ‹_› (h₂ _ hy)

end list

[Junyan Xu]

Nice proof! I weakened the assumptions to [has_one] [has_mul] and filled in the ‹_›.

lemma prod_prop {α : Type*} [has_mul α] [has_one α] {l : list α} {P : α → Prop}
  (h₁ : P 1) (h₂ : ∀ a ∈ l, P a) (h₃ : ∀ a b : α, P a → P b → P (a * b)) : P l.prod :=
foldl_rec_on l _ _ h₁ $ λ _ h _ hy, h₃ _ _ h (h₂ _ hy)

Although it's just a trivial application of docs#list.foldl_rec_on, I think it would be nice to have a specialization of it to list.prod in mathlib. A direct specialization would be:

lemma prod_prop' {α : Type*} [has_mul α] [has_one α] {l : list α} {P : α → Prop}
  (h₁ : P 1) (h₂ : ∀ a, P a → ∀ b, b ∈ l → P (a * b)) : P l.prod := foldl_rec_on l _ _ h₁ h₂

Which one should we prefer?

[Junyan Xu]

Although prod_prop would be nice to have, for the purpose of the Jacobi symbol PR (which I think is the application @Michael Stoll has in mind) the following is probably the easiest:

lemma jacobi_sym_trichotomy (a : ℤ) (b : ℕ) : [a | b]ⱼ = 0 ∨ [a | b]ⱼ = 1 ∨ [a | b]ⱼ = -1 :=
submonoid.list_prod_mem
  ⟨({0, 1, -1} : set ℤ),
   by rintro _ _ (rfl|rfl|(rfl : _ = _)) (rfl|rfl|(rfl : _ = _)); dec_trivial,
   or.inr (or.inl rfl)⟩
begin
  intros _ ha',
  rcases list.mem_pmap.mp ha' with ⟨p, hp, rfl⟩,
  haveI : fact p.prime := ⟨prime_of_mem_factors hp⟩,
  exact quadratic_char_is_quadratic (zmod p) a,
end

and I also think it's a good idea to extract the submonoid to a separate definition.

[Michael Stoll]

@Junyan Xu Nice. I'm defining int.sign_monoid as the submonoid in question and use that in your proof.

[Junyan Xu]

Actually, do people think we should generalize sign_monoid to non_assoc_ring? (I think dec_trivial won't work then.) And should the name be sign_submonoid?

[Michael Stoll]

sign_submonoid is better, I think. In which file should this go eventually?

[Yaël Dillies]

Is this meant to be units + zero, or {-1, 0, 1}?

[Junyan Xu]

The latter.

[Yaël Dillies]

I assume you cannot use docs#sign_type because you want a submonoid?

[Michael Stoll]

Yes, and you may want to compute with the values of the Jacobi symbol as integers (in particular, add them up or use them as coefficients of a linear combination).

[Junyan Xu]

I think there's a possibility of defining quadratic_char, legendre_sym, and jacobi_sym all taking values in sign_type, and use docs#sign_type.cast_hom when we want to work in Z; I think we've considered something like that before, but I forgot about the reasoning that led to the current design.

[Yakov Pechersky]

@Junyan Xu i used the French quote syntax as a shorthand for the assumption tactic

[Junyan Xu]

Yes I know but why not pure term-mode when it can be easily achieved :)

[Michael Stoll]

Junyan Xu said:

I think there's a possibility of defining quadratic_char, legendre_sym, and jacobi_sym all taking values in sign_type, and use docs#sign_type.cast_hom when we want to work in Z; I think we've considered something like that before, but I forgot about the reasoning that led to the current design.

You want to be able to work with more general multiplicative characters (e.g., for cubic reciprocity @Kevin Buzzard), not just ones that take values in {0, 1, -1}. I think it makes sense to have quadratic characters as a special case of multiplicative characters (and avoid the cast from sign_type to the integers whenever you want to do some nontrivial computation with the values).

[Junyan Xu]

I think it would be nice to make definitions more polymorphic. For example, docs#add_char.primitive_add_char is defined with domain cyclotomic_field n R', but it could be defined for any ring, and docs#add_char.primitive_zmod_char could be defined for any ring with a primitive n-th root of unity. If you make them polymorphic like this, I think you won't need to map the values from the cyclotomic field to a larger field in some of your Gauss sum proofs. (Edit: seems I got it backwards, you're mapping something smaller into the cyclotomic field, not the other way.)
For quadratic characters, I think defining a sign_type version and using cast to get to any ring will make it the most polymorphic, but some work may be needed to make it pleasant to work with casts.
Moreover, the cubic stuff doesn't take values in Z, so it seems to strengthen the point of being able to work with different domains.

[Michael Stoll]

You can already do the following, if you like.

import number_theory.legendre_symbol.mul_character
import data.sign

def χ : mul_char (zmod 3) sign_type :=
{ to_fun := λ x, ite (x = 0) 0 (ite (is_square x) 1 (-1)),
  map_one' := rfl,
  map_mul' := dec_trivial,
  map_nonunit' := dec_trivial }

[Michael Stoll]

But as soon as you want to do Gauss sums, say, you'll have to cast to a ring anyway (and ℤ is the universal ring, so it makes sense to have ℤ as the domain).

[Michael Stoll]

The only possible advantage I see right now is that the proof of the trichotomy gets simpler. I'm not sure this is worth it.

[Michael Stoll]

How would you prove docs#quadratic_char_fun_eq_pow_of_char_ne_two in a setting where the character takes values in sign_type?

[Yaël Dillies]

By using injectivity of coe : sign_type → F?

[Michael Stoll]

Yes, but it will be more complicated. The point I'm trying to make is that there is a trade-off, and I am not convinced that the pros outweigh the cons.

[Michael Stoll]

docs#quadratic_char_eq_pow_of_char_ne_two', docs#quadratic_char_card_sqrts

[Yaël Dillies]

You are about to define something isomorphic to sign_type for each ring. There are reasons to be worried!

[Michael Stoll]

docs#quadratic_char_sum_zero

[Junyan Xu]

sign_submonoid is only defined for integers now, it's me who suggested non_assoc_ring.

[Yaël Dillies]

Michael, all lemmas you're linking to genuinely all seem fine with sign_type to me.

[Michael Stoll]

Is there a way to define sign_submonoid as the image of the monoid(_with_zero) homomorphism from sign_typeinto any (non_assoc_)ring? (And use it as easily!)

[Michael Stoll]

The last one uses docs#mul_char.is_nontrivial.sum_eq_zero, for which your target needs to be a domain.

[Michael Stoll]

In my example above, #check χ 1 + 1 complains failed to synthesize type class instance for ⊢ has_add sign_type, so it looks like you have to cast to ℤ explicitly: (χ 1 : ℤ) + 1 (↑(χ 1) + 1 doesn't cut it; it wants to cast to ℕ).

[Yaël Dillies]

Is that a problem?

[Michael Stoll]

It looks clumsy in the statements. I prefer the statements to look as similar as possible to the way you'd write the mathematics they represent.

[Yaël Dillies]

Coercions are on the least clumsy end of the spectrum of things formalisation can introducate in a statement.

[Michael Stoll]

But why introduce them if they are not necessary?
It is not clear to me what you are trying to optimize here. I don't think the mere fact that sign_type exists implies that it has to be used at all costs. As I said earlier, I think using it here would have more disadvantages than advantages.

[Yaël Dillies]

Here it gives you a unique interface for all rings, rather than several submonoids you will need to connect with explicit maps (which might mess you up because submonoids have a coercion to Type).

[Yaël Dillies]

Further, all the basic logic would shared between both types and that makes yet another pair of API that we have to keep in sync.

[Michael Stoll]

I just need the submonoid of the integers (the universal ring). As @Junyan Xu said, generalizing this was his idea.

[Eric Wieser]

The submonoid is (⊤ : submonoid sign_type).map sign_type.cast_hom, right?

[Eric Wieser]

Or even monoid_hom.mrange sign_type.cast_hom

[Michael Stoll]

In the concrete case, monoid_hom.mrange $ @sign_type.cast_hom ℤ _ _ or so. But then the proof which uses it does not work anymore; I'll have to look into that.

[Michael Stoll]

It looks like it's hard to get a reasonably simple proof of the result I want (jacobi_sym_trichotomy) with the monoid_hom.mrange sign_type.cast_hom approach.
Since I need this submonoid olny for this one proof, I will just use it locally (as in @Junyan Xu's original suggestion).

[Eric Wieser]

What does "doesn't work" mean here?

[Junyan Xu]

The following works:

namespace sign_type
lemma range_eq {α} (f : sign_type → α) : set.range f = {f zero, f pos, f neg} :=
begin
  ext, split,
  { rintro ⟨s|s|s, rfl⟩, exacts [or.inl rfl, or.inr $ or.inr rfl, or.inr $ or.inl rfl] },
  { rintro (rfl|rfl|(rfl : _ = _)); apply set.mem_range_self },
end
end sign_type

lemma jacobi_sym_trichotomy (a : ℤ) (b : ℕ) : [a | b]ⱼ = 0 ∨ [a | b]ⱼ = 1 ∨ [a | b]ⱼ = -1 :=
((@sign_type.cast_hom ℤ _ _).to_monoid_hom.mrange.copy _
  (sign_type.range_eq sign_type.cast_hom).symm).list_prod_mem
begin
  intros _ ha',
  rcases list.mem_pmap.mp ha' with ⟨p, hp, rfl⟩,
  haveI : fact p.prime := ⟨prime_of_mem_factors hp⟩,
  exact quadratic_char_is_quadratic (zmod p) a,
end

[Michael Stoll]

Yes, but I think your original proof is simpler (no need to introduce sign_type.range_eq).

[Michael Stoll]

Eric Wieser said:

What does "doesn't work" mean here?

"Doesn't work" means that one needs the additional step provided by @Junyan Xu's code above.

[Junyan Xu]

The original seems simpler but is slower (about 2s, while the one that uses sign_type takes ~0.25s), and sign_type.range_eq could be used elsewhere (it also takes about 0.25s). By the way should lemmas like range_eq be auto-generated? Though the auto-generated lemma would have {zero, neg, pos} instead of what we want ({zero, pos, neg}).

[Alex J. Best]

Yeah I feel like we should generate this change statement as a lemma automagically as part of derive fintype, then a proof could be

import tactic
import data.sign
namespace sign_type
lemma range_eq {α} (f : sign_type → α) : set.range f = {f zero, f neg, f pos} :=
begin
  classical,
  rw ← fintype.coe_image_univ,
  change (finset.univ : finset sign_type) with {zero, neg, pos},
  simp,
end

[Junyan Xu]

This should work for any fintype:

lemma range_eq {α} (f : sign_type → α) : set.range f = {f zero, f neg, f pos} :=
begin
  classical,
  simp only [← finset.coe_singleton, ← finset.image_singleton,
    ← fintype.coe_image_univ, finset.coe_image, ← set.image_insert_eq],
  refl,
end

[Michael Stoll]

So what should I do now?
Add sign_type.range_eq (with [fintype α] added?) to data.sign and change the order in the definition of mul_char.is_quadratic (and everything that uses it) to 0, -1, 1, so that it is compatible with the order given in range_eq?

[Michael Stoll]

(I would like to get on with getting the Jacobi symbol into mathlib without getting lost in too many rabbit holes...)

[Junyan Xu]

To me the order {0,1,-1} is more natural than {0,-1,1}, so if any definition is to be changed it should be sign_type. However you don't have to change any definition; you could just do a rewrite:

lemma jacobi_sym_trichotomy (a : ℤ) (b : ℕ) : [a | b]ⱼ = 0 ∨ [a | b]ⱼ = 1 ∨ [a | b]ⱼ = -1 :=
((@sign_type.cast_hom ℤ _ _).to_monoid_hom.mrange.copy {0, 1, -1} $
  by {rw set.pair_comm, exact (sign_type.range_eq sign_type.cast_hom).symm}).list_prod_mem
begin
  intros _ ha',
  rcases list.mem_pmap.mp ha' with ⟨p, hp, rfl⟩,
  haveI : fact p.prime := ⟨prime_of_mem_factors hp⟩,
  exact quadratic_char_is_quadratic (zmod p) a,
end

[Michael Stoll]

OK; then I'll do that (and add eq_range).

[Eric Wieser]

Just to check; is docs#jacobi_sym in master? I don't see the definition upthread

[Junyan Xu]

It's not in master; it was in PR #16290 but now removed from it, to be added in a later PR. (#16290 now is preliminary lemmas only.) Discussions are in this thread.