Stream: Coq users

Topic: Writing concatenation of sized lsit function ?

vlj (Aug 15 2021 at 21:43):

Hi, I'm having trouble writing a function that takes 2 sized list (eg the dependent type version of a list that takes the number of element as index):

Inductive SizedList {A:Type}: nat -> Type :=
| SizedNil : SizedList 0
| SizedCons : forall {n}, A -> SizedList n -> SizedList (n + 1)
.

and concatenate them ; my issue is with the return type, if n1 and n2 are the size of the input, I want an output of size n1 + n2. It works well for the nil case (likely because 0 + n is definitionally equal to n) but I have trouble for the cons case, basically I don't know how I can tell Coq that n + 1 + n2 is the same as n + n2 + 1 in the context of a function definition (eg not inside a proof). The code is :

Fixpoint concatSized {A:Type} {n1 n2: nat} (lst1: SizedList n1) (lst2: SizedList n2)
  : SizedList (n1 + n2)  :=
match lst1 in SizedList n3
return SizedList (n3 + n2)
with
| SizedNil => lst2
| SizedCons _ x tl => SizedCons x (concatSized tl lst2)
end.

Gaëtan Gilbert (Aug 15 2021 at 21:52):

if you use 1 + n instead of n + 1 in the type of SizedCons it works better (see https://github.com/coq/coq/blob/master/theories/Vectors/VectorDef.v)

vlj (Aug 15 2021 at 22:01):

Thanks ! It works.

vlj (Aug 15 2021 at 22:04):

but in general, is there a way to do "rewrite on the fly" ?

Gaëtan Gilbert (Aug 16 2021 at 08:35):

yes
for instance

Axiom foo : forall n n2, n + n2 + 1 = n + 1 + n2.
Import EqNotations.

Fixpoint concatSized {A:Type} {n1 n2: nat} (lst1: @SizedList A n1) (lst2: SizedList n2)
  : SizedList (n1 + n2)  :=
match lst1 in SizedList n3
return SizedList (n3 + n2)
with
| SizedNil => lst2
| @SizedCons _ n x tl => rew [SizedList] foo _ _ in SizedCons x (concatSized tl lst2)
end.

(rew is just a notation for eq_rect)
(the type A needs to be explicitly used somewhere otherwise you will get a strange error)
of course you can replace the axiom foo by any well-typed proof term

vlj (Aug 16 2021 at 09:03):

thank you for rew! didn't know it

Last updated: Apr 19 2024 at 13:02 UTC