The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Part II of CPDT <http://adam.chlipala.net/cpdt/> is broadly about how to work with dependently typed definitions like yours.  I think it would be a disservice to reply to your question with a customized answer, which would be quite long and would include lots of general background that is already in CPDT (and maybe other sources, too).

On 02/14/2014 10:35 AM, Kirill Taran wrote:

Also, as I understand there is approach with Program and Obligations,
but first of all I am interested with "clean" method.

Sincerely,
Kirill Taran

On Fri, Feb 14, 2014 at 7:21 PM, 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