The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Notation get' n x := $(let ret := constr:(_ : get n x) in let ret' := (eval hnf in ret) in exact ret')$.

(your body works too).

On Sat, Jan 17, 2015 at 10:48 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 01/17/2015 12:03 AM, Jason Gross wrote:

Here's some code for flattened-[get] on right-associated tuples:

Class get {A B} (n : nat) (from : A) := to : B.
Instance get0 {A0} {x : A0} : @get _ _ 0 x | 2 := x.
Instance get1 {A0 A1} {x : A0 * A1} : @get _ _ 1 x | 2 := snd x.
Instance getL {A0 A1 B} {x : A0} {y : A1} {n} {res : get (B := B) n x} :
get n (x, y) | 0 := res.
Instance getR {A0 A1 B} {x : A0} {y : A1} {n} {res : get (B := B) n y} :
get (S n) (x, y) | 1 := res.

Goal True.
   let v := fresh in
   pose (_ : get 0 (1, (2, 3))) as v;
     hnf in v.
   let v := fresh in
   pose (_ : get 1 (1, (2, 3))) as v;
     hnf in v.
   let v := fresh in
   pose (_ : get 2 (1, (2, 3))) as v;
     hnf in v.

If you want it on left-associated tuples, you'll need to either write a
reassociator, or need to add a class for computing the length of a tuple,
and replace [get (S n) (x, y)] with [get (length x + n) (x, y)] in the last
case (or something similar; you may need some [Hint Extern (...) => .... :
typeclass_instances] to get more reduction).

-Jason

Thanks, Jason!  That is a really nice solution.  However, is there a way to define a function that packages the get/hnf functionality? This doesn't work:

  Definition get' (n:nat){T}(x : T) :=
    $(pose (_ : get n x) as v; hnf in v; exact v)$.

-- Jonathan