The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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

On Fri, Jan 16, 2015 at 10:10 PM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 01/15/2015 07:02 PM, Vilhelm Sjöberg wrote:

On 2015-01-15 18:33, Jonathan Leivent wrote:

That does look familiar.  However, how to get 'get' to infer the ts arg from the tuple?  As this doesn't work:

  get _ 2 (1, (true, (42, tt))).

One way is to use typeclasses to infer this. The below code is inspired by the Data.Typeable class in Haskell; I'm not sure if there already is some existing similar framework in Coq.

   Class Typeable (T : Set) := {
     getCode : list Set;
     getCode_spec : T = tupleType getCode
   }.

   Instance TypableUnit : Typeable unit :=
     Build_Typeable unit nil eq_refl.

   Instance TypeablePair (a b : Set) (c : Typeable b) : Typeable (a*b).
      apply (Build_Typeable (a*b) (a::getCode)).
      simpl. rewrite <- getCode_spec.
      reflexivity.
   Defined.

   Definition cast {a b : Set} (p: a=b) (x: a) : b :=
      match p in _=b return b with eq_refl => x end.

   Definition get' {a:Set} {c: Typeable a} (i:nat) (v : a)  :=
      get getCode i (cast getCode_spec v).

   Eval compute in
      get' 2 (1,(true,(42,tt))).  (* = 42 *)

Vilhelm

This reminds me that I really need to learn me some typeclasses :-[

Can this be simplified by using a typeclass to overload get on pairs vs. every other type - and by doing so, ditch the tupleType completely?

-- Jonathan