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.
```

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)

Thanks ! It works.

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

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

thank you for rew! didn't know it

Last updated: Oct 03 2023 at 19:01 UTC