Library deBruijn_Isomorphism

Set Implicit Arguments.

Require Export Variable_Sets.
Require Export deBruijn_Meta_Env.

This file provides a connection between the generic level and many concrete type systems based on some isomorphisms.

A concrete type system TT is isomorphic to the type representation RR when there is an isomorphism between TT and Interpret RR.

Open Scope type_scope.

The following section collects all the functions and predicates which can be defined and handled generically. The section can be extended when new concept is created generically.

Isomorphisms between a representation and a concrete types/terms.

Definition Iso (A B : Type) := (A -> B) * (B -> A).

Function injectivity

Definition fun_inj (A B:Type)(f:A -> B) := forall (x y: A), f x = f y -> x = y.

Infrastructure for Isomorphisms

Given a type TT and a representation type RR,

  • From : TT -> Interpret RR, an one-to-one function
  • To : Interpret RR -> TT, an one-to-one functioen when restricted to Image of From
  • To (From x) = x, hence
  • From (To (From x)) = From x

Module Type Iso_partial.

  Parameter TT : Type.

  Parameter RR : Rep.

  Parameter From : TT -> Interpret RR.

  Parameter From_inj : fun_inj From.

  Parameter To : Interpret RR -> TT.

  Parameter To_From : forall (T:TT), To (From T) = T.

  Definition ISO : Iso TT (Interpret RR) := (From, To).

  Hint Rewrite To_From : isorew.

  Hint Resolve To_From.

End Iso_partial.

If there are variables, then From and To build a real isomorphism between TT and Interpret RR.

  • From and To are one-to-one and onto.
  • To (From} x) = x.

Module Type Iso_full.

  Include Type Iso_partial.

  Parameter From_To : forall (T:Interpret RR), From (To T) = T.

  Parameter To_inj : fun_inj To.

  Hint Rewrite From_To : isorew.

  Hint Resolve From_To.

End Iso_full.

Isomorphism for nat will be the basic for other isomorphisms.

Module Iso_nat.

  Definition TT := nat.

  Definition RR :=
  Fixpoint From (T: TT) : Interpret RR :=
    match T with
      | O => Term (InL _ Unit)
      | S n => Term (InR _ (Rec (From n)))

The following definition using a garbage for never-appearing cases is simpler than other, more accurate variations.

  Fixpoint To_ (T : InterpretRep RR RR) : TT :=
    match T return _ with
      | InL _ _ Unit => 0
      | InR _ _ (Rec U) => S (To U)
      | _ => 0

  with To (T:Interpret RR) : TT :=
    match T with
      | Var _ => 0
      | Term U => To_ U

  Lemma To_From : forall (T:TT), To (From T) = T.
    intro T; induction T; simpl; f_equal; auto.

End Iso_nat.

For automation

Lemma Iso_nat_REC : Iso_nat.RR <> REC.
  unfold Iso_nat.RR; congruence.

Hint Resolve Iso_nat_REC.
Hint Resolve Iso_nat.To_From.

Hint Rewrite Iso_nat.To_From : iso_module.

specialized tactics for the proof of From_To.

Ltac from_to_Rep T H :=
  dependent destruction T;
  destruct T;
  try discriminate;
  repeat (
  match goal with
    | [H : InterpretRep _ _ |- _] => destruct H; try discriminate
  match goal with
    | H : PLUS _ _ = _ |- _ => inversion H; subst
  try (
  match goal with
    | q : QQ |- _ => destruct q
  match goal with
    | H : JMeq _ _ |- _ => rewrite <- (JMeq_eq H); simpl
  try repeat rewrite H; auto;
  try autorewrite with iso_module; auto.

Ltac from_to T H:=
  let v := fresh "v" in
  destruct T as [v | ]; simpl;
  [destruct v | idtac]; auto using H.