## 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: Jun 23 2024 at 23:01 UTC