Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Doubt about refine

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Doubt about refine


Chronological Thread 
  • From: Cedric Auger <sedrikov AT gmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Doubt about refine
  • Date: Wed, 10 Feb 2016 15:00:12 +0100
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=sedrikov AT gmail.com; spf=Pass smtp.mailfrom=sedrikov AT gmail.com; spf=None smtp.helo=postmaster AT mail-io0-f182.google.com
  • Ironport-phdr: 9a23:R/sB+RwNnVXlEAXXCy+O+j09IxM/srCxBDY+r6Qd0e8QIJqq85mqBkHD//Il1AaPBtWErakewLeL+4nbGkU+or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6anHS+4HYoFwnlMkItf6KuStGU1J78ir360qaQSjsLrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGwD884mooRLVry/dKAlR5RZCi4nOiY7/oej4RLEVE6E4mYWemQQiBtBRQbfukLURJD05wD3uvB802GzIML7V/hgQjmu9aZoTwHAhyIONjp/+2bS3J8jxJlHqQ6s8kQsi7XfZ5uYYaJz

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





Archive powered by MHonArc 2.6.18.

Top of Page