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: Saulo Araujo <saulo2 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Doubt about refine
  • Date: Wed, 10 Feb 2016 11:43:29 -0300
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=saulo2 AT gmail.com; spf=Pass smtp.mailfrom=saulo2 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qg0-f54.google.com
  • Ironport-phdr: 9a23:2YlHWRYWM9RtO98l/sQ/9cP/LSx+4OfEezUN459isYplN5qZpc+4bnLW6fgltlLVR4KTs6sC0LqJ9fu6EjJdqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0oMeYPVgArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JaWwLlh0AKhLM8RP9FsPquzb+sbBV1yyTPMmwRrcxD2fxp5x3QQPl3X9UfwUy93va35R9

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






Archive powered by MHonArc 2.6.18.

Top of Page