Module TypeEquality

Set Implicit Arguments.
Require Import MyTactics.
Require Import DeBruijn.
Require Import Layers.
Require Import Types.
Require Import MyLPO.
Require Import List.

In order to define type equality, it seems necessary, or at least convenient, to rule out so-called ill-formed types. A type is ill-formed if it contains a non-contractive recursive type. A recursive type is non-contractive if the cycle goes through non-contractive type constructors only. For our purposes, there are basically just two non-contractive type constructors, namely TyMu itself, and TyTensor, in its left-hand side. Forbidding a cycle that goes through TyMu and through the left-hand side of TyTensor only sounds reasonable -- indeed, if such a type were allowed, it would be impossible to simplify it, using the equational theory, so as to cause some structure other than TyMu and TyTensor to appear at the root. To summarize this discussion, the following table tells which type constructors are contractive in which arguments: TyArrow contractive, contractive TyPair contractive, contractive TyQ contractive TyMu NOT CONTRACTIVE TyBang contractive TyRef contractive TyAt N/A TyRegionCap N/A, contractive TyRegionCapPunched N/A, contractive, N/A TyTensor NOT CONTRACTIVE, contractive The abbreviation "N/A" means that the point is moot because the argument is intended to be a region. In that case, we formally define the argument as contractive, (because this makes more types well-formed,) but this choice has no deep impact; one could just as well define it as non-contractive.

The issue of contractiveness crops up again in the definition of recursive coercions, where it is more subtle; see Coercions.

-------------------------------------------------------------------------

Equality over types is defined in terms of structural equality plus certain reduction rules.

We have reduction rules for recursive types -- they unfold -- and for tensors -- if their argument exhibits enough structure, they reduce.

-------------------------------------------------------------------------

We sometimes use the empty reduction relation over types.

Inductive frozen : ty -> ty -> Prop := .

-------------------------------------------------------------------------

Unfolding the body of a recursive type forms a notion of reduction.

We are interested in allowing this reduction sometimes only at the root, and sometimes also in the left-hand side of a tensor. This gives rise to two reduction relations, tyredmu and tyredmuc.

Definition unfold T :=
  subst_ty (TyMu T) 0 T.

Inductive tyredmu : ty -> ty -> Prop :=
| TyRedMu:
    forall T,
    tyredmu (TyMu T) (unfold T).

Inductive tyredmuc : ty -> ty -> Prop :=
| TyRedMuCInject:
    forall T1 T2,
    tyredmu T1 T2 ->
    tyredmuc T1 T2
| TyRedMuCContext:
    forall T1 T2 U,
    tyredmuc T1 T2 ->
    tyredmuc (TyTensor T1 U) (TyTensor T2 U).

Hint Constructors tyredmu tyredmuc.

-------------------------------------------------------------------------

Simplifying tensors forms another notion of reduction.

One could wish to isolate this as a separate reduction relation. However, because reduction is permitted under a context (viz., under the left-hand side of a tensor), one would then have to parameterize this relation over the reduction relation that is permitted under a context. Several fixed points (reduction of tensors alone, or reduction of tensors and recursive types together) would be defined a posteriori. In principle, this could work, but it is heavy and I have trouble getting Coq to produce the right induction schemes, so I abandon this idea.

As a result, I define only the relation that allows reduction of tensors and reduction of recursive types.

Inductive tyred : ty -> ty -> Prop :=
| TyRedTensorArrow:
    forall T1 T2 U,
    tyred (TyTensor (TyArrow T1 T2) U) (TyArrow (TyCompos T1 U) (TyCompos T2 U))
| TyRedTensorPair:
    forall layer1 layer2 T1 T2 U,
    tyred (TyTensor (TyPair layer1 layer2 T1 T2) U) (TyPair layer1 layer2 (TyTensor T1 U) (TyTensor T2 U))
| TyRedTensorUnit:
    forall layer U,
    tyred (TyTensor (TyUnit layer) U) (TyUnit layer)
| TyRedTensorQ:
    forall q T U,
    tyred (TyTensor (TyQ q T) U) (TyQ q (TyTensor T (lift_ty 0 U)))
| TyRedTensorBang:
    forall T U,
    tyred (TyTensor (TyBang T) U) (TyBang (TyTensor T U))
| TyRedTensorRef:
    forall T U,
    tyred (TyTensor (TyRef T) U) (TyRef (TyTensor T U))
| TyRedTensorAt:
    forall T U,
    tyred (TyTensor (TyAt T) U) (TyAt T)
| TyRedTensorRegionCap:
    forall rk sigma T U,
    tyred (TyTensor (TyRegionCap rk sigma T) U) (TyRegionCap rk sigma (TyTensor T U))
| TyRedTensorRegionCapPunched:
    forall rho sigma T U,
    tyred (TyTensor (TyRegionCapPunched rho T sigma) U) (TyRegionCapPunched rho (TyTensor T U) sigma)
| TyRedTensorContext:
    forall T1 T2 U,
    tyred T1 T2 ->
    tyred (TyTensor T1 U) (TyTensor T2 U)
| TyRedMuInject:
    forall T1 T2,
    tyredmu T1 T2 ->
    tyred T1 T2
.

Hint Constructors tyred.

-------------------------------------------------------------------------

Basic inversion tactics.

Ltac frozen :=
  match goal with h: frozen _ _ |- _ => inversion h end.

Ltac tyredmu :=
  match goal with h: tyredmu _ _ |- _ => inversion h; subst; clear h end.

Ltac tyredmuc :=
  match goal with h: tyredmuc _ _ |- _ => inversion h; subst; clear h end.

Ltac tyred :=
  match goal with h: tyred _ _ |- _ => inversion h; subst; clear h end.

Hint Extern 1 => tyred : tyred.

Hint Extern 1 => tyredmu : tyred.

-------------------------------------------------------------------------

Approximate equality of syntactic types is equality of their unfoldings down to a certain depth. The depth increases only at contractive type constructors. This equality is parameterized over the reductions that are permitted in the left- and right-hand types.

Inductive tyapproxeqrr (tyredl tyredr : ty -> ty -> Prop) : nat -> ty -> ty -> Prop :=
| TyApproxEqZero:
    forall T U,
    tyapproxeqrr tyredl tyredr 0 T U
| TyApproxEqVar:
    forall k x,
    tyapproxeqrr tyredl tyredr k (TyVar x) (TyVar x)
| TyApproxEqArrow:
    forall k T1 T2 U1 U2,
    tyapproxeqrr tyredl tyredr k T1 U1 ->
    tyapproxeqrr tyredl tyredr k T2 U2 ->
    tyapproxeqrr tyredl tyredr (S k) (TyArrow T1 T2) (TyArrow U1 U2)
| TyApproxEqPair:
    forall k layer1 layer2 T1 T2 U1 U2,
    tyapproxeqrr tyredl tyredr k T1 U1 ->
    tyapproxeqrr tyredl tyredr k T2 U2 ->
    tyapproxeqrr tyredl tyredr (S k) (TyPair layer1 layer2 T1 T2) (TyPair layer1 layer2 U1 U2)
| TyApproxEqUnit:
    forall k layer,
    tyapproxeqrr tyredl tyredr k (TyUnit layer) (TyUnit layer)
| TyApproxEqQ:
    forall k q T U,
    tyapproxeqrr tyredl tyredr k T U ->
    tyapproxeqrr tyredl tyredr (S k) (TyQ q T) (TyQ q U)
| TyApproxEqBang:
    forall k T U,
    tyapproxeqrr tyredl tyredr k T U ->
    tyapproxeqrr tyredl tyredr (S k) (TyBang T) (TyBang U)
| TyApproxEqRef:
    forall k T U,
    tyapproxeqrr tyredl tyredr k T U ->
    tyapproxeqrr tyredl tyredr (S k) (TyRef T) (TyRef U)
| TyApproxEqRegion:
    forall k r,
    tyapproxeqrr tyredl tyredr k (TyRegion r) (TyRegion r)
| TyApproxEqAt:
    forall k T U,
    tyapproxeqrr tyredl tyredr k T U ->
    tyapproxeqrr tyredl tyredr (S k) (TyAt T) (TyAt U)
| TyApproxEqRegionCap:
    forall k rk T1 U1 T2 U2,
    tyapproxeqrr tyredl tyredr k T1 U1 ->
    tyapproxeqrr tyredl tyredr k T2 U2 ->
    tyapproxeqrr tyredl tyredr (S k) (TyRegionCap rk T1 T2) (TyRegionCap rk U1 U2)
| TyApproxEqRegionCapPunched:
    forall k T1 U1 T2 U2 T3 U3,
    tyapproxeqrr tyredl tyredr k T1 U1 ->
    tyapproxeqrr tyredl tyredr k T2 U2 ->
    tyapproxeqrr tyredl tyredr k T3 U3 ->
    tyapproxeqrr tyredl tyredr (S k) (TyRegionCapPunched T1 T2 T3) (TyRegionCapPunched U1 U2 U3)
| TyApproxEqTensor:
    forall k T1 U1 T2 U2,
    tyapproxeqrr tyredl tyredr (S k) T1 U1 ->
    tyapproxeqrr tyredl tyredr k T2 U2 ->
    tyapproxeqrr tyredl tyredr (S k) (TyTensor T1 T2) (TyTensor U1 U2)
| TyApproxEqRedLeft:
    forall k T1 T2 U,
    tyredl T1 T2 ->
    tyapproxeqrr tyredl tyredr k T2 U ->
    tyapproxeqrr tyredl tyredr k T1 U
| TyApproxEqRedRight:
    forall k T U1 U2,
    tyredr U1 U2 ->
    tyapproxeqrr tyredl tyredr k T U2 ->
    tyapproxeqrr tyredl tyredr k T U1
.

Hint Constructors tyapproxeqrr.

-------------------------------------------------------------------------

The normal notion of equality arises when all reductions are permitted in the left- and right-hand types.

