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: Oct 13 2024 at 01:02 UTC