nat.antidiagonal for pi types

Stream: Is there code for X?

[Eric Wieser]

Do we have a variant of docs#finset.nat.antidiagonal that produces a k-way split?

/-- When k=2 this is the "same" as finset.nat.antidiagonal -/
def finset.nat.antidiagonal' (n : ℕ) (k : ℕ) :
  finset (fin k → ℕ) := sorry

def finset.nat.mem_antidiagonal' {n : ℕ} {k : ℕ} (x : fin k → ℕ) :
  x ∈ finset.nat.antidiagonal' n k ↔ ∑ i : fin k, x i = n := sorry

[Yaël Dillies]

We have docs#std_simplex, which is pretty close.

[Eric Wieser]

I was thinking something like

import data.finset
import data.fin.tuple
import data.fin.vec_notation

open_locale big_operators

def list.nat.antidiagonal' : ℕ → Π k, list (fin k → ℕ)
| n 1 := [![n]]
| n (k + 1) := (list.range n.succ).reverse.bind $ λ ni,
  (list.nat.antidiagonal' ni k).map $ λ x, fin.cons (n - ni) x

#eval list.nat.antidiagonal' 2 3
-- [![0, 0, 2], ![0, 1, 1], ![0, 2, 0], ![1, 0, 1], ![1, 1, 0], ![2, 0, 0]]

[Yaël Dillies]

Why not simply filtering out fintype.pi_finset (λ _, range n)?

[Eric Wieser]

Can you make a #mwe?

[Eric Wieser]

But I think one answer is "that's way slower to compute"

[Yaël Dillies]

import algebra.big_operators.order

open finset fintype
open_locale big_operators

variables (ι : Type*) {α : Type*} [fintype ι] [decidable_eq ι] (n : ℕ)

def finset.nat.antidiagonal' (n : ℕ) : finset (ι → ℕ) :=
(pi_finset $ λ _, range $ n + 1).filter $ λ f, ∑ i, f i = n

variables {ι n} {f : ι → ℕ}

lemma finset.nat.mem_antidiagonal'_iff : f ∈ finset.nat.antidiagonal' ι n ↔ ∑ i, f i = n :=
begin
  refine mem_filter.trans (and_iff_right_of_imp $ λ h, _),
  simp_rw [mem_pi_finset, mem_range, nat.lt_succ_iff],
  exact λ i, (single_le_sum (λ j _, nat.zero_le _) (mem_univ _)).trans h.le,
end

[Eric Wieser]

Admittedly the proof is easier there

[Yaël Dillies]

Why do you care about computation?

[Eric Wieser]

We cared about it for finset.nat.antidiagonal

[Eric Wieser]

it seems sensible to be consistent

[Yaël Dillies]

Why did we care back then?

[Eric Wieser]

It's entirely conceivable that norm_num would want to actually iterate over an antidiagonal?

[Yaël Dillies]

Note that @Alex J. Best recently made stuff less computable in this area. #10891 and #10930

[Alex J. Best]

Well I only changed the definition of trunc? So I don't think I changed too much. Certainly it could be that the new definition is less computable in some sense? But the target of trunc is highly noncomputable anyway so I'm not sure I made any difference at all

[Eric Wieser]

PRd as #13031