We use a notation rather than a definition, so as to avoid unfolding hell.

Notation tyapproxeq :=
(tyapproxeqrr tyred tyred).

-------------------------------------------------------------------------

Type equality is the limit of approximate type equality.

Definition tyeq (T U : ty) :=
forall k, tyapproxeq k T U.

-------------------------------------------------------------------------

A type is contractive with respect to variable k if k occurs only under contractive type constructors.

Inductive contractive : nat -> ty -> Prop :=
| ContractiveTyVar:
    forall k x,
    k <> x ->
    contractive k (TyVar x)
| ContractiveTyArrow:
    forall k T1 T2,
    contractive k (TyArrow T1 T2)
| ContractiveTyPair:
    forall k layer1 layer2 T1 T2,
    contractive k (TyPair layer1 layer2 T1 T2)
| ContractiveTyUnit:
    forall k layer,
    contractive k (TyUnit layer)
| ContractiveTyQ:
    forall k q T,
    contractive k (TyQ q T)
| ContractiveTyMu:
    forall k T,
    contractive (S k) T ->
    contractive k (TyMu T)
| ContractiveTyBang:
    forall k T,
    contractive k (TyBang T)
| ContractiveTyRef:
    forall k T,
    contractive k (TyRef T)
| ContractiveTyRegion:
    forall k r,
    contractive k (TyRegion r)
| ContractiveTyAt:
    forall k T,
    contractive k (TyAt T)
| ContractiveTyRegionCap:
    forall k rk T1 T2,
    contractive k (TyRegionCap rk T1 T2)
| ContractiveTyRegionCapPunched:
    forall k T1 T2 T3,
    contractive k (TyRegionCapPunched T1 T2 T3)
| ContractiveTyTensor:
    forall k T1 T2,
    contractive k T1 ->
    contractive k (TyTensor T1 T2)
.

-------------------------------------------------------------------------

A type T is well-formed if, within T, the body of every recursive type is contractive with respect to the mu-bound variable.

Inductive wf : ty -> Prop :=
| WfTyVar:
    forall x,
    wf (TyVar x)
| WfTyArrow:
    forall T1 T2,
    wf T1 ->
    wf T2 ->
    wf (TyArrow T1 T2)
| WfTyPair:
    forall layer1 layer2 T1 T2,
    wf T1 ->
    wf T2 ->
    wf (TyPair layer1 layer2 T1 T2)
| WfTyUnit:
    forall layer,
    wf (TyUnit layer)
| WfTyQ:
    forall q T,
    wf T ->
    wf (TyQ q T)
| WfTyMu:
    forall T,
    wf T ->
    contractive 0 T ->
    wf (TyMu T)
| WfTyBang:
    forall T,
    wf T ->
    wf (TyBang T)
| WfTyRef:
    forall T,
    wf T ->
    wf (TyRef T)
| WfTyRegion:
    forall r,
    wf (TyRegion r)
| WfTyAt:
    forall T,
    wf T ->
    wf (TyAt T)
| WfTyRegionCap:
    forall rk T1 T2,
    wf T1 ->
    wf T2 ->
    wf (TyRegionCap rk T1 T2)
| WfTyRegionCapPunched:
    forall T1 T2 T3,
    wf T1 ->
    wf T2 ->
    wf T3 ->
    wf (TyRegionCapPunched T1 T2 T3)
| WfTyTensor:
    forall T1 T2,
    wf T1 ->
    wf T2 ->
    wf (TyTensor T1 T2)
.

Inductive wfs: list ty -> Prop :=
| WfsNil:
    wfs nil
| WfsCons:
    forall T Ts,
    wf T ->
    wfs Ts ->
    wfs (T :: Ts).

Hint Constructors contractive wf wfs.

-------------------------------------------------------------------------

Well-formedness is hereditary.

-------------------------------------------------------------------------

Approximate equality at level 0 is always true, so, when the goal has the form tyapproxeqrr _ _ k T U, it is always possible to substitute S k for k.

Ltac tyapproxeqrr_increment :=
  match goal with
  | |- tyapproxeqrr _ _ (S ?k) _ _ =>
      idtac
  | |- tyapproxeqrr _ _ ?k _ _ =>
      destruct k; [ solve [ econstructor ] | idtac ]
  end.

-------------------------------------------------------------------------

Approximate equality decreases as k increases.

Hint Extern 2 => tyapproxeqrr_increment : tyapproxeqrr_increment.

Lemma tyapproxeqrr_decreases:
  forall tyredl tyredr k T1 T2,
  tyapproxeqrr tyredl tyredr (S k) T1 T2 ->
  tyapproxeqrr tyredl tyredr k T1 T2.

Proof.

introv h. dependent induction h; eauto 6 with tyapproxeqrr_increment.
Qed.

-------------------------------------------------------------------------

Basic properties of contractiveness and well-formedness.

Lemma frozen_lift:
forall T1 T2, frozen T1 T2 -> forall k, frozen (lift_ty k T1) (lift_ty k T2).

Proof.

inversion 1.
Qed.

Lemma frozen_subst:
forall T1 T2, frozen T1 T2 -> forall k U, frozen (subst_ty U k T1) (subst_ty U k T2).

Proof.

inversion 1.
Qed.

Lemma contractive_lift_1:
  forall k1 T,
  contractive k1 T ->
  forall k2,
  k1 >= k2 ->
  contractive (S k1) (lift_ty k2 T).

Proof.

induction 1; intros; simpl; eauto.
constructor. unfold lift_var; by_cases; easy.
Qed.

Lemma contractive_lift_2:
  forall k1 T,
  contractive k1 T ->
  forall k2,
  k1 < k2 ->
  contractive k1 (lift_ty k2 T).

Proof.

induction 1; intros; simpl; eauto.
constructor. unfold lift_var; by_cases; easy.
Qed.

Lemma contractive_lift_3:
forall T k,
contractive k (lift_ty k T).

Proof.

induction T; simpl; intros; eauto.
constructor. unfold lift_var; by_cases; easy.
Qed.

Lemma contractive_subst_1:
  forall T U k1,
  contractive k1 U ->
  contractive (S k1) T ->
  forall k2,
  k1 >= k2 ->
  contractive k1 (subst_ty U k2 T).

Proof.

induction T; simpl; introv hU hT ?; dependent destruction hT; eauto using contractive_lift_1.
unfold subst_var. by_cases; eauto.
Qed.

Lemma contractive_subst_2:
  forall T U k1,
  contractive k1 U ->
  contractive k1 T ->
  forall k2,
  k1 < k2 ->
  contractive k1 (subst_ty U k2 T).

Proof.

induction T; simpl; introv hU hT ?; dependent destruction hT; eauto using contractive_lift_1.
unfold subst_var. by_cases; eauto.
Qed.

Lemma contractive_unfold:
  forall k T,
  contractive (S k) T ->
  contractive k (unfold T).

Proof.

unfold unfold. eauto using contractive_subst_1.
Qed.

Lemma contractive_tyredmu:
  forall k T1,
  contractive k T1 ->
  forall T2,
  tyredmu T1 T2 ->
  contractive k T2.

Proof.

induction 1; inversion 1; eauto using contractive_unfold.
Qed.

Lemma contractive_tyred:
  forall k T1,
  contractive k T1 ->
  forall T2,
  tyred T1 T2 ->
  contractive k T2.

Proof.

induction 1; intros; tyred; try solve [ tyredmu ]; eauto 3 using contractive_tyredmu;
match goal with h: contractive _ _ |- _ => depelim h end; eauto.
Qed.

Lemma wf_lift:
  forall T,
  wf T ->
  forall k,
  wf (lift_ty k T).

Proof.

induction 1; intros; simpl; eauto using contractive_lift_2.
Qed.

Lemma wf_subst:
  forall T,
  wf T ->
  forall k U,
  wf U ->
  wf (subst_ty U k T).

Proof.

induction 1; intros; simpl; eauto using wf_lift, contractive_subst_2, contractive_lift_3.
unfold subst_var; by_cases; easy.
Qed.

Lemma wf_unfold:
  forall T,
  wf (TyMu T) ->
  wf (unfold T).

Proof.

unfold unfold. introv h. apply wf_subst. dependent destruction h; auto. auto.
Qed.

Lemma contractive_lift_inverse:
  forall j T1,
  contractive j T1 ->
  forall k T,
  T1 = lift_ty k T ->
  j < k ->
  contractive j T.

Proof.

induction 1; intros; invert_lift_equality; eauto.

TyVar

unfold lift_var in *. by_cases; eauto.
Qed.

Lemma wf_lift_inverse:
  forall k T,
  wf (lift_ty k T) ->
  wf T.

Proof.

introv h; dependent induction h; invert_lift_equality; eauto using contractive_lift_inverse.
Qed.

Same thing, this time for subst instead of lift.

Lemma contractive_subst_inverse:
  forall j T1,
  contractive j T1 ->
  forall U k T,
  T1 = subst_ty U k T ->
  j < k ->
  contractive j T.

Proof.

induction 1; intros; invert_subst_equality; eauto; invert_subst_var_equality.
Qed.

Lemma wf_subst_inverse:
  forall U k T,
  wf (subst_ty U k T) ->
  wf T.

Proof.

introv h; dependent induction h; invert_subst_equality; eauto using contractive_subst_inverse.
Qed.

Lemma wfs_map:
  forall f,
  (forall T, wf T -> wf (f T)) ->
  forall Ts,
  wfs Ts ->
  wfs (map f Ts).

Proof.

induction 2; simpl; eauto.
Qed.

Lemma wfs_app:
  forall Ts Us,
  wfs Ts ->
  wfs Us ->
  wfs (Ts ++ Us).

Proof.

induction 1; simpl; eauto.
Qed.

Hint Resolve wfs_map wfs_app.

Lemma wfs_append_invert:
  forall Ts Us,
  wfs (Ts ++ Us) ->
  wfs Ts /\ wfs Us.

