The Coq mailing list

[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