The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

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