Zulip Chat Archive

Stream: general

Topic: is this a pattern


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

view this post on Zulip Mario Carneiro (Apr 29 2020 at 06:57):

what is the goal?

view this post on Zulip Mario Carneiro (Apr 29 2020 at 06:57):

(abstractly)

view this post on Zulip Mario Carneiro (Apr 29 2020 at 06:58):

that is, what would you like to write?

view this post on Zulip Johan Commelin (Apr 29 2020 at 07:01):

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

(xKxiki)((x1,,xi^,,xn)Kn1x1k1xnkn)\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)

view this post on Zulip Mario Carneiro (Apr 29 2020 at 07:04):

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

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

view this post on Zulip Mario Carneiro (Apr 29 2020 at 07:04):

equiv.sigma_preimage_equiv

view this post on Zulip Mario Carneiro (Apr 29 2020 at 07:05):

In this case, the function is the ith projection

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

view this post on Zulip Johan Commelin (Apr 29 2020 at 07:07):

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

view this post on Zulip Johan Commelin (Apr 29 2020 at 07:07):

But I can try to see what happens

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

view this post on Zulip 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}  β) :=

view this post on Zulip Johan Commelin (Apr 29 2020 at 13:16):

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

view this post on Zulip Johan Commelin (Apr 30 2020 at 08:53):

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

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

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 11:13):

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


Last updated: May 08 2021 at 03:17 UTC