is this a pattern

Stream: general

[Johan Commelin]

On the chev-warn branch, I'm writing the following code:

  let S : finset (σ → K) := univ.filter (λ x, x i = 0),
  let stratified : finset (σ → K) := S.bind (λ x, univ.filter (λ y, ∀ j ≠ i, y j = x j)),
  have : stratified = univ,

It feels like this should be abstracted away into some general API, but I'm not sure what that should look like. Do people have useful suggestions?
https://github.com/leanprover-community/mathlib/pull/1564/files#diff-c5bb8de7cb26ae773e9bcb3fa594be6fR68-R70

[Mario Carneiro]

what is the goal?

[Mario Carneiro]

(abstractly)

[Mario Carneiro]

that is, what would you like to write?

[Johan Commelin]

Well, I have a multivariate monomial $X_1^{k_1} \cdot X_2^{k_2} \cdot X_n^{k_n}$ and I want to sum over the entire vector space $K^n$ (which makes sense, because $K$ is a finite field). Now I have some fixed index $i$, and so this total sum is equal to

$\left( \sum_{x \in K} x_i^{k_i} \right) \cdot \left( \sum_{(x_1, \dots, \hat{x_i}, \dots, x_n) \in K^{n-1}} x_1^{k_1} \cdots x_n^{k_n} \right)$

[Mario Carneiro]

It sort of reminds me of the equiv that stratifies a type over a function

[Johan Commelin]

So, use stratified = univ and then sum_bind, and afterwards I have to prove a lot of tedious proof obligations. It feels like they don't belong in the proof of Chev-Warn. But if I factor them out, I would prefer to factor them into something reusable.

[Mario Carneiro]

equiv.sigma_preimage_equiv

[Mario Carneiro]

In this case, the function is the ith projection

[Mario Carneiro]

You could transfer the sum over that equiv, and then break up the sum over a Sigma

[Johan Commelin]

Hmm, isn't it easier to do this with finsets in the same type?

[Johan Commelin]

But I can try to see what happens

[Mario Carneiro]

I think you will have to prove a lot of injectivity and surjectivity things with your proof

[Johan Commelin]

How should I call this equiv?

def equiv.foo (p : α → Prop) [decidable_pred p] (x₀ : {a // p a} → β) :
  {x : α → β // x ∘ coe = x₀} ≃ ({a // ¬ p a} → β) :=

[Johan Commelin]

@Mario Carneiro See https://github.com/leanprover-community/mathlib/pull/1564/commits/8b2cf7d3796dc113003cb43e10b9c079fb373970 for the result

[Johan Commelin]

Before-after: https://github.com/leanprover-community/mathlib/pull/1564/files/88a5f988abd92ea699824d72dd8c0fcdd5cd4ac0..60f01102933198521d31c2d58ad07651a23dccec#diff-c5bb8de7cb26ae773e9bcb3fa594be6fL57-R230

[Johan Commelin]

I think this proof can now be read if you only look at the lean code (even without interactive tactic state)

[Kevin Buzzard]

It's certainly much more readable. I thought mathlib had made a conscious decision not to be readable though ;-)