Proof.

  induction Ts; simpl.
  eauto.
  inversion 1. subst. forwards [ ? ? ]: IHTs. eassumption. eauto.
Qed.

-------------------------------------------------------------------------

Compatibility of unfold, tyred, tyapproxeq, and tyeq with lifting and substitution.

Lemma unfold_lift:
  forall k T,
  lift_ty k (unfold T) =
  unfold (lift_ty (S k) T).

Proof.

unfold unfold. intros. apply lift_subst_2_ty. omega.
Qed.

Lemma unfold_subst:
  forall k T U,
  subst_ty U k (unfold T) =
  unfold (subst_ty (lift_ty 0 U) (S k) T).

Proof.

unfold unfold. intros. rewrite subst_subst_ty. auto. omega.
Qed.

Lemma unfold_subst_mu:
  forall k T U,
  subst_ty (TyMu U) k (unfold T) =
  unfold (subst_ty (TyMu (lift_ty 1 U)) (S k) T).

Proof.

intros. rewrite unfold_subst. reflexivity.
Qed.

Lemma tyredmu_lift:
forall T1 T2, tyredmu T1 T2 -> forall k, tyredmu (lift_ty k T1) (lift_ty k T2).

Proof.

inversion 1; intro. rewrite unfold_lift. econstructor.
Qed.

Lemma tyredmu_subst:
forall T1 T2, tyredmu T1 T2 -> forall k U, tyredmu (subst_ty U k T1) (subst_ty U k T2).

Proof.

inversion 1; intros. rewrite unfold_subst. econstructor.
Qed.

Lemma tyred_lift:
  forall T1 T2,
  tyred T1 T2 ->
  forall k,
  tyred (lift_ty k T1) (lift_ty k T2).

Proof.

induction 1; simpl; intro; eauto using tyredmu_lift.

TyRedTensorQ

rewrite <- lift_lift_ty; eauto.
Qed.

Lemma tyred_subst:
  forall T1 T2,
  tyred T1 T2 ->
  forall k U,
  tyred (subst_ty U k T1) (subst_ty U k T2).

Proof.

induction 1; simpl; intros; eauto using tyredmu_subst.

TyRedTensorQ

rewrite <- lift_subst_1_ty; eauto.
Qed.

Lemma tyapproxeqrr_lift:
  forall (tyredl tyredr : ty -> ty -> Prop),
  (forall T1 T2, tyredl T1 T2 -> forall k, tyredl (lift_ty k T1) (lift_ty k T2)) ->
  (forall T1 T2, tyredr T1 T2 -> forall k, tyredr (lift_ty k T1) (lift_ty k T2)) ->
  forall n T U,
  tyapproxeqrr tyredl tyredr n T U ->
  forall k,
  tyapproxeqrr tyredl tyredr n (lift_ty k T) (lift_ty k U).

Proof.

introv ? ?; induction 1; simpl; intro; eauto.
Qed.

Lemma tyapproxeqrr_subst:
  forall (tyredl tyredr : ty -> ty -> Prop),
  (forall T1 T2, tyredl T1 T2 -> forall k, tyredl (lift_ty k T1) (lift_ty k T2)) ->
  (forall T1 T2, tyredr T1 T2 -> forall k, tyredr (lift_ty k T1) (lift_ty k T2)) ->
  (forall T1 T2, tyredl T1 T2 -> forall k U, tyredl (subst_ty U k T1) (subst_ty U k T2)) ->
  (forall T1 T2, tyredr T1 T2 -> forall k U, tyredr (subst_ty U k T1) (subst_ty U k T2)) ->
  forall n T1 T2,
  tyapproxeqrr tyredl tyredr n T1 T2 ->
  forall k U1 U2,
  tyapproxeqrr tyredl tyredr n U1 U2 ->
  tyapproxeqrr tyredl tyredr n (subst_ty U1 k T1) (subst_ty U2 k T2).

Proof.

introv ? ? ? ?. induction 1; simpl; intros; eauto 8 using tyapproxeqrr_decreases, tyapproxeqrr_lift.
unfold subst_var. by_cases; easy.
Qed.

Hint Resolve wf_lift wf_subst.
Hint Immediate contractive_tyred tyred_lift tyred_subst.

Lemma tyeq_lift:
  forall T U,
  tyeq T U ->
  forall k,
  tyeq (lift_ty k T) (lift_ty k U).

Proof.

unfold tyeq. eauto using tyapproxeqrr_lift.
Qed.

Lemma tyeq_subst:
  forall T1 T2,
  tyeq T1 T2 ->
  forall k U1 U2,
  tyeq U1 U2 ->
  tyeq (subst_ty U1 k T1) (subst_ty U2 k T2).

Proof.

unfold tyeq. eauto using tyapproxeqrr_subst.
Qed.

If the type T1 that we are substituting into is contractive with respect to the variable k that we are substituting for, then it is sufficient to require the types U1 and U2 to be n-equal, instead of n+1-equal. This is because U1 and U2 are copied at least one level deep. The hypothesis that T2 is contractive is not needed; it is implied by the fact that T1 is contractive and T1 and T2 are n+1-equal.

Lemma tyapproxeqrr_subst_contractive:
  forall (tyredl tyredr : ty -> ty -> Prop),
  (forall T1 T2, tyredl T1 T2 -> forall k, tyredl (lift_ty k T1) (lift_ty k T2)) ->
  (forall T1 T2, tyredr T1 T2 -> forall k, tyredr (lift_ty k T1) (lift_ty k T2)) ->
  (forall T1 T2, tyredl T1 T2 -> forall k U, tyredl (subst_ty U k T1) (subst_ty U k T2)) ->
  (forall T1 T2, tyredr T1 T2 -> forall k U, tyredr (subst_ty U k T1) (subst_ty U k T2)) ->
  (forall k T1, contractive k T1 -> forall T2, tyredl T1 T2 -> contractive k T2) ->
  forall n T1 T2,
  tyapproxeqrr tyredl tyredr (S n) T1 T2 ->
  forall k U1 U2,
  contractive k T1 ->
  tyapproxeqrr tyredl tyredr n U1 U2 ->
  tyapproxeqrr tyredl tyredr (S n) (subst_ty U1 k T1) (subst_ty U2 k T2).

Proof.

  introv ? ? ? ? ?.
  introv hT; dependent induction hT; introv hc hU; simpl;
  try solve [ eauto ];
  dependent destruction hc;
  eauto using tyapproxeqrr_subst, tyapproxeqrr_lift.
  unfold subst_var; by_cases; easy.
Qed.

Hint Immediate tyredmu_lift frozen_lift tyredmu_subst frozen_subst contractive_tyredmu.

-------------------------------------------------------------------------

A tactic for proving approximate equality goals.

Ltac tyapproxeqrr :=
  match goal with
  | |- tyapproxeqrr _ _ (S ?k) _ _ =>
      solve [ eauto using tyapproxeqrr_decreases, tyapproxeqrr_lift |
              econstructor; tyapproxeqrr ]
  | |- tyapproxeqrr _ _ ?k _ _ =>
      solve [ eauto using tyapproxeqrr_decreases, tyapproxeqrr_lift |
              destruct k; [ solve [ econstructor ] | tyapproxeqrr ]]
  | _ =>
      idtac "tyapproxeqrr: failure"
  end.

-------------------------------------------------------------------------

Properties of tyredmuc.

If subst_ty U k T1 reduces, and if T1 is contractive with respect to k, then T1 itself reduces. In other words, inserting some structure at a contractive position cannot create a new redex for tyredmuc. Indeed, tyredmuc allows reduction only in the left-hand side of a tensor, and this is not a contractive context.

Lemma tyredmuc_subst:
  forall k T1,
  contractive k T1 ->
  forall U T'2,
  tyredmuc (subst_ty U k T1) T'2 ->
  exists T2,
  tyredmuc T1 T2 /\
  T'2 = subst_ty U k T2 /\
  contractive k T2.

Proof.

induction 1; simpl; try solve [ intros; tyredmuc; tyredmu ].

TyVar

This cannot be the variable we are substituting for. Furthermore, a variable does not reduce. Thus, this case is impossible.

unfold subst_var. by_cases; tyredmuc; tyredmu.

TyMu

intros. tyredmuc. tyredmu. intuition eauto 6 using unfold_subst, contractive_unfold.

TyTensor

  intros. tyredmuc. tyredmu.
  forwards: IHcontractive. eassumption. unpack. subst.
  intuition eauto 6.
Qed.

As a consequence of the above result, we find that if T is accessible, then subst_ty U k T is accessible as well. In other words, if there were an infinite reduction sequence out of subst_ty U k T, there would be one out of T as well.

Lemma acc_tyredmuc_subst:
  forall T,
  Acc (transpose tyredmuc) T ->
  forall k,
  contractive k T ->
  forall U,
  Acc (transpose tyredmuc) (subst_ty U k T).
Ltac trivially_accessible :=
  constructor; intros; tyredmuc; tyredmu.

Proof.

unfold transpose. induction 1; intros. constructor; intros.
forwards: tyredmuc_subst. eassumption. eassumption. unpack. subst. eauto.
Qed.

The only way in which a tensor can reduce is via reduction of its left-hand side. As a result, if there were an infinite reduction sequence out of TyTensor T1 T2, there would be an infinite reduction sequence out of T1.

Lemma acc_tyredmuc_tensor:
  forall T1,
  Acc (transpose tyredmuc) T1 ->
  forall T2,
  Acc (transpose tyredmuc) (TyTensor T1 T2).

Proof.

unfold transpose. induction 1. constructor; intros. tyredmuc. tyredmu. eauto.
Qed.

This leads us to the conclusion that, at well-formed types, tyredmuc is well-founded.

Lemma tyredmuc_well_founded:
  forall T,
  wf T ->
  Acc (transpose tyredmuc) T.

