Zulip Chat Archive

Stream: new members

Topic: Transforming the type of a function


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (May 27 2020 at 20:48):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 27 2020 at 20:51):

finset X is the type of finite subsets of X

view this post on Zulip Kevin Buzzard (May 27 2020 at 20:51):

Not the assertion that X is finite

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 27 2020 at 20:52):

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

view this post on Zulip Johan Commelin (May 27 2020 at 20:53):

But what is f in your case?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Patrick Stevens (May 27 2020 at 20:54):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 27 2020 at 20:55):

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

view this post on Zulip Patrick Stevens (May 27 2020 at 20:55):

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

view this post on Zulip Johan Commelin (May 27 2020 at 20:55):

Ooh, you do, because of the .get

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Reid Barton (May 27 2020 at 20:57):

I think you want finset.attach.

view this post on Zulip Reid Barton (May 27 2020 at 20:57):

And prod_attach

view this post on Zulip Patrick Stevens (May 27 2020 at 20:57):

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

view this post on Zulip 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

view this post on Zulip Patrick Stevens (May 27 2020 at 20:57):

Oh, prod_attach looks promising

view this post on Zulip Patrick Stevens (May 27 2020 at 20:58):

Hah, that does sound quite mathlibby, actually

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Johan Commelin (May 27 2020 at 21:00):

But padic_val probably isn't defined for arbitrary p.

view this post on Zulip Johan Commelin (May 27 2020 at 21:00):

So in that case you need the attach approach

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 27 2020 at 21:01):

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

view this post on Zulip Johan Commelin (May 27 2020 at 21:01):

Wrong thread?

view this post on Zulip Patrick Stevens (May 27 2020 at 21:01):

No, I see

view this post on Zulip 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

view this post on Zulip Patrick Stevens (May 27 2020 at 21:02):

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

view this post on Zulip Kevin Buzzard (May 27 2020 at 21:02):

There is fintype for proving that a type is finite.

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 27 2020 at 21:03):

Aha, I see. I have to scroll up.

view this post on Zulip Mario Carneiro (May 27 2020 at 21:04):

It's a bit disappointing that there is no padic_val_nat

view this post on Zulip 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

view this post on Zulip Johan Commelin (May 27 2020 at 21:05):

That's what I would go for, I think

view this post on Zulip Patrick Stevens (May 27 2020 at 21:06):

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

view this post on Zulip Patrick Stevens (May 27 2020 at 21:06):

Such is life

view this post on Zulip Johan Commelin (May 27 2020 at 21:08):

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

view this post 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.

view this post on Zulip Johan Commelin (May 27 2020 at 21:09):

Then you don't loose that much work at all

view this post on Zulip 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

view this post on Zulip Patrick Stevens (May 27 2020 at 21:09):

Yeah, I suspect lots of it should be salvageable

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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