Hi all, I'm looking for the simplest way to convert the goal

"\sum_(i1 <- enum 'I_m) \sum_(i2 <- enum 'I_n) C i1 i2 *: delta_mx i1 i2 == 0 ->false"

to

"\sum_(i1 < m) \sum_(i2 < n) C i1 i2 *: delta_mx i1 i2 == 0 ->false"

My aim is to then use "matrix_sum_delta" to derive "C == 0 -> false" (here C is a matrix), but the details of "C i1 i2 *: delta_mx i1 i2" aren't too imporant I think.

I've tried everything I can find in bigop.v and can't figure it out. It looks like it should be simple enough but every lemma seems to throw up extra complexity.

Many thanks.

does `rewrite big_enum; under eq_bigr do rewrite big_enum.`

work?

It converts to "\sum_(i in 'I_m) \sum_(i0 in 'I_n) C i i0 *: delta_mx i i0 == 0 -> false" but I'm not sure how to convert to the ordinal range from there.

using big_enum_val in place of big_enum gives "\sum_(i < #|'I_m|) \sum_(i0 < #|'I_n|) C (enum_val i) (enum_val i0) *: delta_mx (enum_val i) (enum_val i0) ==0 -> false"

Which is closer to what I need, but matrix_sum_delta is very particular with the form it requires.

From there can you use `card_ord`

to get what you want?

Unfortunately I get a Dependent type error when I try that. If it helps the specific error message is:

```
Dependent type error in rewrite of (fun _pattern_value_ : nat =>
\sum_(i < _pattern_value_)
\sum_(i0 < #|'I_n|)
C (enum_val i) (enum_val i0) *:
delta_mx (enum_val i) (enum_val i0) ==
0 -> false)
Type error was: Illegal application:
The term "@enum_val" of type
"forall (T : finType) (A : {pred T}), 'I_#|[eta A]| -> T"
cannot be applied to the terms
"ordinal_finType m" : "finType"
"pred_of_simpl (T:='I_m) 'I_m" : "pred 'I_m"
"i" : "'I__pattern_value_"
The 3rd term has type "'I__pattern_value_" which should be coercible to
"'I_#|[eta 'I_m]|".
```

I've now spent more than half an hour trying to solve this problem and I'm completely stumped. I'd really like to know the answer to this question too.

Can you be more specific as what code are you trying?

```
From mathcomp Require Import all_ssreflect.
Lemma bigmax_enum (n : nat) :
\max_(x <- enum 'I_n.+1) x = n.
Proof.
rewrite big_enum big_enum_val /=.
Fail rewrite card_ord.
Abort.
```

Umm, if you do `rewrite big_enum -[LHS]/(\max_(i < n.+1) i).`

you obtain `\max_(i < n.+1) i = n`

. Is that what you want? The `_(i < n)`

is convertible to `_(i in 'I_n)`

. Is that what you were trying to do?

I guess the problem is that still the dependent indexes are in the body of the bigop, that's tricky, I don't know a better way than ```
rewrite -(big_map val [pred x | true] id) val_enum_ord /=.
```

you need to remove the `val n`

coertion from the bigop body

Both great answers, thank you!

@Ana de Almeida Borges , note that you don't even need to do the conversion. Lemmas of with an "ordinal range" apply also the convertible `_(i in 'I_n)`

form.

Christian Doczkal said:

Ana de Almeida Borges , note that you don't even need to do the conversion. Lemmas of with an "ordinal range" apply also the convertible

`_(i in 'I_n)`

form.

That explains why I couldn't find any lemmas with the `_(i in 'I_n)`

form!

Yes, this is a minor variation of the usual mathcomp wisdom: "If there is an obvious equality missing for some concept, that's likely the definition."

Does this work the other way? Does `_ (i in 'I_n)`

convert to `_ < n`

? Or is there a lemma to convert the range to ordinal?

Oh actually `big_enum_cond`

or in my case `rewrite big_enum_cond; under eq_bigr do rewrite big_enum_cond.`

does this!

Yes, I suppose it's not particularly newcomer-friendly to have the `i`

in the body of `big[_/_]_(n <= i < m) F i`

be a `nat`

while in `big[_/_]_(i < n) F i`

, we have `i : 'I_n`

. :shrug:

Last updated: Jul 25 2024 at 16:02 UTC