Stream: general

Topic: is this a pattern

Johan Commelin (Apr 29 2020 at 06:55):

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 (Apr 29 2020 at 06:57):

what is the goal?

(abstractly)

Mario Carneiro (Apr 29 2020 at 06:58):

that is, what would you like to write?

Johan Commelin (Apr 29 2020 at 07:01):

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 (Apr 29 2020 at 07:04):

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

Johan Commelin (Apr 29 2020 at 07:04):

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 (Apr 29 2020 at 07:04):

equiv.sigma_preimage_equiv

Mario Carneiro (Apr 29 2020 at 07:05):

In this case, the function is the ith projection

Mario Carneiro (Apr 29 2020 at 07:06):

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

Johan Commelin (Apr 29 2020 at 07:07):

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

Johan Commelin (Apr 29 2020 at 07:07):

But I can try to see what happens

Mario Carneiro (Apr 29 2020 at 07:07):

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

Johan Commelin (Apr 29 2020 at 10:16):

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 (Apr 29 2020 at 13:16):

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

Johan Commelin (Apr 30 2020 at 08:54):

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