## Stream: math-comp users

### Topic: ✔ recursive function adn typechecing

#### Laurent Théry (Jan 27 2022 at 11:48):

I would like to turn a recursion with natural number into a recursion with power of 2 .
Here is a dummy version with natural number :

``````From mathcomp Require Import all_ssreflect algebra.zmodp.

Fixpoint test m : seq 'I_m :=
if m is m1.+1 then
if m1 is _.+1 then [seq (inZp (i : 'I_m1)) | i <- test m1]
else [:: ord_max]
else [::].
``````

I've defined the power of 2

``````Fixpoint p2n n := if n is n1.+1 then p2n n1 + p2n n1 else 1.
``````

but now the direct translation

``````Fixpoint test1 m : seq 'I_(p2n m) :=
if m is m1.+1 then
if m1 is _.+1 then [seq (lshift _ (i : 'I_(p2n m1))) | i <- test1 m1]
else [:: ord_max]
else [::].
``````

does not typecheck anymore.

``````The term "[:: ord_max]" has type "seq 'I_?n'.+1"
while it is expected to have type "seq 'I_(p2n ?n0@{m2:=0})".
``````

I've managed to get somewhat what I want with

``````Fixpoint test1 m : seq 'I_(p2n m) :=
if m is m1.+1 then
if m1 is _.+1 then [seq (lshift _ (i : 'I_(p2n m1))) | i <- test1 m1]
else if m1 is 1 then [:: ord_max] else [::]
else [::].
``````

but is there some more elegant way to do this?

#### YAMAMOTO Mitsuharu (Jan 28 2022 at 11:28):

Laurent Théry said:

I've managed to get somewhat what I want with

``````Fixpoint test1 m : seq 'I_(p2n m) :=
if m is m1.+1 then
if m1 is _.+1 then [seq (lshift _ (i : 'I_(p2n m1))) | i <- test1 m1]
else if m1 is 1 then [:: ord_max] else [::]
else [::].
``````

This `test1` always returns `[::]`. Probably this is not what you intended.

``````Definition test1 m : seq 'I_(p2n m) :=
if m is m1.+1 then
(fix test1' m1 : seq 'I_(p2n m1.+1) :=
if m1 is m2.+1 then [seq lshift _ i | i <- test1' m2]
else [:: ord_max]) m1
else [::].
``````

#### Laurent Théry (Jan 28 2022 at 12:09):

YAMAMOTO Mitsuharu said:

``````This `test1` always returns `[::]`.  Probably this is not what you intended.
``````

Yes it is a dummy example that only means to show the type-checking problem I had.

Thanks, this fix inside a fix is a bit scary....

#### YAMAMOTO Mitsuharu (Jan 29 2022 at 05:53):

The internal `fix` can be made into an auxiliary `Fixpoint`. And that might make proofs simpler.

``````Fixpoint test1_aux m1 : seq 'I_(p2n m1.+1) :=
if m1 is m2.+1 then [seq lshift _ i | i <- test1_aux m2]
else [:: ord_max].

Definition test1 m : seq 'I_(p2n m) :=
if m is m1.+1 then test1_aux m1 else [::].
``````

#### Notification Bot (Jan 29 2022 at 10:43):

Laurent Théry has marked this topic as resolved.

Last updated: Jul 25 2024 at 17:02 UTC