Proof.

unfold transpose. induction 1; try solve [ constructor; intros; tyredmuc; tyredmu ].

TyMu

constructor; intros. tyredmuc. tyredmu. unfold unfold. eauto using acc_tyredmuc_subst.

TyTensor

eauto using acc_tyredmuc_tensor.
Qed.

-------------------------------------------------------------------------

A type is finite if it contains no occurrence of TyMu.

Inductive finite : ty -> Prop :=
| FiniteTyVar:
    forall x,
    finite (TyVar x)
| FiniteTyArrow:
    forall T1 T2,
    finite T1 ->
    finite T2 ->
    finite (TyArrow T1 T2)
| FiniteTyPair:
    forall layer1 layer2 T1 T2,
    finite T1 ->
    finite T2 ->
    finite (TyPair layer1 layer2 T1 T2)
| FiniteTyUnit:
    forall layer,
    finite (TyUnit layer)
| FiniteTyQ:
    forall q T,
    finite T ->
    finite (TyQ q T)
| FiniteTyBang:
    forall T,
    finite T ->
    finite (TyBang T)
| FiniteTyRef:
    forall T,
    finite T ->
    finite (TyRef T)
| FiniteTyRegion:
    forall r,
    finite (TyRegion r)
| FiniteTyAt:
    forall T,
    finite T ->
    finite (TyAt T)
| FiniteTyRegionCap:
    forall rk T1 T2,
    finite T1 ->
    finite T2 ->
    finite (TyRegionCap rk T1 T2)
| FiniteTyRegionCapPunched:
    forall T1 T2 T3,
    finite T1 ->
    finite T2 ->
    finite T3 ->
    finite (TyRegionCapPunched T1 T2 T3)
| FiniteTyTensor:
    forall T1 T2,
    finite T1 ->
    finite T2 ->
    finite (TyTensor T1 T2)
.

Hint Constructors finite.

-------------------------------------------------------------------------

Basic properties of finiteness.

Lemma finite_lift:
  forall T,
  finite T ->
  forall k,
  finite (lift_ty k T).

Proof.

induction 1; intros; simpl; eauto.
Qed.

Lemma finite_subst:
  forall T,
  finite T ->
  forall k U,
  finite U ->
  finite (subst_ty U k T).

Proof.

induction 1; intros; simpl; eauto using finite_lift.
unfold subst_var; by_cases; easy.
Qed.

Local Hint Resolve finite_lift finite_subst.

Lemma tyredmu_finite:
  forall T1 T2,
  tyredmu T1 T2 ->
  finite T1 ->
  False.

Proof.

inversion 1; inversion 1.
Qed.

Lemma tyred_finite:
  forall T1 T2,
  tyred T1 T2 ->
  finite T1 ->
  finite T2.

Proof.

induction 1; intros; hereditary finite; eauto 6.
false; eauto using tyredmu_finite.
Qed.

-------------------------------------------------------------------------

The following well-founded relation is used in the proof that approximate equality is transitive.

This relation is the restriction to finite types of the union of the sub-term relation and the type reduction relation.

Inductive fto : ty -> ty -> Prop :=
| FtoArrow1:
    forall T1 T2,
    finite T1 ->
    fto T1 (TyArrow T1 T2)
| FtoArrow2:
    forall T1 T2,
    finite T2 ->
    fto T2 (TyArrow T1 T2)
| FtoPair1:
    forall layer1 layer2 T1 T2,
    finite T1 ->
    fto T1 (TyPair layer1 layer2 T1 T2)
| FtoPair2:
    forall layer1 layer2 T1 T2,
    finite T2 ->
    fto T2 (TyPair layer1 layer2 T1 T2)
| FtoQ:
    forall q T,
    finite T ->
    fto T (TyQ q T)
| FtoBang:
    forall T,
    finite T ->
    fto T (TyBang T)
| FtoRef:
    forall T,
    finite T ->
    fto T (TyRef T)
| FtoAt:
    forall T,
    finite T ->
    fto T (TyAt T)
| FtoRegionCap1:
    forall rk T1 T2,
    finite T1 ->
    fto T1 (TyRegionCap rk T1 T2)
| FtoRegionCap2:
    forall rk T1 T2,
    finite T2 ->
    fto T2 (TyRegionCap rk T1 T2)
| FtoRegionCapPunched1:
    forall T1 T2 T3,
    finite T1 ->
    fto T1 (TyRegionCapPunched T1 T2 T3)
| FtoRegionCapPunched2:
    forall T1 T2 T3,
    finite T2 ->
    fto T2 (TyRegionCapPunched T1 T2 T3)
| FtoRegionCapPunched3:
    forall T1 T2 T3,
    finite T3 ->
    fto T3 (TyRegionCapPunched T1 T2 T3)
| FtoTensor1:
    forall T1 T2,
    finite T1 ->
    fto T1 (TyTensor T1 T2)
| FtoTensor2:
    forall T1 T2,
    finite T2 ->
    fto T2 (TyTensor T1 T2)
| FtoRed:
    forall T1 T2,
    tyred T1 T2 ->
    finite T2 ->
    fto T2 T1
.

Hint Constructors fto.

Lemma fto_finite:
  forall T1 T2,
  fto T1 T2 ->
  finite T1.

Proof.

introv h; dependent destruction h; eauto.
Qed.

-------------------------------------------------------------------------

A finite type is mapped to a skeleton where we only distinguish between tensors and other type constructors.

Proof.

induction T; simpl; congruence.
Qed.

When restricted to finite types, type reduction causes a decrease in the skeleton according to a lexicographic path ordering.

Lemma tyred_lpo:
  forall T1 T2,
  tyred T1 T2 ->
  finite T1 ->
  lt_lpo (skeleton T2) (skeleton T1).

Proof.

  induction 1; simpl; intros;
  hereditary finite;
  try rewrite skeleton_lift;
  try solve [ false; eauto using tyredmu_finite ];
  eauto with lpo.
Qed.

The same is true of fto.

Lemma fto_lpo:
  forall T1 T2,
  fto T1 T2 ->
  finite T2 ->
  lt_lpo (skeleton T1) (skeleton T2).

Proof.

introv step ?; dependent destruction step; simpl; eauto using tyred_lpo with lpo.
Qed.

This allows to prove that fto is well-founded.

Lemma fto2lpo:
  forall st,
  Acc lt_lpo st ->
  forall T,
  finite T ->
  st = skeleton T ->
  Acc fto T.

Proof.

induction 1. intros. constructor; intros. subst. eauto using fto_lpo, fto_finite.
Qed.

Lemma fto_well_founded:
well_founded fto.

Proof.

intro T1. constructor; intros T2 ?.
eauto using fto2lpo, myLPO_wf, fto_finite.
Qed.

-------------------------------------------------------------------------

The proposition unfolding k T U holds if the type U is the unfolding of the type T up to depth k.

Technically, the predicate unfolding is defined in terms of tyapproxeqrr, our generic notion of approximate equality. On the left-hand side, tyredmu is permitted, which means that recursive types can be unfolded, but tensors cannot be reduced. On the right-hand side, no reduction is permitted. Thus, this is a notion of unfolding where tensors are uninterpreted.

Notation unfolding :=
(tyapproxeqrr tyredmu frozen).

Every well-formed type T admits an unfolding U up to depth k, and U is a finite type.

Lemma unfolding_exists:
  forall k T,
  wf T ->
  exists U,
  unfolding k T U /\
  finite U.
Ltac unfolding_ih :=
  match goal with
  | hwf: wf ?T, ih: forall T, wf T -> _ |- _ =>
      unpack (ih _ hwf); clear hwf; unfolding_ih
  | |- _ =>
      idtac
  end.

Proof.

induction k.

When k is zero, we must give an explicit witness.

exists TyPhyUnit. eauto.

When k is non-zero, use an auxiliary induction over T.

induction 1; try solve [ unfolding_ih; unpack; eauto ].

TyMu

  match goal with h: wf ?T |- _ => assert (wf (TyMu T)); [ eauto 2 | clear h ] end.
  unfolding_ih; unpack.
  eexists; split.
  econstructor.
    econstructor.
    unfold unfold. eapply tyapproxeqrr_subst_contractive; eauto.
  eauto.
Qed.

If the unfolding of T1 is U, and if T1 takes one unfolding step towards T2, then the unfolding of T2 is also U.

Lemma unfolding_tyredmuc:
  forall k T1 U,
  unfolding k T1 U ->
  forall T2,
  tyredmuc T1 T2 ->
  unfolding k T2 U.

Proof.

induction 1; introv h; eauto; try solve [ tyredmuc; tyredmu ].

Case: T1 is a tensor. Then, the unfolding step must be a step of reduction under a context. The conclusion is immediate.

tyredmuc. tyredmu. eauto.

Case: the proof of equality between T1 and U begins with an unfolding step at the root of T1. Then, this step must coincide with the reduction step of T1 to T2.

tyredmu. tyredmuc. tyredmu. assumption.
Qed.

-------------------------------------------------------------------------

The following well-founded relation is used in the proof that approximate equality is transitive.

This relation is, roughly speaking, the restriction to well-formed types of the union of the sub-term relation and the type reduction relation. If it were defined in this way, though, it would not be well-founded, because the union of the sub-term relation and of the unfolding of recursive types is ill-founded. Thus, we add an integer depth, which decreases at every contractive constructor, and blocks at zero.

Inductive tto : (nat * ty) -> (nat * ty) -> Prop :=
| TtoArrow1:
    forall k T1 T2,
    wf T1 ->
    tto (k, T1) (S k, TyArrow T1 T2)
| TtoArrow2:
    forall k T1 T2,
    wf T2 ->
    tto (k, T2) (S k, TyArrow T1 T2)
| TtoPair1:
    forall k layer1 layer2 T1 T2,
    wf T1 ->
    tto (k, T1) (S k, TyPair layer1 layer2 T1 T2)
