The Coq mailing list

[Kirill Taran <kirill.t256 AT gmail.com>]

Hmm, previous question could be solved with providing equation, but for me it was mainly about normalization. > you can use this "convey" technique to hack the equality in, and generate it using eq_refl
Ye, seems that it is possible; but require some more manual code.

Ok, I am going to read CPDT as soon as possible :)

Sincerely,
Kirill Taran

On Fri, Feb 14, 2014 at 7:42 PM, Kristopher Micinski <krismicinski AT gmail.com> wrote:

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