Library DGP_Core

Set Implicit Arguments.

Require Export Max.
Require Export Equality.
Require Export Eqdep_dec.
Require Export Metatheory_Var.
Require Export Metatheory_Env.

DGP Universe Language


Rep is the universe of the representations of object languages

Inductive Rep : Type :=
| UNIT : Rep
| CONST : Rep -> Rep
| REPR : Rep -> Rep
| PLUS : Rep -> Rep -> Rep
| PROD : Rep -> Rep -> Rep
| BIND : Rep -> Rep -> Rep
| REC : Rep.

The DGP universe is decidable.

Lemma Rep_dec : forall r r0 : Rep, {r = r0} + {r <> r0}.
Proof.
  decide equality.
Defined.

Lemma Rep_dec_or : forall r r0 : Rep, r = r0 \/ r <> r0.
Proof.
  intros; elim (Rep_dec r r0); tauto.
Defined.

Lemma Rep_dec_unicity : forall (r r0 : Rep)(H H0: r =r0), H = H0.
Proof.
  intros; auto using eq_proofs_unicity, Rep_dec_or.
Qed.

case_rep destructs the Rep_dec cases.

Ltac case_rep :=
  match goal with
    | |- context [Rep_dec ?r ?s] => destruct (Rep_dec r s)
    | H: context [Rep_dec ?r ?s] |- _ => destruct (Rep_dec r s)
  end.

noRepr denotes that there are no embedded terms in the representation.
  • Examples: type classes in STLC or System F, or the term class in STLC.

Fixpoint noRepr (r:Rep) : Prop :=
  match r with
    | UNIT => True
    | CONST _ => True
    | REPR _ => False
    | PLUS r0 r1 => noRepr r0 /\ noRepr r1
    | PROD r0 r1 => noRepr r0 /\ noRepr r1
    | BIND r0 r1 => if Rep_dec r0 REC then noRepr r1 else False
    | REC => True
  end.

Interpretation of the DGP universe


The module Dgp explains how to interpret the Dgp universe.
  • Dgp is parametrized with two sets of variables.
  • VSet stands for the class of variables.
  • QSet stands for the class of variables to be bound.
  • The basic requirement for VSet and QSet is decidability.

Module Dgp (VSet : GenericVarSig)(QSet: QuantificationVarSig).

VV denotes for the class of variables which will be used as concrete term/type variables.
  • Locally nameless: VV = nat + nat
  • de Bruijn stle : VV = nat
  • Locally named: VV = nat + nat
  • Nominal approach : VV = nat

  Definition VV := VSet.t.

QQ denotes the class of variables intended for the abstraction variables.
  • Locally nameless: QQ = unit type
  • de Bruijn stle : QQ = unit type
  • Locally named: QQ = nat
  • Nominal approach : QQ = nat

  Definition QQ := QSet.t.

Interpretation of representations using inductive families.

  Inductive InterpretRep (r : Rep) : Rep -> Type :=
  | Unit : InterpretRep r UNIT
  | Const : forall (s : Rep), Interpret s -> InterpretRep r (CONST s)
  | Repr : forall (s : Rep), Interpret s -> InterpretRep r (REPR s)
  | InL : forall s s0, InterpretRep r s -> InterpretRep r (PLUS s s0)
  | InR : forall s s0, InterpretRep r s0-> InterpretRep r (PLUS s s0)
  | Pair : forall s s0, InterpretRep r s -> InterpretRep r s0 -> InterpretRep r (PROD s s0)
  | Bind : forall r0 s, QQ -> InterpretRep r s -> InterpretRep r (BIND r0 s)
  | Rec : Interpret r -> InterpretRep r REC

  with Interpret (r : Rep) : Type :=
  | Var : VV -> Interpret r
  | Term : InterpretRep r r -> Interpret r.

  Hint Constructors InterpretRep Interpret.

  Implicit Arguments Unit [r].

Generic functions independent of the first-order representation styles:
  • Complexivity of a term which measures the depth of the term structure.

  Fixpoint sizeRep (r s : Rep)(T : InterpretRep r s){struct T} : nat :=
    match T with
      | Unit => 0
      | Const _ _ => 0
      | Repr _ T0 => size T0
      | InL _ _ T0 => sizeRep T0
      | InR _ _ T0 => sizeRep T0
      | Pair _ _ T0 T1 => S (max (sizeRep T0) (sizeRep T1))
      | Bind _ _ _ T0 => S (sizeRep T0)
      | Rec T0 => size T0
    end

  with size (r : Rep)(T : Interpret r){struct T} : nat :=
    match T with
      | Var _ => 0
      | Term T0 => sizeRep T0
    end.

conv is an automorphism.
  • conv is sometimes necessary to enable Coq's type checking.
  • conv is used to define heterogeneous substitutions using dependent types.

  Definition conv r r0 (e: r = r0) (T:Interpret r0) : Interpret r.
  Proof.
    intros r r0 e T; rewrite e; exact T.
  Defined.

  Lemma conv_indep r r0 (e e0: r = r0) (T:Interpret r0) : conv e T = conv e0 T.
  Proof.
    intros r r0 e; case e; clear e; intro e0.
    rewrite (Rep_dec_unicity e0 refl); auto.
  Qed.

  Lemma conv_id : forall (r : Rep)(e:r = r)(T:Interpret r), conv e T = T.
  Proof.
    intros r e T.
    rewrite (Rep_dec_unicity e(refl_equal r)); reflexivity.
  Qed.

  Hint Rewrite conv_id : isorew.

  Lemma conv_Var : forall r r0 (e:r = r0) x, Var r x = conv e (Var r0 x).
  Proof.
    intros r r0 e; case e; unfold conv; reflexivity.
  Qed.

  Lemma conv_size : forall r r0 (e:r = r0)(T:Interpret r0), size T = size (conv e T).
  Proof.
    intros r r0 e; case e; unfold conv; reflexivity.
  Qed.

End Dgp.