Library LNameless_Fsub_Iso

Set Implicit Arguments.

Require Export LNameless_Isomorphism.

Fsub Part 1A and 2A


Reference: Chargueraud's POPL solution using Locally Nameless style and cofinite quantification

Language Syntax for System F with subtyping


Notation var := atom.

Inductive typ : Set :=
| typ_bvar : nat -> typ
| typ_fvar : var -> typ
| typ_top : typ
| typ_arrow : typ -> typ -> typ
| typ_all : typ -> typ -> typ.

Inductive trm : Set :=
| trm_bvar : nat -> trm
| trm_fvar : var -> trm
| trm_app : trm -> trm -> trm
| trm_abs : typ -> trm -> trm
| trm_tapp : trm -> typ -> trm
| trm_tabs : typ -> trm -> trm.

Isomorphism modules

Module Iso_typ <: Iso_full.

  Definition TT := typ.

  Hint Unfold TT.

For the generic representation of typ, typ_all case needs special care:

  • PROD should come before BIND.
  • Otherwise, the definition of substitution would be impossible.

  Definition RR :=
    PLUS
    UNIT
    (PLUS
      (PROD REC REC)
      (PROD REC (BIND REC REC))).
  Fixpoint From (T : TT) : Interpret RR :=
    match T with
      | typ_bvar j => Var _ (inr j)
      | typ_fvar n => Var _ (inl n)
      | typ_top => Term (InL _ Unit)
      | typ_arrow T0 T1 => Term (InR _ (InL _ (Pair (Rec (From T0)) (Rec (From T1)))))
      | typ_all T0 T1 => Term (InR _ (InR _ (Pair (Rec (From T0)) (Bind REC tt (Rec (From T1))))))
    end.

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

  Fixpoint To_ (T : InterpretRep RR RR) : typ :=
    match T return _ with
      | InL _ _ Unit =>
        typ_top
      | InR _ _ (InL _ _ (Pair _ _ (Rec T0) (Rec T1))) =>
        typ_arrow (To T0) (To T1)
      | InR _ _ (InR _ _ (Pair _ _ (Rec T0) (Bind REC _ tt (Rec T1)))) =>
        typ_all (To T0) (To T1)
      | _ =>
        typ_fvar 0
    end

  with To (T : Interpret RR) : typ :=
    match T with
      | Var (inl k) => typ_fvar k
      | Var (inr j) => typ_bvar j
      | Term T0 => To_ T0
    end.

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

  Lemma From_inj : forall T U : TT, From T = From U -> T = U.
  Proof.
    intros T U H.
    rewrite <- (To_From T), <- (To_From U).
    rewrite H; auto.
  Qed.

  Lemma From_To_Rep : forall (T : InterpretRep RR RR), From (To_ T) = Term T
    
    with From_To : forall (T : Interpret RR), From (To T) = T.
  Proof.
    from_to_Rep T From_To.

    from_to T From_To_Rep.
  Qed.

  Lemma To_inj : forall (T U:Interpret RR), To T = To U -> T = U.
  Proof.
    intros T U H.
    rewrite <- (From_To T), <- (From_To U).
    rewrite H; auto.
  Qed.

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

End Iso_typ.

For automation

Hint Resolve Iso_typ.To_From.
Hint Resolve Iso_typ.From_To.

Hint Rewrite Iso_typ.To_From : iso_module.
Hint Rewrite Iso_typ.From_To : iso_module.

Module Iso_trm <: Iso_full.

  Definition TT := trm.

For the generic representation of trm, trm_abs and trm_tabs cases need special care:

  • PROD should come before BIND.
  • Otherwise, the definition of substitution would be impossible.

  Definition RR :=
    PLUS (PROD REC REC)
    (PLUS (PROD (REPR Iso_typ.RR) (BIND REC REC))
      (PLUS (PROD REC (REPR Iso_typ.RR))
        (PROD (REPR Iso_typ.RR) (BIND Iso_typ.RR REC)))).
  Fixpoint From (T : TT) : Interpret RR :=
    match T return Interpret RR with
      | trm_bvar j => Var _ (inr j)
      | trm_fvar n => Var _ (inl n)
      | trm_app T0 T1 =>
        Term (InL _ (Pair (Rec (From T0)) (Rec (From T1))))
      | trm_abs U T0 =>
        Term (InR _ (InL _ (Pair (Repr _ (Iso_typ.From U)) (Bind REC tt (Rec (From T0))))))
      | trm_tapp T0 U =>
        Term (InR _ (InR _ (InL _ (Pair (Rec (From T0)) (Repr _ (Iso_typ.From U))))))
      | trm_tabs U T0 =>
        Term (InR _ (InR _ (InR _ (Pair (Repr _ (Iso_typ.From U)) (Bind Iso_typ.RR tt (Rec (From T0)))))))
    end.

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 _ _ (Pair _ _ (Rec U) (Rec V)) =>
        trm_app (To U) (To V)
      | InR _ _ (InL _ _ (Pair _ _ (Repr (PLUS (UNIT) (PLUS (PROD REC REC) (PROD REC (BIND REC REC)))) t) (Bind REC _ _ (Rec U)))) =>
        trm_abs (Iso_typ.To t) (To U)
      | InR _ _ (InR _ _ (InL _ _ (Pair _ _ (Rec U) (Repr (PLUS (UNIT) (PLUS (PROD REC REC) (PROD REC (BIND REC REC)))) t)))) =>
        trm_tapp (To U) (Iso_typ.To t)
      | InR _ _ (InR _ _ (InR _ _ (Pair _ _ (Repr (PLUS (UNIT) (PLUS (PROD REC REC) (PROD REC (BIND REC REC)))) t) (Bind (PLUS UNIT (PLUS (PROD REC REC) (PROD REC (BIND REC REC)))) _ _ (Rec U))))) =>
        trm_tabs (Iso_typ.To t) (To U)
      | _ => trm_fvar 0
    end
  with To (T : Interpret RR) : TT :=
    match T return trm with
      | Var (inl k) => trm_fvar k
      | Var (inr l) => trm_bvar l
      | Term U => To_ U
    end.

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

  Lemma From_inj : forall T U : TT, From T = From U -> T = U.
  Proof.
    intros T U H.
    rewrite <- (To_From T), <- (To_From U).
    rewrite H; auto.
  Qed.

  Lemma From_To_Rep : forall (T : InterpretRep RR RR), From (To_ T) = Term T
    
    with From_To : forall (T : Interpret RR), From (To T) = T.
  Proof.
    from_to_Rep T From_To.
    from_to T From_To_Rep.
  Qed.

  Lemma To_inj : forall (T U:Interpret RR), To T = To U -> T = U.
  Proof.
    intros T U H.
    rewrite <- (From_To T), <- (From_To U).
    rewrite H; auto.
  Qed.

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

End Iso_trm.

Making implicit arguments

Implicit Arguments Iso_typ.From_inj [T U].

Implicit Arguments Iso_trm.From_inj [T U].
Implicit Arguments Iso_trm.To_inj [T U].

For noRepr cases

Lemma typ_noRepr : noRepr Iso_typ.RR.
Proof.
  firstorder.
Qed.

Lemma trm_typ : Iso_trm.RR <> Iso_typ.RR.
Proof.
red; intro Heq; discriminate.
Qed.

Lemma Iso_typ_REC : Iso_typ.RR <> REC.
Proof.
  unfold Iso_typ.RR; congruence.
Qed.

Hint Resolve typ_noRepr trm_typ Iso_typ_REC.