The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Just to point out, this is very similar to a previous question you've
asked.  To add to Adam's answer, you can use this "convey" technique
to hack the equality in, and generate it using eq_refl.

Kris


On Fri, Feb 14, 2014 at 10:21 AM, Kirill Taran 
<kirill.t256 AT gmail.com>
 wrote:
> Hello,
>
> I am trying to implement module type for queue.
> I have such code:
>
> Module Type Queue.
>   Parameter queue : nat -> Type -> Type.
>   Parameter pop   : forall {n : nat} {X : Type}, queue (S n) X -> X * queue
> n X.
>   Parameter push  : forall {n : nat} {X : Type}, X -> queue n X -> queue (S
> n) X.
>
>   Fixpoint concat {nl nr} {X} : queue nl X -> queue nr X -> queue (nl + nr)
> X :=
>     match nl as nl' return queue nl' X -> queue nr X -> queue (nl' + nr) X
> with
>     | S nl' => fun ql qr => match pop ql with (m,ql') => concat ql' (push m
> qr) end
>     | O     => fun _  qr => qr
>     end.
>
> But it can't pass type checking:
>
> The term "concat nl' (S nr) X ql' (push m qr)" has type
>  "queue (nl' + S nr) X" while it is expected to have type
>  "queue (S nl' + nr) X".
>
> So I want somehow tell type checker that S x + y = x + S y, but how to do
> it?
>
> P.S. Also solutions with signature with such signature are welcome:
> concat {nl nr} {X} (ql : queue nl X) (qr : queue nr X) : queue (nl + nr) X
>
> Sincerely,
> Kirill Taran