Module AdmissibleSubtyping

Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Types.
Require Import TypeEquality.
Require Import Coercions.
Require Import Subtyping.
Require Import Environments.
Require Import DerivedSubtyping.
Require Import TypeSubstitution.

Admissible subtyping rules.

Amadio and Cardelli's subtyping rule is admissible.

Definition CoMuAmadioCardelli c :=
  CoMu (CoTyEq c).

Lemma JCoMuAmadioCardelli:
  forall C c T U,
  jco (C!!;; TyVar 0 --> TyVar 1) c (lift_ty 1 T --> lift_ty 0 U) ->
  wf (TyMu T) ->
  wf (TyMu U) ->
  jco C (CoMuAmadioCardelli c) (TyMu T --> TyMu U).

Proof.

  introv h wf0 wf1.
  constructor; eauto.
  eapply JCoTyEq; eauto using tyeq_fold.
  unfold unfold.

We will now replace the type variable 0 with the type TyMu T and the type variable 1 with the type TyMu U.

We begin with the first of these substitutions.

  generalize (jco_type_substitution h 0 (wf_lift wf0 0)); simpl; clear h; intro h.
  unfold subst_var, lift_var in h; simpl in h.
  rewrite subst_lift_ty in h.
  rewrite subst_lift_env in h.
  change (TyMu (lift_ty 1 T)) with (lift_ty 0 (TyMu T)) in h.
  rewrite <- lift_subst_2_ty in h; eauto.

We continue with the second of these substitutions.

  generalize (jco_type_substitution h 0 wf1); simpl; clear h; intro h.
  unfold subst_var, lift_var in h; simpl in h.
  repeat rewrite subst_lift_ty in h.
  rewrite subst_lift_env in h.

We are done!

assumption.

Qed.