Transforming the type of a function

Stream: new members

[Patrick Stevens]

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]

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

[Patrick Stevens]

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]

finset X is the type of finite subsets of X

[Kevin Buzzard]

Not the assertion that X is finite

[Patrick Stevens]

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]

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

[Johan Commelin]

But what is f in your case?

[Kevin Buzzard]

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]

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]

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]

I need the term of type nat.prime p when I call this

[Patrick Stevens]

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]

But you don't use is_prime in that defintion, right?

[Patrick Stevens]

I use it to prove that p is not 1, for example

[Johan Commelin]

Ooh, you do, because of the .get

[Kevin Buzzard]

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]

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]

I think you want finset.attach.

[Reid Barton]

And prod_attach

[Patrick Stevens]

I use finset.attach to create this in the first place, yes

[Johan Commelin]

@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]

Oh, prod_attach looks promising

[Patrick Stevens]

Hah, that does sound quite mathlibby, actually

[Patrick Stevens]

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

[Johan Commelin]

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

[Mario Carneiro]

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]

But padic_val probably isn't defined for arbitrary p.

[Johan Commelin]

So in that case you need the attach approach

[Patrick Stevens]

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]

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

[Johan Commelin]

Wrong thread?

[Patrick Stevens]

No, I see

[Kevin Buzzard]

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

[Patrick Stevens]

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

[Kevin Buzzard]

There is fintype for proving that a type is finite.

[Johan Commelin]

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

[Johan Commelin]

Aha, I see. I have to scroll up.

[Mario Carneiro]

It's a bit disappointing that there is no padic_val_nat

[Johan Commelin]

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

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

[Johan Commelin]

That's what I would go for, I think

[Patrick Stevens]

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

[Patrick Stevens]

Such is life

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Then you don't loose that much work at all

[Mario Carneiro]

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]

Yeah, I suspect lots of it should be salvageable

[Patrick Stevens]

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]

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]

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]

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)