| TtoPair2:
    forall k layer1 layer2 T1 T2,
    wf T2 ->
    tto (k, T2) (S k, TyPair layer1 layer2 T1 T2)
| TtoQ:
    forall k q T,
    wf T ->
    tto (k, T) (S k, TyQ q T)
| TtoBang:
    forall k T,
    wf T ->
    tto (k, T) (S k, TyBang T)
| TtoRef:
    forall k T,
    wf T ->
    tto (k, T) (S k, TyRef T)
| TtoAt:
    forall k T,
    wf T ->
    tto (k, T) (S k, TyAt T)
| TtoRegionCap1:
    forall k rk T1 T2,
    wf T1 ->
    tto (k, T1) (S k, TyRegionCap rk T1 T2)
| TtoRegionCap2:
    forall k rk T1 T2,
    wf T2 ->
    tto (k, T2) (S k, TyRegionCap rk T1 T2)
| TtoRegionCapPunched1:
    forall k T1 T2 T3,
    wf T1 ->
    tto (k, T1) (S k, TyRegionCapPunched T1 T2 T3)
| TtoRegionCapPunched2:
    forall k T1 T2 T3,
    wf T2 ->
    tto (k, T2) (S k, TyRegionCapPunched T1 T2 T3)
| TtoRegionCapPunched3:
    forall k T1 T2 T3,
    wf T3 ->
    tto (k, T3) (S k, TyRegionCapPunched T1 T2 T3)
| TtoTensor1:
    forall k T1 T2,
    wf T1 ->
    tto (S k, T1) (S k, TyTensor T1 T2)
| TtoTensor2:
    forall k T1 T2,
    wf T2 ->
    tto (k, T2) (S k, TyTensor T1 T2)
| TtoRed:
    forall k T1 T2,
    tyred T1 T2 ->
    wf T2 ->
    tto (S k, T2) (S k, T1)
.

Hint Constructors tto.

-------------------------------------------------------------------------

Basic properties of tto.

Lemma tto_wf:
  forall k1 T1 k2 T2,
  tto (k1, T1) (k2, T2) ->
  wf T1.

Proof.

introv h; dependent destruction h; auto.
Qed.

Lemma acc_tto_zero:
forall T,
Acc tto (0, T).

Proof.

intro; constructor; intros [ ? ? ] h. dependent destruction h.
Qed.

-------------------------------------------------------------------------

The well-foundedness of tto reduces to that of fto.

If T1 takes a reduction step towards T2, then either this is an unfolding step -- that is, tyredmuc T1 T2 holds -- or this is a tensor simplification step -- and, in that case, the unfolding U1 of T1 is able to simulate this step.

Lemma tyred_unfolding:
  forall T1 T2,
  tyred T1 T2 ->
  tyredmuc T1 T2 \/
  forall k U1,
  unfolding (S k) T1 U1 ->
  exists U2,
  tyred U1 U2 /\
  unfolding (S k) T2 U2.
Ltac midnight_booze :=
  match goal with h: tyapproxeqrr _ _ (S _) _ _ |- _ =>
    depelim h; try solve [ tyredmu | frozen ]
  end.
Ltac hangover :=
  eexists; split; [ eauto | tyapproxeqrr ].

Proof.

  induction 1;
  try solve [ left; eauto 2 ];
  match goal with
  | ih: _ \/ _ |- _ =>
      idtac
  | _ =>

TyArrow, TyPair, etc.

right; intros; do 2 midnight_booze; hangover
end.

TyTensor

destruct IHtyred as [ ? | ih ]; [ left; eauto 2 | right; intros ].
midnight_booze. forwards: ih. eassumption. unpack. hangover.
Qed.

In a tto reduction sequence, every step either is an unfolding step -- but this cannot happen forever, because tyredmuc is well-founded -- or is reflected as an fto step in the unfolding. In other words, if there is an infinite tto reduction sequence out of T, then there is an infinite fto reduction sequence out of the unfolding of T.

Lemma tto2fto:
  forall U,
  Acc fto U ->
  finite U ->
  forall T,
  Acc (transpose tyredmuc) T ->
  forall k,
  unfolding k T U ->
  Acc tto (k, T).

Proof.

  unfold transpose.
  induction 1 as [ ? ? outer_ih ]; intro.
  induction 1 as [ ? ? inner_ih ]; introv eq.
  dependent destruction eq; try solve [
    frozen |
    eauto using acc_tto_zero
  ];
  constructor; intros [ ? ? ] htto; dependent destruction htto;
  hereditary finite;
  try solve [
    tyredmu |
    tyred; tyredmu |
    eauto using tyredmuc_well_founded
  ].

After this intimidating prologue, we are left with just two cases.

Case: a tensor takes a step.

This is either an unfolding step or a tensor simplification step.

forwards [ ? | u ]: tyred_unfolding. eassumption.

If the former, then nothing happens in the unfolding, and the inner induction hypothesis applies.

eapply inner_ih. eauto. eapply unfolding_tyredmuc. econstructor; eauto. eassumption.

If the latter, then the unfolding is able to simulate this step and to take an fto step. Thus, the outer induction hypothesis applies.

forwards: u. econstructor; eassumption. unpack.
eapply outer_ih; [ idtac | idtac | idtac | eassumption ]; eauto using tyred_finite, tyredmuc_well_founded.

Case: a tto step out of T involves a reduction step, and the definition of u involves an unfolding step. Because reduction is deterministic, these two steps must coincide, and the inner induction hypothesis applies.

tyredmu. tyred. tyredmu. eapply inner_ih; eauto.
Qed.

Thus, tto is well-founded.

Lemma tto_well_founded:
well_founded tto.

Proof.

intros [ ? ? ].

Take a first step, so as to obtain a well-formedness hypothesis.

constructor; intros [ ? ? ] ?.
forwards: tto_wf. eassumption.

Use the fact that every type has an unfolding.

forwards: unfolding_exists. eassumption. unpack.

Now, apply the above key lemma.

eapply tto2fto. apply fto_well_founded. eassumption. eauto using tyredmuc_well_founded. eauto.
Qed.

-------------------------------------------------------------------------

Type equality is a congruence with respect to the mu type constructor -- with a contractiveness condition.

The following lemma is a direct consequence of the definition of approximate equality. It is, however, not very useful, because of the unfolding in the premise.

Lemma tyeq_mu_mu:
  forall T U,
  tyeq (unfold T) (unfold U) ->
  tyeq (TyMu T) (TyMu U).

Proof.

unfold tyeq. eauto.
Qed.

How does one prove that unfold T and unfold U are k-equal? The key is to exploit a contractiveness condition and invoke the lemma tyapproxeq_subst_contractive. If one naively attempts to use tyapproxeq_subst, one finds that, after a series of proof steps, one comes back to the initial goal! Here, instead, we are back to a goal that is identical to the initial goal, except k has decreased, so, by induction over k, the proofs works out.

The contractiveness hypothesis is required: if it was absent, the lemma would be false. Take T and U to be TyVar 0. Then, T is equal to itself at every depth, because TyVar 0 is a well-formed type; but its unfolding TyMu (TyVar 0), an ill-formed type, is equal to itself only at depth 0.

Lemma tyapproxeq_unfold:
  forall T U,
  contractive 0 T ->
  forall k,
  tyapproxeq k T U ->
  tyapproxeq k (unfold T) (unfold U).

Proof.

induction k; intro; eauto.
unfold unfold. eauto 8 using tyapproxeqrr_subst_contractive, tyapproxeqrr_decreases.
Qed.

Thanks to the above key lemma, we find that, subject to a contractiveness condition, type equality is a congruence with respect to unfold and with respect to TyMu.

Lemma tyeq_unfold_unfold:
  forall T U,
  contractive 0 T ->
  tyeq T U ->
  tyeq (unfold T) (unfold U).

Proof.

unfold tyeq. eauto using tyapproxeq_unfold.
Qed.

Lemma tyapproxeq_mu:
  forall k T U,
  contractive 0 T ->
  tyapproxeq k T U ->
  tyapproxeq k (TyMu T) (TyMu U).

Proof.

eauto 8 using tyapproxeq_unfold.
Qed.

Lemma tyeq_mu:
  forall T U,
  contractive 0 T ->
  tyeq T U ->
  tyeq (TyMu T) (TyMu U).

Proof.

eauto using tyeq_mu_mu, tyeq_unfold_unfold.
Qed.

-------------------------------------------------------------------------

Reduction of types is deterministic.

Lemma tyred_deterministic:
  forall T U1 U2,
  tyred T U1 ->
  tyred T U2 ->
  U1 = U2.

Proof.

  induction T; introv h1 h2; dependent destruction h1; dependent destruction h2;
  repeat tyredmu;
  try solve [ tyred | tyred; tyredmu ];
  auto.

Only the case where both sides reduce under a tensor remains.

f_equal; eauto.
Qed.

Ltac tyred_deterministic :=
  match goal with
  h1: tyred ?T ?T1, h2: tyred ?T ?T2 |- _ =>
    unpack (tyred_deterministic h1 h2); subst T2; clear h2
  end.

-------------------------------------------------------------------------

The reflexive, transitive closure of tyred.

Inductive tyredstar : ty -> ty -> Prop :=
| TyRedStarNil:
    forall T,
    tyredstar T T
| TyRedStarCons:
    forall T1 T2 T3,
    tyred T1 T2 ->
    tyredstar T2 T3 ->
    tyredstar T1 T3.

Hint Constructors tyredstar.

Lemma tyredstar_tensor_context:
  forall T1 T2 U,
  tyredstar T1 T2 ->
  tyredstar (TyTensor T1 U) (TyTensor T2 U).

Proof.

induction 1; eauto.
Qed.

Lemma tyapproxeq_redstar_right:
  forall k T U1 U2,
  tyredstar U1 U2 ->
  tyapproxeq k T U2 ->
  tyapproxeq k T U1.

