Stream: math-comp users

Topic: bigop convert range to ordinal


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

view this post on Zulip Cyril Cohen (Oct 16 2020 at 14:06):

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

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

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

view this post on Zulip Ana de Almeida Borges (Oct 16 2020 at 15:35):

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 23 2020 at 13:31):

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

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

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

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

view this post on Zulip Emilio Jesús Gallego Arias (Oct 23 2020 at 14:13):

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

view this post on Zulip Ana de Almeida Borges (Oct 23 2020 at 14:17):

Both great answers, thank you!

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

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

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

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

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

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