Library DGP_Core
Set Implicit Arguments.
Require Export Max.
Require Export Equality.
Require Export Eqdep_dec.
Require Export Metatheory_Var.
Require Export Metatheory_Env.
Require Export Max.
Require Export Equality.
Require Export Eqdep_dec.
Require Export Metatheory_Var.
Require Export Metatheory_Env.
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.
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.
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
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
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.