Proof.

induction 1; eauto.
Qed.

-------------------------------------------------------------------------

Reduction of types eventually reveals a type's true head constructor.

This is formalized as follows: if a type T is equal at depth S k to some arrow type, then T reduces to a related arrow type. The same is true of every other type constructor other than TyMu and TyTensor. I state a separate lemma for each type constructor, because I don't know how to do better. The proofs are shared via a tactic.

Lemma tyred_reveals_arrow:
  forall k T U1 U2,
  tyapproxeq (S k) (TyArrow U1 U2) T ->
  exists T1 T2,
  tyredstar T (TyArrow T1 T2) /\
  tyapproxeq k U1 T1 /\
  tyapproxeq k U2 T2.

Proof.

introv h; dependent induction h.

The first case is obvious: T is an arrow.

intuition eauto 10.

In the second case, TyArrow U1 U2 makes a step; but that is impossible.

tyred. tyredmu.

The last case is easy: T reduces by one step; we conclude via the induction hypothesis.

  match goal with ih: forall k, _ |- _ =>
    forwards: ih; [ reflexivity | reflexivity | unpack; intuition eauto 8 ]
  end.
Qed.

Ltac tyred_reveals :=
  introv h; dependent induction h; solve [
    intuition eauto 10
  | tyred; tyredmu
  | match goal with ih: forall k, _ |- _ =>
      forwards: ih; [ reflexivity | reflexivity | unpack; intuition eauto 8 ]
    end
  ].

Lemma tyred_reveals_pair:
  forall k layer1 layer2 T U1 U2,
  tyapproxeq (S k) (TyPair layer1 layer2 U1 U2) T ->
  exists T1 T2,
  tyredstar T (TyPair layer1 layer2 T1 T2) /\
  tyapproxeq k U1 T1 /\
  tyapproxeq k U2 T2.

Proof.

tyred_reveals.
Qed.

Lemma tyred_reveals_unit:
  forall k layer T,
  tyapproxeq (S k) (TyUnit layer) T ->
  tyredstar T (TyUnit layer).

Proof.

tyred_reveals.
Qed.

Lemma tyred_reveals_q:
  forall k T q U1,
  tyapproxeq (S k) (TyQ q U1) T ->
  exists T1,
  tyredstar T (TyQ q T1) /\
  tyapproxeq k U1 T1.

Proof.

tyred_reveals.
Qed.

Lemma tyred_reveals_bang:
  forall k T U1,
  tyapproxeq (S k) (TyBang U1) T ->
  exists T1,
  tyredstar T (TyBang T1) /\
  tyapproxeq k U1 T1.

Proof.

tyred_reveals.
Qed.

Lemma tyred_reveals_ref:
  forall k T U1,
  tyapproxeq (S k) (TyRef U1) T ->
  exists T1,
  tyredstar T (TyRef T1) /\
  tyapproxeq k U1 T1.

Proof.

tyred_reveals.
Qed.

Lemma tyred_reveals_at:
  forall k T U1,
  tyapproxeq (S k) (TyAt U1) T ->
  exists T1,
  tyredstar T (TyAt T1) /\
  tyapproxeq k U1 T1.

Proof.

tyred_reveals.
Qed.

Lemma tyred_reveals_regioncap:
  forall k T rk U1 U2,
  tyapproxeq (S k) (TyRegionCap rk U1 U2) T ->
  exists T1 T2,
  tyredstar T (TyRegionCap rk T1 T2) /\
  tyapproxeq k U1 T1 /\
  tyapproxeq k U2 T2.

Proof.

tyred_reveals.
Qed.

Lemma tyred_reveals_regioncappunched:
  forall k T U1 U2 U3,
  tyapproxeq (S k) (TyRegionCapPunched U1 U2 U3) T ->
  exists T1 T2 T3,
  tyredstar T (TyRegionCapPunched T1 T2 T3) /\
  tyapproxeq k U1 T1 /\
  tyapproxeq k U2 T2 /\
  tyapproxeq k U3 T3.

Proof.

tyred_reveals.
Qed.

-------------------------------------------------------------------------

Approximate type equality is closed under reduction. (It is also, by definition, closed under inverse reduction.)

Lemma tyapproxeq_tyred:
  forall k T1 U,
  tyapproxeq k T1 U ->
  forall T2,
  tyred T1 T2 ->
  tyapproxeq k T2 U.

Proof.

induction 1; introv h; eauto; try solve [ tyred; tyredmu ].

Case: T1 is a tensor, of the form TyTensor T1 T2, and U is also a tensor, of the form TyTensor U1 U2. The approximate equality proof between these tensors was obtained via structural decomposition, so we have tyapproxeq (S k) T1 U1 and tyapproxeq k T2 U2.

We proceed by case analysis over the reduction step out of TyTensor T1 T2.

dependent destruction h; try solve [ tyredmu ].

Sub-case: T1 is an arrow.

Because U1 is related to T1, it must itself reduce to an arrow.

forwards [ U11 [ U12 ? ]]: tyred_reveals_arrow. eassumption. unpack.

Because reduction under tensor is permitted, TyTensor U1 U2 reduces to TyTensor (TyArrow U11 U12) U2, which itself reduces.

  eapply tyapproxeq_redstar_right.
    eapply tyredstar_tensor_context. eassumption.
    eapply TyApproxEqRedRight. econstructor. tyapproxeqrr.

The following sub-cases are analogous.

  Ltac trcase h :=
    forwards: h; [ eassumption | unpack;
    eapply tyapproxeq_redstar_right; [
      eapply tyredstar_tensor_context; eassumption
    | eapply TyApproxEqRedRight; [ econstructor | tyapproxeqrr ]
    ]].

  trcase tyred_reveals_pair.
  trcase tyred_reveals_unit.
  trcase tyred_reveals_q.
  trcase tyred_reveals_bang.
  trcase tyred_reveals_ref.
  trcase tyred_reveals_at.
  trcase tyred_reveals_regioncap.
  trcase tyred_reveals_regioncappunched.

Sub-case: T1 itself reduces, and TyTensor T1 T2 reduces via reduction under a context. The goal is obtained via the induction hypothesis.

eauto.

Case: we have two reduction steps out of T1.

tyred_deterministic. assumption.

Qed.

As a special case of the above result, we find that the reduction of a tensor type is guided by the head constructor of its first argument.

This is formalized via a commutative diagram: if TyTensor T1 T2 reduces, if we change T1 to U1 via approximate equality at depth S k (so T1 and U1 have the same head constructor), if we change T2 to U2 via approximate equality at depth k, then TyTensor U1 U2 reduces to a related result.

Lemma tyred_tensor:
  forall T1 T2 T,
  tyred (TyTensor T1 T2) T ->
  forall k U1 U2,
  tyapproxeq (S k) T1 U1 ->
  tyapproxeq k T2 U2 ->
  tyapproxeq (S k) T (TyTensor U1 U2).

Proof.

eauto using tyapproxeq_tyred.
Qed.

-------------------------------------------------------------------------

Type reduction preserves well-formedness.

Lemma tyred_wf:
  forall T1 T2,
  tyred T1 T2 ->
  wf T1 ->
  wf T2.

Proof.

cut (forall T1, wf T1 -> forall T2, tyred T1 T2 -> wf T2). eauto.
induction 1; intros; tyred; try tyredmu; hereditary wf; eauto 8 using wf_unfold.
Qed.

-------------------------------------------------------------------------

Approximate equality is a partial equivalence relation. At well-formed types, it is reflexive. (At non-well-formed types, the level 0 relation is the full relation, but the level 1 relation never gets off the ground.) It is symmetric. At well-formed pivots, it is transitive.

Before the introduction of tensor, the transitivity proof did not require a well-formedness hypothesis. In the presence of tensor, I was not able to make the proof go through without this hypothesis.

Lemma tyapproxeq_reflexive:
  forall k T,
  wf T ->
  tyapproxeq k T T.

Proof.

  induction k; eauto.
  induction 1; eauto.
  apply tyapproxeq_mu; auto.
Qed.

Lemma tyapproxeq_symmetric:
  forall k T1 T2,
  tyapproxeq k T1 T2 ->
  tyapproxeq k T2 T1.

Proof.

induction 1; eauto.
Qed.

Lemma tyapproxeq_transitive:
  forall k T2,
  wf T2 ->
  forall T1,
  tyapproxeq k T1 T2 ->
  forall T3,
  tyapproxeq k T2 T3 ->
  tyapproxeq k T1 T3.

Proof.

We wish to reason by well-founded induction over the pair (k, T2). This requires massaging the goal as follows.

  cut (
    forall kT2 : nat * ty,
    match kT2 with (k, T2) =>
    wf T2 ->
    forall T1,
    tyapproxeq k T1 T2 ->
    forall T3,
    tyapproxeq k T2 T3 ->
    tyapproxeq k T1 T3
    end
  ). solve [ intros h k T2; apply (h (k, T2)) ].

Now, announce our induction schema.

intro kT2. induction_wf ih: tto_well_founded kT2. destruct kT2 as [ k T2 ].

We must now massage the induction hypothesis in the opposite way, so as to make k and T2 separate parameters again! Otherwise, eauto does not know how to instantiate the induction hypothesis.

We seize this opportunity to remove the hypothesis wf T2b, which is redundant, because it is implied by the hypothesis tto (kb, T2b) (k, T2).

We seize this opportunity to put the two most interesting hypotheses first, and the routine verification hypothesis last. This may help eauto guess how to instantiate the induction hypothesis.

  assert (IH:
    forall kb T2b T1 T3,
    tyapproxeq kb T1 T2b ->
    tyapproxeq kb T2b T3 ->
    tto (kb, T2b) (k, T2) ->
    tyapproxeq kb T1 T3
  ). solve [ intros; apply (ih (kb, T2b)); eauto using tto_wf ].
  clear ih.

We are now ready to begin the proof!

