Stream: math-comp users

Topic: ✔ recursive function adn typechecing


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

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

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

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

How about this one?

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

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

view this post on Zulip Notification Bot (Jan 29 2022 at 10:43):

Laurent Théry has marked this topic as resolved.


Last updated: Feb 02 2023 at 15:04 UTC