## Stream: new members

### Topic: Transforming the type of a function

#### Patrick Stevens (May 27 2020 at 20:28):

I've got the following definition, where I want to get the restrictions into the type because I'm going to end up taking a product of a function a (n : nat) (is_prime : nat.prime n) : nat over this set, and this way I can just use bigoperators.

import tactic
import data.subtype

def primes_le (n : nat) : finset {m : nat // m ≤ n ∧ nat.prime m} :=
begin
have r : finset {m : nat // m ≤ n ∧ nat.prime m} = finset {m : nat // m < n + 1 ∧ nat.prime m},
{ congr, ext,
split,
{ rintros ⟨x_le_n, x_prime⟩,
exact ⟨nat.lt_succ_iff.mpr x_le_n, x_prime⟩, },
{ rintros ⟨x_lt_sn, x_prime⟩,
exact ⟨nat.lt_succ_iff.mp x_lt_sn, x_prime ⟩, }, },
simpa only [r, finset.mem_filter, finset.mem_range] using (finset.filter nat.prime (finset.range (n + 1))).attach,
end


However, proving anything about this set is not obviously possible; it doesn't behave nicely under unfold, which is to be expected because I'm in tactic mode, which is always a big no-no when defining a function.

I'm going to want both m <= n and nat.prime m in scope when I take my product over primes_le n. One way to proceed is to just use finset.filter nat.prime (finset.range (n + 1)) in the definition of primes_le, and then at every call site I could prove m <= n and nat.prime m; another way would be to provide an explicit function finset {m:nat // m \in finset.filter nat.prime (finset.range (n + 1))} to finset {m : nat // m <= n and nat.prime m} and compose that with my primes_le. What's the One True Answer? I'm inclined to think the latter.

#### Kevin Buzzard (May 27 2020 at 20:48):

You're defining a certain finite subset of the primes which are at most n?

#### Patrick Stevens (May 27 2020 at 20:51):

I'm defining exactly the primes which are at most n, but I need the fact that they're at most n to be stored with them, so that when I prod x in primes_le 10, f x I'll be able to pass the fact that x is prime into f

#### Kevin Buzzard (May 27 2020 at 20:51):

finset X is the type of finite subsets of X

#### Kevin Buzzard (May 27 2020 at 20:51):

Not the assertion that X is finite

#### Patrick Stevens (May 27 2020 at 20:52):

In fact my next theorem, the one that sparked this question, is a proof that primes_le 10 contains every prime leq 10

#### Johan Commelin (May 27 2020 at 20:52):

@Patrick Stevens There's a bit of an art to using finset.prod and finset.sum

#### Johan Commelin (May 27 2020 at 20:53):

But what is f in your case?

#### Kevin Buzzard (May 27 2020 at 20:53):

Are you sure that this is true though? You're using simp to construct data. I have no idea what data it constructed. It's like you defined a natural number using simp and are now complaining that you don't know what it is

#### Johan Commelin (May 27 2020 at 20:53):

I think primes_le n := (range (n+1)).filter prime would work. Haven't you used something like that in the other PRs?

#### Patrick Stevens (May 27 2020 at 20:54):

I don't know if it has a good name, it's used in Erdos's proof of Bertrand's postulate, it's the multiplicity of the prime p in 2n choose n:

import data.subtype
import data.nat.prime
import data.nat.choose
import data.nat.multiplicity
import ring_theory.multiplicity
import tactic

open_locale big_operators

private def α (n : nat) (pos : 0 < n) (p : nat) (is_prime : nat.prime p) : nat :=
(multiplicity p (nat.choose (2 * n) n)).get $begin have not_one : p ≠ 1 := nat.prime.ne_one is_prime, have pos : 0 < nat.choose (2 * n) n := nat.choose_pos (by linarith), have fin : multiplicity.finite p (nat.choose (2 * n) n) := (@multiplicity.finite_nat_iff p (nat.choose (2 * n) n)).2 ⟨not_one, pos⟩, exact (multiplicity.finite_iff_dom.1 fin), end  #### Patrick Stevens (May 27 2020 at 20:54): I need the term of type nat.prime p when I call this #### Patrick Stevens (May 27 2020 at 20:55): I'm not using simp to construct data, as such - at least, not from a programmer's perspective; I'm using simp to transform the type of that data #### Johan Commelin (May 27 2020 at 20:55): But you don't use is_prime in that defintion, right? #### Patrick Stevens (May 27 2020 at 20:55): I use it to prove that p is not 1, for example #### Johan Commelin (May 27 2020 at 20:55): Ooh, you do, because of the .get #### Kevin Buzzard (May 27 2020 at 20:55): Johan's idea will give you this. You're using complicated tactics to define data which can't be right. Complicated tactics are for proofs. Do you understand what I'm saying about what finset X means? #### Patrick Stevens (May 27 2020 at 20:56): I do understand, yes; I have an auxiliary lemma I'm going to prove immediately afterwards stating that while all I know of primes_le from its type alone is that it is some finite subset of {primes less than or equal to n}, in fact it contains all the primes less than or equal to n #### Reid Barton (May 27 2020 at 20:57): I think you want finset.attach. #### Reid Barton (May 27 2020 at 20:57): And prod_attach #### Patrick Stevens (May 27 2020 at 20:57): I use finset.attach to create this in the first place, yes #### Johan Commelin (May 27 2020 at 20:57): @Patrick Stevens One option is to cheat, and define your function on non-primes as well: private def α (n : nat) (pos : 0 < n) (p : nat) : nat := if hp : p.prime then (multiplicity p (nat.choose (2 * n) n)).get$
begin
have not_one : p ≠ 1 := hp.ne_one,
have pos : 0 < nat.choose (2 * n) n := nat.choose_pos (by linarith),
have fin : multiplicity.finite p (nat.choose (2 * n) n) :=
(@multiplicity.finite_nat_iff p (nat.choose (2 * n) n)).2 ⟨not_one, pos⟩,
exact (multiplicity.finite_iff_dom.1 fin),
end
else 0


#### Patrick Stevens (May 27 2020 at 20:57):

Oh, prod_attach looks promising

#### Patrick Stevens (May 27 2020 at 20:58):

Hah, that does sound quite mathlibby, actually

#### Patrick Stevens (May 27 2020 at 20:58):

Thanks, I'll see if I can prod_attach it and also see what it looks like with that cheat

#### Johan Commelin (May 27 2020 at 20:59):

Also, to make it readable, I would put the proof that you pass to .get in a lemma

#### Mario Carneiro (May 27 2020 at 20:59):

Isn't this already defined? I think the name padic_val is not good for it (in metamath I used "pCnt" or "prime count" because p-adic valuation could also mean 1/p^k)

#### Johan Commelin (May 27 2020 at 21:00):

But padic_val probably isn't defined for arbitrary p.

#### Johan Commelin (May 27 2020 at 21:00):

So in that case you need the attach approach

#### Patrick Stevens (May 27 2020 at 21:00):

Actually looks like it uses the cheat:

def padic_val_rat (p : ℕ) (q : ℚ) : ℤ :=
if h : q ≠ 0 ∧ p ≠ 1
then (multiplicity (p : ℤ) q.num).get
(multiplicity.finite_int_iff.2 ⟨h.2, rat.num_ne_zero_of_ne_zero h.1⟩) -
(multiplicity (p : ℤ) q.denom).get
(multiplicity.finite_int_iff.2 ⟨h.2, by exact_mod_cast rat.denom_ne_zero _⟩)
else 0


#### Kevin Buzzard (May 27 2020 at 21:01):

def n : ℕ := by simpa only [has_zero] using 1


No, I see

#### Kevin Buzzard (May 27 2020 at 21:02):

I don't understand why Patrick's proposal for a definition isn't as crazy as what I just wrote

#### Patrick Stevens (May 27 2020 at 21:02):

How do I know simp has actually used what I told it to use

#### Kevin Buzzard (May 27 2020 at 21:02):

There is fintype for proving that a type is finite.

#### Johan Commelin (May 27 2020 at 21:03):

This is talking about another definition, i guess. Not the \a that we were discussing right now

#### Johan Commelin (May 27 2020 at 21:03):

Aha, I see. I have to scroll up.

#### Mario Carneiro (May 27 2020 at 21:04):

It's a bit disappointing that there is no padic_val_nat

#### Johan Commelin (May 27 2020 at 21:05):

def primes_le (n) := (range (n+1)).filter prime

def foo := \prod p in primes_le n, padic_val(_nat) p n


#### Johan Commelin (May 27 2020 at 21:05):

That's what I would go for, I think

#### Patrick Stevens (May 27 2020 at 21:06):

Sigh, I've got a nontrivial amount of proof about the properties of my existing \a

Such is life

#### Johan Commelin (May 27 2020 at 21:08):

@Patrick Stevens So... ask more questions on zulip

#### Johan Commelin (May 27 2020 at 21:09):

Also, maybe you can just rename your \a to padic_val_nat and weaken the assumptions a bit.

#### Johan Commelin (May 27 2020 at 21:09):

Then you don't loose that much work at all

#### Mario Carneiro (May 27 2020 at 21:09):

Your definition neatly decomposes as the padic_val of a particular number. Any theorems that are just theorems about padic_val should be generalized (and are probably already proven), and stuff about the central binomial coefficient should still be in your proof as before

#### Patrick Stevens (May 27 2020 at 21:09):

Yeah, I suspect lots of it should be salvageable

#### Patrick Stevens (May 30 2020 at 10:37):

So people wouldn't object to me adding a new function padic_val_nat in the general neighbourhood of the existing mathlib lemma padic_val_rat_of_int (z : ℤ) (hp : p ≠ 1) (hz : z ≠ 0) : padic_val_rat p (z : ℚ) = (multiplicity (p : ℤ) z).get (finite_int_iff.2 ⟨hp, hz⟩) that calls through to padic_val_rat, along with lemmas like padic_val_rat_of_int that equate it with the existing padic_val_rat?

#### Reid Barton (May 30 2020 at 10:40):

Maybe @Rob Lewis or @Chris Hughes could chime in, because I think there used to be something called padic_val or padic_val_nat that was replaced by multiplicity, and was very similar to what you are suggesting

#### Chris Hughes (May 30 2020 at 10:52):

I can believe that replacing padic_val with multiplicity was a mistake. It happens all the time that you want to raise something to the power of the multiplicity, and obviously this gets messy. I think the best way is to state theorems in the form (n : nat) (hn : n ∈ multiplicity p x) so you don't have get in all the statements, which I did not do when I wrote multiplicity. This might make the interface okay, but it also may well be worth having a version that defaults to zero.

#### Mario Carneiro (May 30 2020 at 11:12):

Since (multiplicity p x).dom is decidable, it should at least be possible to use (multiplicity p x).to_option.iget (there should be an roption.iget for this)

Last updated: May 14 2021 at 23:14 UTC