Eliminate the case where k is zero.

destruct k. eauto.

Launch auxiliary structural inductions over the two equality hypotheses, and let eauto deal with most of the cases that arise.

  intro wfT2.
  introv eq1; dependent induction eq1; hereditary wf; eauto 3;
  introv eq2; dependent induction eq2; try solve [ tyred; tyredmu ]; hereditary wf;
  try solve [ econstructor; eauto 3 ];
  try solve [ eauto 3 ].

Only three cases should remain.

Case: the guy in the middle is a tensor and reduces (as part of the right-hand approximate equality proof) while the left-hand approximate equality proof uses TyApproxEqTensor.

  forwards: tyred_tensor.
    eassumption.
    apply tyapproxeq_symmetric; eassumption.
    apply tyapproxeq_symmetric; eassumption.
  eapply IH.
    apply tyapproxeq_symmetric; eassumption.
    eassumption.
    eauto using tyred_wf.

Case: the guy in the middle is a tensor and reduces (as part of the left-hand approximate equality proof) while the right-hand approximate equality proof uses TyApproxEqTensor.

  forwards: tyred_tensor.
    eassumption.
    eassumption.
    eassumption.
  eapply IH.
    eassumption.
    eassumption.
    eauto using tyred_wf.

Case: the guy in the middle reduces in two different ways via tyred.

tyred_deterministic. eauto using tyred_wf.
Qed.

-------------------------------------------------------------------------

Type equality is also a partial equivalence relation.

Lemma tyeq_reflexive:
forall T, wf T -> tyeq T T.

Proof.

unfold tyeq. eauto using tyapproxeq_reflexive.
Qed.

Lemma tyeq_symmetric:
forall T1 T2, tyeq T1 T2 -> tyeq T2 T1.

Proof.

unfold tyeq. eauto using tyapproxeq_symmetric.
Qed.

Lemma tyeq_transitive:
forall T1 T2 T3, tyeq T1 T2 -> tyeq T2 T3 -> wf T2 -> tyeq T1 T3.

Proof.

unfold tyeq. eauto using tyapproxeq_transitive.
Qed.

Hint Resolve tyeq_reflexive.

-------------------------------------------------------------------------

Type equality is a congruence with respect to ordinary type constructors.

Ltac tyeq_congruence :=
  unfold tyeq; eauto with tyapproxeqrr_increment.

Lemma tyeq_var:
  forall x,
  tyeq (TyVar x) (TyVar x).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_arrow:
  forall T1 T2 U1 U2,
  tyeq T1 U1 ->
  tyeq T2 U2 ->
  tyeq (TyArrow T1 T2) (TyArrow U1 U2).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_pair:
  forall layer1 layer2 T1 T2 U1 U2,
  tyeq T1 U1 ->
  tyeq T2 U2 ->
  tyeq (TyPair layer1 layer2 T1 T2) (TyPair layer1 layer2 U1 U2).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_q:
  forall q T U,
  tyeq T U ->
  tyeq (TyQ q T) (TyQ q U).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_bang:
  forall T U,
  tyeq T U ->
  tyeq (TyBang T) (TyBang U).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_ref:
  forall T U,
  tyeq T U ->
  tyeq (TyRef T) (TyRef U).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_region:
forall r,
tyeq (TyRegion r) (TyRegion r).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_at:
  forall T U,
  tyeq T U ->
  tyeq (TyAt T) (TyAt U).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_regioncap:
  forall rk T1 T2 U1 U2,
  tyeq T1 U1 ->
  tyeq T2 U2 ->
  tyeq (TyRegionCap rk T1 T2) (TyRegionCap rk U1 U2).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_regioncappunched:
  forall T1 T2 T3 U1 U2 U3,
  tyeq T1 U1 ->
  tyeq T2 U2 ->
  tyeq T3 U3 ->
  tyeq (TyRegionCapPunched T1 T2 T3) (TyRegionCapPunched U1 U2 U3).

Proof.

tyeq_congruence.
Qed.

Lemma tyeq_tensor:
  forall T1 T2 U1 U2,
  tyeq T1 U1 ->
  tyeq T2 U2 ->
  tyeq (TyTensor T1 T2) (TyTensor U1 U2).

Proof.

tyeq_congruence.
Qed.

Hint Resolve tyeq_var tyeq_arrow tyeq_pair tyeq_q tyeq_bang tyeq_ref
tyeq_region tyeq_at tyeq_regioncap tyeq_regioncappunched tyeq_tensor :
tyeq_congruence.

-------------------------------------------------------------------------

This tactic proves a well-formedness goal.

Ltac wf :=
repeat constructor; eauto.

-------------------------------------------------------------------------

Type equality includes the equational theory of tensor.

Lemma tyred_tyeq:
  forall T1 T2,
  tyred T1 T2 ->
  wf T2 ->
  tyeq T1 T2.

Proof.

unfold tyeq. eauto using tyapproxeq_reflexive.
Qed.

These lemmas duplicate the definition of tyred, which is rather unpleasant. One could try to avoid this by exploiting the tactic tyred_tyeq directly -- all of these lemmas have the same proof -- but that might be more brittle.

TEMPORARY remove these lemmas if they become unused -- see Revelation

Ltac tyred_tyeq :=
  intros; eapply tyred_tyeq; [ eauto | wf ].

Lemma tyeq_tensor_arrow:
  forall T1 T2 U,
  wf T1 ->
  wf T2 ->
  wf U ->
  tyeq (TyTensor (TyArrow T1 T2) U) (TyArrow (TyCompos T1 U) (TyCompos T2 U)).

Proof.

tyred_tyeq.
Qed.

Lemma tyeq_tensor_pair:
  forall layer1 layer2 T1 T2 U,
  wf T1 ->
  wf T2 ->
  wf U ->
  tyeq (TyTensor (TyPair layer1 layer2 T1 T2) U) (TyPair layer1 layer2 (TyTensor T1 U) (TyTensor T2 U)).

Proof.

tyred_tyeq.
Qed.

Lemma tyeq_tensor_unit:
  forall layer U,
  wf U ->
  tyeq (TyTensor (TyUnit layer) U) (TyUnit layer).

Proof.

tyred_tyeq.
Qed.

Lemma tyeq_tensor_q:
  forall q T U,
  wf T ->
  wf U ->
  tyeq (TyTensor (TyQ q T) U) (TyQ q (TyTensor T (lift_ty 0 U))).

Proof.

tyred_tyeq.
Qed.

Lemma tyeq_tensor_bang:
  forall T U,
  wf T ->
  wf U ->
  tyeq (TyTensor (TyBang T) U) (TyBang (TyTensor T U)).

Proof.

tyred_tyeq.
Qed.

Lemma tyeq_tensor_ref:
  forall T U,
  wf T ->
  wf U ->
  tyeq (TyTensor (TyRef T) U) (TyRef (TyTensor T U)).

Proof.

tyred_tyeq.
Qed.

Lemma tyeq_tensor_at:
  forall sigma U,
  wf sigma ->
  wf U ->
  tyeq (TyTensor (TyAt sigma) U) (TyAt sigma).

Proof.

tyred_tyeq.
Qed.

Lemma tyeq_tensor_regioncap:
  forall rk sigma T U,
  wf sigma ->
  wf T ->
  wf U ->
  tyeq (TyTensor (TyRegionCap rk sigma T) U) (TyRegionCap rk sigma (TyTensor T U)).

Proof.

tyred_tyeq.
Qed.

Lemma tyeq_tensor_regioncappunched:
  forall rho sigma T U,
  wf rho ->
  wf sigma ->
  wf T ->
  wf U ->
  tyeq (TyTensor (TyRegionCapPunched rho T sigma) U) (TyRegionCapPunched rho (TyTensor T U) sigma).

Proof.

tyred_tyeq.
Qed.

-------------------------------------------------------------------------

Type equality is consistent.

Lemma tyeq_decompose_var:
  forall x y,
  tyeq (TyVar x) (TyVar y) ->
  x = y.

Proof.

introv h. specializes h 1. dependent destruction h; auto with tyred.
Qed.

Ltac tyeq_hereditary :=
  intros;
  match goal with
  | h: tyeq ?T ?U |- tyeq _ _ =>
      intro k;
      try solve [
        generalize (h k); clear h; intro h; inversion h; auto with tyred |
        generalize (h (S k)); clear h; intro h; inversion h; auto with tyred
      ]
  | h: tyeq ?T ?U |- _ = _ =>
      specializes h 1; inversion h; auto with tyred
  end.

Lemma tyeq_decompose_arrow:
  forall T1 T2 U1 U2,
  tyeq (TyArrow T1 T2) (TyArrow U1 U2) ->
  tyeq T1 U1 /\ tyeq T2 U2.

Proof.

intuition tyeq_hereditary.
Qed.

Lemma tyeq_decompose_pair:
  forall layer1a layer2a layer1b layer2b T1 T2 U1 U2,
  tyeq (TyPair layer1a layer2a T1 T2) (TyPair layer1b layer2b U1 U2) ->
  layer1a = layer1b /\ layer2a = layer2b /\ tyeq T1 U1 /\ tyeq T2 U2.

Proof.

intuition tyeq_hereditary.
Qed.

Lemma tyeq_decompose_unit:
  forall layera layerb,
  tyeq (TyUnit layera) (TyUnit layerb) ->
  layera = layerb.

Proof.

intuition tyeq_hereditary.
Qed.

Lemma tyeq_decompose_q:
  forall q T U,
  tyeq (TyQ q T) (TyQ q U) ->
  tyeq T U.

Proof.

tyeq_hereditary.
Qed.

Lemma tyeq_decompose_bang:
  forall T U,
  tyeq (TyBang T) (TyBang U) ->
  tyeq T U.

Proof.

tyeq_hereditary.
Qed.

Lemma tyeq_decompose_ref:
  forall T U,
  tyeq (TyRef T) (TyRef U) ->
  tyeq T U.

