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?

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.

How about this one?

```
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 [::].
```

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.

How about this one?

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

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 [::].
```

Laurent Théry has marked this topic as resolved.

Last updated: Jul 25 2024 at 17:02 UTC