# Zulip Chat Archive

## 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-`prime`

s 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
```

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

Wrong thread?

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

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`

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

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