## Stream: math-comp users

### Topic: bigop convert range to ordinal

#### Daniel Kirk (Oct 16 2020 at 13:47):

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.

#### Cyril Cohen (Oct 16 2020 at 14:06):

does rewrite big_enum; under eq_bigr do rewrite big_enum. work?

#### Daniel Kirk (Oct 16 2020 at 14:40):

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.

#### Daniel Kirk (Oct 16 2020 at 14:41):

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.

#### Ana de Almeida Borges (Oct 16 2020 at 15:35):

From there can you use card_ord to get what you want?

#### Daniel Kirk (Oct 17 2020 at 18:12):

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

#### Daniel Kirk (Oct 17 2020 at 18:13):

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]|".


#### Ana de Almeida Borges (Oct 23 2020 at 13:12):

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.

#### Emilio Jesús Gallego Arias (Oct 23 2020 at 13:31):

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

#### Ana de Almeida Borges (Oct 23 2020 at 13:48):

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.


#### Christian Doczkal (Oct 23 2020 at 14:00):

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?

#### Emilio Jesús Gallego Arias (Oct 23 2020 at 14:09):

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 /=. 

#### Emilio Jesús Gallego Arias (Oct 23 2020 at 14:13):

you need to remove the val n coertion from the bigop body

#### Christian Doczkal (Oct 23 2020 at 14:19):

@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.

#### Ana de Almeida Borges (Oct 23 2020 at 14:21):

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!

#### Christian Doczkal (Oct 23 2020 at 14:42):

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."

#### Daniel Kirk (Oct 23 2020 at 15:10):

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?

#### Daniel Kirk (Oct 23 2020 at 15:25):

Oh actually big_enum_cond or in my case rewrite big_enum_cond; under eq_bigr do rewrite big_enum_cond. does this!

#### Christian Doczkal (Oct 23 2020 at 16:01):

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: Feb 02 2023 at 13:03 UTC