Proof.

tyeq_hereditary.
Qed.

Lemma tyeq_decompose_region:
  forall r1 r2,
  tyeq (TyRegion r1) (TyRegion r2) ->
  r1 = r2.

Proof.

tyeq_hereditary.
Qed.

Lemma tyeq_decompose_at:
  forall T U,
  tyeq (TyAt T) (TyAt U) ->
  tyeq T U.

Proof.

tyeq_hereditary.
Qed.

Lemma tyeq_decompose_regioncap:
  forall rk1 rk2 T1 T2 U1 U2,
  tyeq (TyRegionCap rk1 T1 T2) (TyRegionCap rk2 U1 U2) ->
  rk1 = rk2 /\ tyeq T1 U1 /\ tyeq T2 U2.

Proof.

intuition tyeq_hereditary.
Qed.

Lemma tyeq_decompose_regioncappunched:
  forall T1 T2 T3 U1 U2 U3,
  tyeq (TyRegionCapPunched T1 T2 T3) (TyRegionCapPunched U1 U2 U3) ->
  tyeq T1 U1 /\ tyeq T2 U2 /\ tyeq T3 U3.

Proof.

intuition tyeq_hereditary.
Qed.

Ltac tyeq :=
  match goal with
  | h: tyeq (TyVar ?v) (TyVar _) |- _ =>
      unpack (tyeq_decompose_var h); clear h; try subst v; tyeq
  | h: tyeq (TyArrow _ _) (TyArrow _ _) |- _ =>
      unpack (tyeq_decompose_arrow h); clear h; tyeq
  | h: tyeq (TyPair ?layer1 ?layer2 _ _) (TyPair _ _ _ _) |- _ =>
      unpack (tyeq_decompose_pair h); clear h; try subst layer1; try subst layer2; tyeq
  | h: tyeq (TyUnit ?layer) (TyUnit _) |- _ =>
      unpack (tyeq_decompose_unit h); clear h; try subst layer; tyeq
  | h: tyeq (TyQ _ _) (TyQ _ _) |- _ =>
      unpack (tyeq_decompose_q h); clear h; tyeq
  | h: tyeq (TyBang _) (TyBang _) |- _ =>
      unpack (tyeq_decompose_bang h); clear h; tyeq
  | h: tyeq (TyRef _) (TyRef _) |- _ =>
      unpack (tyeq_decompose_ref h); clear h; tyeq
  | h: tyeq (TyRegion ?r) (TyRegion _) |- _ =>
      unpack (tyeq_decompose_region h); clear h; try subst r; tyeq
  | h: tyeq (TyAt _) (TyAt _) |- _ =>
      unpack (tyeq_decompose_at h); clear h; tyeq
  | h: tyeq (TyRegionCap ?rk _ _) (TyRegionCap _ _ _) |- _ =>
      unpack (tyeq_decompose_regioncap h); clear h; try subst rk; tyeq
  | h: tyeq (TyRegionCapPunched _ _ _) (TyRegionCapPunched _ _ _) |- _ =>
      unpack (tyeq_decompose_regioncappunched h); clear h; tyeq
  | _ =>
      idtac
  end.

Hint Extern 1 (tyeq _ _) => tyeq.

Ltac impossible :=
  false; match goal with h: tyeq ?T1 ?T2 |- _ => specializes h 1; inversion h; auto with tyred end.

Lemma tyeq_impossible_example:
  forall T1 T2 U,
  ~ (tyeq (TyArrow T1 T2) (TyRef U)).

Proof.

intros; intro. impossible.
Qed.

-------------------------------------------------------------------------

The following lemma and tactic are useful when a region is known under two different names.

Lemma two_regions:
  forall r1 r2 sigma,
  tyeq (TyRegion r1) sigma ->
  tyeq (TyRegion r2) sigma ->
  wf sigma ->
  r1 = r2.

Proof.

intros. eapply tyeq_decompose_region. eauto using tyeq_symmetric, tyeq_transitive.
Qed.

Ltac two_regions :=
  match goal with
  h1: tyeq (TyRegion ?r1) ?sigma,
  h2: tyeq (TyRegion ?r2) ?sigma |- _ =>
    forwards: (two_regions h1 h2); [ wf | subst r1; clear h1 ]
  end.

-------------------------------------------------------------------------

Prior to the introduction of tensor, we could prove that type equality implies well-formedness: that is, well-formedness was a necessary and sufficient condition for a type to be equal to itself. This is no longer the case, because the reduction rules for tensor can cause an ill-formed sub-term to vanish. Perhaps one could attempt to fix this by altering the definition of tyred and requiring any term that vanishes to be well-formed. However, it seems simpler to just abandon this property. After all, we are not interested in ill-formed types, and we don't care if some of them happen to participate in the equality relation.

-------------------------------------------------------------------------

At well-formed types, type equality validates the folding and unfolding of recursive types. In other words, TyMu T is a solution of the contractive equation represented by T.

Lemma tyeq_fold:
  forall T,
  wf (TyMu T) ->
  tyeq (unfold T) (TyMu T).

Proof.

intros; intro. eauto using tyapproxeq_reflexive, wf_unfold.
Qed.

Lemma tyeq_unfold:
  forall T,
  wf (TyMu T) ->
  tyeq (TyMu T) (unfold T).

Proof.

intros; intro. eauto using tyapproxeq_reflexive, wf_unfold.
Qed.

Contractive type equations have unique solutions.

Lemma contractive_type_equations_have_unique_solutions:
  forall T,
  wf (TyMu T) ->
  forall U1 U2,
  tyeq U1 (subst_ty U1 0 T) ->
  tyeq U2 (subst_ty U2 0 T) ->
  wf U1 ->
  wf U2 ->
  tyeq U1 U2.

Proof.

  introv wfmt h1 h2 ? ?. dependent destruction wfmt. intro k; induction k; auto.
  eapply tyapproxeq_transitive; [ idtac | eexact (h1 (S k)) | idtac ]. eauto.
  eapply tyapproxeq_transitive; [ idtac | idtac | eexact (tyeq_symmetric h2 (S k)) ]. eauto.
  eapply tyapproxeqrr_subst_contractive; eauto.
  eapply tyeq_reflexive. assumption.
Qed.

In fact, the unique solution of the type equation represented by T is of course TyMu T.

Lemma contractive_type_equations_have_solution_mu:
  forall T,
  wf (TyMu T) ->
  forall U,
  tyeq U (subst_ty U 0 T) ->
  wf U ->
  tyeq U (TyMu T).

Proof.

  intros.
  eapply contractive_type_equations_have_unique_solutions; eauto.
  apply tyeq_unfold.
  assumption.
Qed.

-------------------------------------------------------------------------

Tensor commutes with type substitution.

Perhaps surprisingly, the proof of this fact is trivial. This is so because the behavior of substitution at tensors is already built in the definition of subst_ty. What was perhaps non-trivial was the fact that type equality is compatible with substitution; this was proved earlier.

Lemma tensor_subst:
  forall U k T1 T2,
  wf U ->
  wf T1 ->
  wf T2 ->
  tyeq (TyTensor (subst_ty U k T1) T2) (subst_ty U k (TyTensor T1 (lift_ty k T2))).

Proof.

intros. simpl. rewrite subst_lift_ty. eauto.
Qed.

-------------------------------------------------------------------------

The following hint can help prove that types are well-formed.

Hint Extern 1 (wf _) => hereditary wf; repeat constructor.

-------------------------------------------------------------------------

Lifting is injective with respect to type equality.

Lemma tyredmu_lift_inverse:
  forall k T1 T2,
  tyredmu (lift_ty k T1) T2 ->
  exists T'2,
  tyredmu T1 T'2 /\
  T2 = lift_ty k T'2.

Proof.

introv h. dependent destruction h.
invert_lift_equality. eauto using unfold_lift.
Qed.

Lemma tyred_lift_inverse:
  forall k T1 T2,
  tyred (lift_ty k T1) T2 ->
  exists T'2,
  tyred T1 T'2 /\
  T2 = lift_ty k T'2.

Proof.

introv h. dependent induction h;

Base cases.

try solve [ do 2 invert_lift_equality; try rewrite lift_lift_ty; eauto ].

Reduction under a tensor.

invert_lift_equality. generalize (IHh _ _ eq_refl); clear IHh; intro. unpack. subst. eauto.

tyredmu

forwards: tyredmu_lift_inverse. eassumption. unpack. subst. eauto.
Qed.

Lemma lift_ty_injective_tyapproxeq:
  forall j k T1 T2,
  tyapproxeq j (lift_ty k T1) (lift_ty k T2) ->
  tyapproxeq j T1 T2.

Proof.

introv h. dependent induction h; eauto 1;

All congruence cases.

try solve [ do 2 invert_lift_equality; eauto ].

TyVar

do 2 invert_lift_equality. forwards: lift_var_injective. eassumption. subst; eauto.

tyred

forwards: tyred_lift_inverse. eassumption. unpack. eauto.
forwards: tyred_lift_inverse. eassumption. unpack. eauto.
Qed.

Lemma lift_ty_injective_tyeq:
  forall k T1 T2,
  tyeq (lift_ty k T1) (lift_ty k T2) ->
  tyeq T1 T2.

Proof.

unfold tyeq. eauto using lift_ty_injective_tyapproxeq.
Qed.

Lemma tyeq_region_lift:
  forall { r k sigma },
  tyeq (TyRegion r) (lift_ty k sigma) ->
  tyeq (TyRegion r) sigma.

Proof.

  introv h.
  change (TyRegion r) with (lift_ty k (TyRegion r)) in h.
  eauto using lift_ty_injective_tyeq.
Qed.

Ltac tyeq_region_lift :=
  match goal with
  h: tyeq (TyRegion _) (lift_ty _ _) |- _ =>
    generalize (tyeq_region_lift h); clear h; intro h
  end.