bigop convert range to ordinal · math-comp users

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):

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):

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):

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):

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

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 (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:

Stream: math-comp users

Topic: bigop convert range to ordinal

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