The Coq mailing list

[Saulo Araujo <saulo2 AT gmail.com>]

Thanks for your explanation Cedric! 

I was searching about the convoy pattern and I found a nice presentation about it: https://yow.eventer.com/yow-lambda-jam-2015-

1305/pattern-matching-dependent-types-in-coq-by-matthew-brecknell-1881 Maybe it will be useful to other newcomers to dependent types in Coq. Coincidentally, similarly to what I did, the presenter extracted the arguments with which a value was constructed to tuples. However, rather than using letting expressions, the presenter did a match in the tuples. By doing that, his code felt, at least syntactically, more familiar than mine.

Sincerely,

Saulo

On Wed, Feb 10, 2016 at 12:32 PM, Cedric Auger <sedrikov AT gmail.com> wrote:

I have no instance of Coq running, but as I could tell, when you do:

fun s (ds : List Digit (S n')) =>

  match s with

  | SequenceNode n1 s0 s1 => …

Then in the context of '…', ds has type "List Digit (S n')", as it has been introduced in the context BEFORE destructuration of s.

Thus it has kept its type, whereas s0 and s1 have type "Sequence E n1". Thus in this way, you lost the link between "n'" and "n1".

To avoid that, you should be able to do something like:

fun s =>

  match s with

  | SequenceNode n1 s0 s1 => fun (ds : List Digit (S n1)) => …

Thus putting the introduction of "ds" under destructructuration of s.

(That is in term of dependant anotations, have something like "match s in Sequence _ sn return List Digit n -> … with … end")

Note that using fixpoints for these types would have let to

Inductive OSequence : Type := …
Inductive SSequence (T : Type) := SequenceNode : T -> T -> SSequence T.
Fixpoint Sequence (n : nat) : Type :=

  match n with

  | O => OSequence

  | S n => SSequence (Sequence n)

  end.

…

fun (s : Sequence E (S n')) (ds : List Digit (S n')) =>

  match s with

  | SequenceNode s0 s1 => (* note that there would be no 'n1' parameter anymore, thus no problem with keeping the link with (S n') *)

    match ds with

    | ListNode d ds' => (* as above, no 'n2' parameter here *)

      match d with

      | D0 => get s0 ds' (* Coq would not complain here *)

which indeed is convertible (by reducing the types, like what the "simpl" tactic does) to

fun (s : SSequence E n') (ds : SList Digit n') =>

  match s with

  | SequenceNode s0 s1 => (* note that there would be no 'n1' parameter anymore, thus no problem with keeping the link with (S n') *)

    match ds with

    | ListNode d ds' => (* as above, no 'n2' parameter here *)

      match d with

      | D0 => get s0 ds' (* Coq would not complain here *)

2016-02-10 15:43 GMT+01:00 Saulo Araujo <saulo2 AT gmail.com>:

HI Cedric,

Thanks for your suggestion! I believe this technique is described in the section "Recursive Type Definitions" of http://adam.chlipala.net/cpdt/html/Cpdt.DataStruct.html I am surely gonna try it.

So far, working with dependent types has been very tricky, i.e., frustrating :). For example, it is not clear to me why Coq does not accept the definition 

Fixpoint get E n (s: Sequence E n) (ds: List Digit n): E :=

  match n as n0 return Sequence E n0 -> List Digit n0 -> E with

  | 0 =>

      fun (s: Sequence E 0) (ds: List Digit 0) =>

        match s, ds with

        | SequenceLeaf e0 e1, ListLeaf D0 => e0

        | SequenceLeaf e0 e1, ListLeaf D1 => e1

        end

  | S n' =>

      fun (s: Sequence E (S n')) (ds: List Digit (S n')) =>

          match s with

          | SequenceNode n1 s0 s1 => 

              match ds with

              | ListNode n2 d ds' => 

                  match d with

                  | D0 => get s0 ds' (* Coq complains here, saying that the type of ds' is not List Digit n1 *)

                  | D1 => get s1 ds'

                  end

              end

          end

  end s ds.

But accepts the definition below, that uses let expressions to store the s0 and s1 extracted from a SequenceLeaf and the d and ds' extracted from a ListLeaf. Looks like that the let _expression_ forces Coq to remove n1 and n2 from the context, substituting them for n'.

Fixpoint get E n (s: Sequence E n) (ds: List Digit n): E :=

  match n as n0 return Sequence E n0 -> List Digit n0 -> E with

  | 0 =>

      fun (s: Sequence E 0) (ds: List Digit 0) =>

        match s, ds with

        | SequenceLeaf e0 e1, ListLeaf D0 => e0

        | SequenceLeaf e0 e1, ListLeaf D1 => e1

        end

  | S n' =>

      fun (s: Sequence E (S n')) (ds: List Digit (S n')) =>

        let (s0, s1) :=

          match s with

          | SequenceNode n1 s0 s1 => (s0, s1)

          end

        in let (d, ds') :=

          match ds with

          | ListNode n2 d ds' => (d, ds')

          end

        in

          match d with

          | D0 => get s0 ds'

          | D1 => get s1 ds'

          end

  end s ds.

Sincerely,

Saulo

On Wed, Feb 10, 2016 at 11:00 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

Oh, and by the way, I find it often simpler to define types with fixpoints rather than inductives with dependant indices.

For instance, your List : nat -> Type could have been written:

Inductive olist : Type := Nil.

Record slist(t : Type) : Type := { head : E ; tail : t}.

Fixpoint List (n : nat) : Type :=

  match n with

  | O => olist (* alt. you can use "unit" which is already defined *)

  | S n => slist (List n) (* alt. you can user E*(List n) *)

  end.

This way, you don’t have to do tricky things with inversion.

2016-02-07 11:53 GMT+01:00 Saulo Araujo <saulo2 AT gmail.com>:

James and Guillaume,

Thanks a lot for your help!

Saulo

On Sun, Feb 7, 2016 at 4:26 AM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

On 07/02/2016 04:22, Saulo Araujo wrote:

> Looks like refine is discarding some information that the command
>
> *inversion t as [e0 e1 | x t0 t1].*

The refine tactic is not losing any information. It is just that the
proof term you passed to it is closer from destruct than from inversion.
And since you cannot finish this proof by starting with destruct, you
cannot expect to finish it by starting with (refine match) either.

The inversion tactic works by generalizing some equalities before doing
an actual destruct. Here you want to remember what n has become once you
have destructed (t : Sequence E n), so your proof term should start with

refine (match t in Sequence _ n' return n = n' -> _ with
  | SequenceLeaf e0 e1 => _
  | SequenceNode x s0 s1 => _
  end eq_refl).

Notice the eq_refl at the end (the equality), and the "in Sequence _ n'
return n = n' ->" at the start (and its generzalization).

Best regards,

Guillaume