Coral.Types: simple types, well typed terms, and type soundness

Author: Benoît Montagu
Copyright © Inria 2020 CeCILL-B License
Synopsis: Simple types, typing judgment, preservation and progress, and relation over typed terms.

Require Import Infrastructure.
Import Notations.
Require Import Env.
Require Import Transp.
Require Import Rel.
Require Import RelLc.
Require Import RelClosed.
Require Import Lia.

Types

Simple types: unit, pairs, binary sums, and function types. This is the definition in Section 5.2 on page 19 of the ICFP'20 paper.
Inductive ty: Type :=
| TUnit
| TPair (tau1 tau2: ty)
| TSum (tau1 tau2: ty)
| TFun (tau1 tau2: ty)
.

Equality is decidable for types.
Definition ty_eq_dec (tau1 tau2: ty): { tau1 = tau2 } + { tau1 ≠ tau2 }.
Proof.
  decide equality.
Qed.

Size of a type.
Fixpoint ty_size (tau: ty) : nat :=
  match tau with
  | TUnit ⇒ 1
  | TPair tau1 tau2 | TSum tau1 tau2 | TFun tau1 tau2 ⇒ 1 + ty_size tau1 + ty_size tau2
  end.

A type cannot have size 0.
Lemma ty_size_not_zero tau:
  ty_size tau ≠ 0.
Proof.
  destruct tau; simpl; lia.
Qed.

Typing judgment

Typing judgment for terms. wf_term Gamma t tau says that in the typing environment Gamma, the term t has type tau.
Inductive wf_term: env ty → term → ty → Prop :=
| WfVar: ∀ Gamma x tau,
    get x Gamma = Some tau →
    wf_term Gamma (Var x) tau
| WfLet: ∀ Gamma x t1 t2 tau1 tau2,
    wf_term Gamma t1 tau1 →
    wf_term (x ¬ tau1 ++ Gamma) t2 tau2 →
    x `notin` dom Gamma →
    wf_term Gamma (Let t1 (close x t2)) tau2
| WfLam: ∀ Gamma x t tau1 tau2,
    wf_term (x ¬ tau1 ++ Gamma) t tau2 →
    x `notin` dom Gamma →
    wf_term Gamma (Lam (close x t)) (TFun tau1 tau2)
| WfApp: ∀ Gamma t1 t2 tau1 tau2,
    wf_term Gamma t1 (TFun tau2 tau1) →
    wf_term Gamma t2 tau2 →
    wf_term Gamma (App t1 t2) tau1
| WfUnit: ∀ Gamma,
    wf_term Gamma Unit TUnit
| WfPair: ∀ Gamma t1 t2 tau1 tau2,
    wf_term Gamma t1 tau1 →
    wf_term Gamma t2 tau2 →
    wf_term Gamma (Pair t1 t2) (TPair tau1 tau2)
| WfFst: ∀ Gamma t tau1 tau2,
    wf_term Gamma t (TPair tau1 tau2) →
    wf_term Gamma (Fst t) tau1
| WfSnd: ∀ Gamma t tau1 tau2,
    wf_term Gamma t (TPair tau1 tau2) →
    wf_term Gamma (Snd t) tau2
| WfInjL: ∀ Gamma t tau1 tau2,
    wf_term Gamma t tau1 →
    wf_term Gamma (InjL t) (TSum tau1 tau2)
| WfInjR: ∀ Gamma t tau1 tau2,
    wf_term Gamma t tau2 →
    wf_term Gamma (InjR t) (TSum tau1 tau2)
| WfMatch: ∀ Gamma t x1 t1 x2 t2 tau tau1 tau2,
    wf_term Gamma t (TSum tau1 tau2) →
    wf_term (x1 ¬ tau1 ++ Gamma) t1 tau →
    x1 `notin` dom Gamma →
    wf_term (x2 ¬ tau2 ++ Gamma) t2 tau →
    x2 `notin` dom Gamma →
    wf_term Gamma (Match t (close x1 t1) (close x2 t2)) tau
.

Well typed terms are locally-closed.
Lemma wf_term_lc Gamma t tau:
  wf_term Gamma t tau →
  lc t.
Proof.
  intro Hwf. induction Hwf; auto with lngen.
Qed.
Hint Resolve wf_term_lc: lngen.

The free variables of well typed terms belong to the domain of the typing environment.
Lemma wf_term_fv Gamma t tau:
  wf_term Gamma t tau →
  fv t [<=] dom Gamma.
Proof.
  intro Hwf. induction Hwf; simpl in *; try (repeat rewrite fv_close); try fsetdec.
  apply get_in_dom in H. fsetdec.
Qed.

wf_term is equivariant.
Lemma wf_term_equivariant x y Gamma t tau:
  wf_term Gamma t tau ↔ wf_term (transp_dom x y Gamma) (transp_term x y t) tau.
Proof.
  revert Gamma t tau.
  assert (∀ Gamma t tau,
             wf_term Gamma t tau →
             wf_term (transp_dom x y Gamma) (transp_term x y t) tau) as H.
  { intros Gamma t tau Hwf. induction Hwf; simpl.
    - apply WfVar. rewrite <- get_transp_dom_equivariant. assumption.
    - rewrite close_equivariant. eapply WfLet; eauto.
      rewrite <- dom_equivariant. apply notin_equivariant. assumption.
    - rewrite close_equivariant. eapply WfLam; eauto.
      rewrite <- dom_equivariant. apply notin_equivariant. assumption.
    - eapply WfApp; eauto.
    - apply WfUnit.
    - apply WfPair; auto.
    - eapply WfFst; eauto.
    - eapply WfSnd; eauto.
    - apply WfInjL; eauto.
    - apply WfInjR; eauto.
    - repeat rewrite close_equivariant. eapply WfMatch; eauto.
      + rewrite <- dom_equivariant. apply notin_equivariant. assumption.
      + rewrite <- dom_equivariant. apply notin_equivariant. assumption.
  }
  intros Gamma t tau. split; intro Hwf; auto.
  apply H in Hwf.
  rewrite transp_dom_involution in Hwf.
  rewrite transp_term_involution in Hwf.
  assumption.
Qed.

Strengthened typing jugment

Strengthened typing judgment, that universally quantifies over the variables chosen to instantiate bound names. This judgment provides a stronger induction principle, that is necessary to conduct some proofs.
Inductive wf_term_strong: env ty → term → ty → Prop :=
| WfStrongVar: ∀ Gamma x tau,
    get x Gamma = Some tau →
    wf_term_strong Gamma (Var x) tau
| WfStrongLet: ∀ S Gamma t1 t2 tau1 tau2,
    wf_term_strong Gamma t1 tau1 →
    (∀ x, x `notin` S `union` dom Gamma → wf_term_strong (x ¬ tau1 ++ Gamma) (t2 ^ x) tau2) →
    wf_term_strong Gamma (Let t1 t2) tau2
| WfStrongLam: ∀ S Gamma t tau1 tau2,
    (∀ x, x `notin` S `union` dom Gamma → wf_term_strong (x ¬ tau1 ++ Gamma) (t ^ x) tau2) →
    wf_term_strong Gamma (Lam t) (TFun tau1 tau2)
| WfStrongApp: ∀ Gamma t1 t2 tau1 tau2,
    wf_term_strong Gamma t1 (TFun tau2 tau1) →
    wf_term_strong Gamma t2 tau2 →
    wf_term_strong Gamma (App t1 t2) tau1
| WfStrongUnit: ∀ Gamma,
    wf_term_strong Gamma Unit TUnit
| WfStrongPair: ∀ Gamma t1 t2 tau1 tau2,
    wf_term_strong Gamma t1 tau1 →
    wf_term_strong Gamma t2 tau2 →
    wf_term_strong Gamma (Pair t1 t2) (TPair tau1 tau2)
| WfStrongFst: ∀ Gamma t tau1 tau2,
    wf_term_strong Gamma t (TPair tau1 tau2) →
    wf_term_strong Gamma (Fst t) tau1
| WfStrongSnd: ∀ Gamma t tau1 tau2,
    wf_term_strong Gamma t (TPair tau1 tau2) →
    wf_term_strong Gamma (Snd t) tau2
| WfStrongInjL: ∀ Gamma t tau1 tau2,
    wf_term_strong Gamma t tau1 →
    wf_term_strong Gamma (InjL t) (TSum tau1 tau2)
| WfStrongInjR: ∀ Gamma t tau1 tau2,
    wf_term_strong Gamma t tau2 →
    wf_term_strong Gamma (InjR t) (TSum tau1 tau2)
| WfStrongMatch: ∀ S Gamma t t1 t2 tau tau1 tau2,
    wf_term_strong Gamma t (TSum tau1 tau2) →
    (∀ x1 , x1 `notin` S `union` dom Gamma → wf_term_strong (x1 ¬ tau1 ++ Gamma) (t1 ^ x1) tau) →
    (∀ x2, x2 `notin` S `union` dom Gamma → wf_term_strong (x2 ¬ tau2 ++ Gamma) (t2 ^ x2) tau) →
    wf_term_strong Gamma (Match t t1 t2) tau
.

wf_term_strong is equivariant.
Lemma wf_term_strong_equivariant x y Gamma t tau:
  wf_term_strong Gamma t tau ↔ wf_term_strong (transp_dom x y Gamma) (transp_term x y t) tau.
Proof.
  revert Gamma t tau.
  assert (∀ Gamma t tau,
             wf_term_strong Gamma t tau →
             wf_term_strong (transp_dom x y Gamma) (transp_term x y t) tau) as H.
  { intros Gamma t tau Hwf. induction Hwf; simpl.
    - apply WfStrongVar. rewrite <- get_transp_dom_equivariant. assumption.
    - eapply WfStrongLet with (S := add x (add y S) `union` dom Gamma); eauto.
      intros z Hz.
      replace (z ¬ tau1) with (transp_dom x y (z ¬ tau1)) at 1;
        [| solve [simpl; rewrite transp_atom_other; simpl; auto]].
      rewrite <- transp_dom_app.
      rewrite <- (transp_term_fresh_eq x y (Var z));
        [| solve [simpl; auto] | solve [simpl;auto]].
      rewrite <- open_equivariant.
      apply H0. auto.
    - eapply WfStrongLam with (S := add x (add y S) `union` dom Gamma); eauto.
      intros z Hz.
      replace (z ¬ tau1) with (transp_dom x y (z ¬ tau1)) at 1;
        [| solve [simpl; rewrite transp_atom_other; simpl; auto]].
      rewrite <- transp_dom_app.
      rewrite <- (transp_term_fresh_eq x y (Var z));
        [| solve [simpl; auto] | solve [simpl;auto]].
      rewrite <- open_equivariant.
      apply H0. auto.
    - eapply WfStrongApp; eauto.
    - apply WfStrongUnit.
    - apply WfStrongPair; auto.
    - eapply WfStrongFst; eauto.
    - eapply WfStrongSnd; eauto.
    - apply WfStrongInjL; eauto.
    - apply WfStrongInjR; eauto.
    - eapply WfStrongMatch with (S := add x (add y S) `union` dom Gamma); eauto.
      + intros z Hz.
        replace (z ¬ tau1) with (transp_dom x y (z ¬ tau1)) at 1;
          [| solve [simpl; rewrite transp_atom_other; simpl; auto]].
        rewrite <- transp_dom_app.
        rewrite <- (transp_term_fresh_eq x y (Var z));
          [| solve [simpl; auto] | solve [simpl;auto]].
        rewrite <- open_equivariant.
        apply H0. auto.
      + intros z Hz.
        replace (z ¬ tau2) with (transp_dom x y (z ¬ tau2)) at 1;
          [| solve [simpl; rewrite transp_atom_other; simpl; auto]].
        rewrite <- transp_dom_app.
        rewrite <- (transp_term_fresh_eq x y (Var z));
          [| solve [simpl; auto] | solve [simpl;auto]].
        rewrite <- open_equivariant.
        apply H2. auto.
  }
  intros Gamma t tau. split; intro Hwf; auto.
  apply H in Hwf.
  rewrite transp_dom_involution in Hwf.
  rewrite transp_term_involution in Hwf.
  assumption.
Qed.

wf_term_strong implies wf_term.
Lemma wf_term_weaken Gamma t tau:
  wf_term_strong Gamma t tau →
  wf_term Gamma t tau.
Proof.
  intro Hwf. induction Hwf; try solve [ constructor; auto | econstructor; eauto ].
  - pick fresh x for (S `union` dom Gamma `union` fv t2).
    rewrite <- (close_open t2 x); auto. econstructor; eauto.
  - pick fresh x for (S `union` dom Gamma `union` fv t).
    rewrite <- (close_open t x); auto. constructor; auto.
  - pick fresh x1 for (S `union` dom Gamma `union` fv t1).
    rewrite <- (close_open t1 x1); auto.
    pick fresh x2 for (S `union` dom Gamma `union` fv t2).
    rewrite <- (close_open t2 x2); auto.
    econstructor; eauto.
Qed.

wf_term implies wf_term_strong.
Lemma wf_term_strengthen Gamma t tau:
  wf_term Gamma t tau →
  wf_term_strong Gamma t tau.
Proof.
  intro Hwf. induction Hwf; try solve [ constructor; auto | econstructor; eauto ].
  - apply WfStrongLet with (S := fv t2 `union` dom Gamma) (tau1 := tau1); auto.
    intros y Hy. rewrite <- subst_spec.
    rewrite <- transp_term_freshL_is_subst; auto.
    rewrite (wf_term_strong_equivariant y x) in IHHwf2.
    rewrite transp_dom_app in IHHwf2. simpl in IHHwf2.
    rewrite transp_atom_thisR in IHHwf2.
    rewrite transp_dom_fresh_eq in IHHwf2; auto.
  - apply WfStrongLam with (S := fv t `union` dom Gamma); auto.
    intros y Hy. rewrite <- subst_spec.
    rewrite <- transp_term_freshL_is_subst; auto.
    rewrite (wf_term_strong_equivariant y x) in IHHwf.
    rewrite transp_dom_app in IHHwf. simpl in IHHwf.
    rewrite transp_atom_thisR in IHHwf.
    rewrite transp_dom_fresh_eq in IHHwf; auto.
  - apply WfStrongMatch with (S := fv t1 `union` fv t2 `union` dom Gamma)
                             (tau1 := tau1) (tau2 := tau2); auto.
    + intros y Hy. rewrite <- subst_spec.
      rewrite <- transp_term_freshL_is_subst; auto.
      rewrite (wf_term_strong_equivariant y x1) in IHHwf2.
      rewrite transp_dom_app in IHHwf2. simpl in IHHwf2.
      rewrite transp_atom_thisR in IHHwf2.
      rewrite transp_dom_fresh_eq in IHHwf2; auto.
    + intros y Hy. rewrite <- subst_spec.
      rewrite <- transp_term_freshL_is_subst; auto.
      rewrite (wf_term_strong_equivariant y x2) in IHHwf3.
      rewrite transp_dom_app in IHHwf3. simpl in IHHwf3.
      rewrite transp_atom_thisR in IHHwf3.
      rewrite transp_dom_fresh_eq in IHHwf3; auto.
Qed.

Syntactic type soundness

Intermediate lemmas

Weakening lemma
Lemma wf_term_weakening Gamma1 Gamma2 t tau:
  leq_env Gamma1 Gamma2 →
  wf_term Gamma1 t tau →
  wf_term Gamma2 t tau.
Proof.
  intros Hleq Hwf. revert Gamma2 Hleq.
  apply wf_term_strengthen in Hwf.
  induction Hwf; intros; try solve [ constructor; auto | econstructor; eauto ].
  - pick fresh x for (S `union` fv t2 `union` dom Gamma2).
    rewrite <- (close_open t2 x); auto.
    econstructor; eauto. apply H0; auto using leq_env_update_stable.
    apply leq_env_dom in Hleq. fsetdec.
  - pick fresh x for (S `union` fv t `union` dom Gamma2).
    rewrite <- (close_open t x); auto.
    econstructor; eauto. apply H0; auto using leq_env_update_stable.
    apply leq_env_dom in Hleq. fsetdec.
  - pick fresh x1 for (S `union` fv t1 `union` dom Gamma2).
    rewrite <- (close_open t1 x1); auto.
    pick fresh x2 for (S `union` fv t2 `union` dom Gamma2).
    rewrite <- (close_open t2 x2); auto.
    econstructor; eauto.
    + apply H0; auto using leq_env_update_stable.
      apply leq_env_dom in Hleq. fsetdec.
    + apply H2; auto using leq_env_update_stable.
      apply leq_env_dom in Hleq. fsetdec.
Qed.

Substitution lemma.
Lemma wf_term_subst Gamma1 t1 tau1 Gamma2 x t2 tau2:
  leq_env Gamma1 (Gamma2 ++ Gamma1) →
  x `notin` dom Gamma2 →
  wf_term Gamma1 t1 tau1 →
  wf_term (Gamma2 ++ x ¬ tau1 ++ Gamma1) t2 tau2 →
  wf_term (Gamma2 ++ Gamma1) (subst t1 x t2) tau2.
Proof.
  intros Hleq Hx Hwf1 Hwf2.
  remember (Gamma2 ++ x ¬ tau1 ++ Gamma1) as Gamma.
  revert Gamma2 Hleq Hx HeqGamma.
  apply wf_term_strengthen in Hwf2.
  induction Hwf2; intros; subst; simpl;
    try solve [ constructor; auto | econstructor; eauto ].
  - destruct (x0 == x); subst.
    + assert (tau = tau1); subst.
      { assert (get x (Gamma2 ++ x ¬ tau1 ++ Gamma1) = Some tau1).
        { apply get_decompose_env. eauto. }
        congruence.
      }
      eapply wf_term_weakening; eauto.
    + constructor. case_eq (get x0 Gamma2); intros.
      × rewrite get_app_left in H; [| congruence ].
        rewrite get_app_left; congruence.
      × rewrite get_app_right in H; [ rewrite get_app_right in H |]; auto.
        simpl. destruct (x0 == x); congruence.
  - pick fresh y for (add x S `union` fv t1 `union` fv t2 `union` dom Gamma2 `union` dom Gamma1).
    rewrite <- (close_open t2 y); auto.
    rewrite subst_close;
      [| solve [eapply wf_term_lc; eauto] | solve [auto] | solve [auto] ].
    econstructor; eauto.
    rewrite <- app_assoc. apply H0; auto.
    rewrite app_assoc. transitivity (Gamma2 ++ Gamma1); [ assumption |].
    apply leq_env_update. apply get_notin_dom. auto.
  - pick fresh y for (add x S `union` fv t1 `union` fv t `union` dom Gamma2 `union` dom Gamma1).
    rewrite <- (close_open t y); auto.
    rewrite subst_close;
      [| solve [eapply wf_term_lc; eauto] | solve [auto] | solve [auto] ].
    econstructor; eauto.
    rewrite <- app_assoc. apply H0; auto.
    rewrite app_assoc. transitivity (Gamma2 ++ Gamma1); [ assumption |].
    apply leq_env_update. apply get_notin_dom. auto.
  - pick fresh y for (add x S `union` fv t0 `union` fv t1 `union` fv t2 `union` dom Gamma2 `union` dom Gamma1).
    rewrite <- (close_open t0 y); auto.
    rewrite subst_close;
      [| solve [eapply wf_term_lc; eauto] | solve [auto] | solve [auto] ].
    rewrite <- (close_open t2 y); auto.
    rewrite subst_close;
      [| solve [eapply wf_term_lc; eauto] | solve [auto] | solve [auto] ].
    econstructor; eauto.
    + rewrite <- app_assoc. apply H0; auto.
      rewrite app_assoc. transitivity (Gamma2 ++ Gamma1); [ assumption |].
      apply leq_env_update. apply get_notin_dom. auto.
    + rewrite <- app_assoc. apply H2; auto.
      rewrite app_assoc. transitivity (Gamma2 ++ Gamma1); [ assumption |].
      apply leq_env_update. apply get_notin_dom. auto.
Qed.

Preservation

step preserves wf_term.
Lemma preservation_step Gamma t1 t2 tau:
  step t1 t2 →
  wf_term Gamma t1 tau →
  wf_term Gamma t2 tau.
Proof.
  intros Hstep Hwf. revert tau Hwf.
  induction Hstep; intros;
    try solve [ inversion Hwf; subst; econstructor; eauto ].
  - inversion Hwf; subst. inversion H3; subst.
    rewrite <- subst_spec.
    eapply wf_term_subst with (Gamma2 := nil); eauto. reflexivity.
  - inversion Hwf; subst.
    rewrite <- subst_spec.
    eapply wf_term_subst with (Gamma2 := nil); eauto. reflexivity.
  - inversion Hwf; subst. inversion H3; subst. assumption.
  - inversion Hwf; subst. inversion H3; subst. assumption.
  - inversion Hwf; subst. inversion H3; subst.
    rewrite <- subst_spec.
    eapply wf_term_subst with (Gamma2 := nil); eauto. reflexivity.
  - inversion Hwf; subst. inversion H3; subst.
    rewrite <- subst_spec.
    eapply wf_term_subst with (Gamma2 := nil); eauto. reflexivity.
Qed.

steps preserves wf_term.
Lemma preservation_steps Gamma t1 t2 tau:
  steps t1 t2 →
  wf_term Gamma t1 tau →
  wf_term Gamma t2 tau.
Proof.
  intros Hsteps Hwf. induction Hsteps; eauto using preservation_step.
Qed.

eval preserves wf_term.
Lemma preservation_eval Gamma t v tau:
  eval t v →
  wf_term Gamma t tau →
  wf_term Gamma v tau.
Proof.
  intros [Hsteps Hvalue] Hwf.
  eapply preservation_steps; eauto.
Qed.

Canonicity of values

The only values of type TFun tau1 tau2 are functions.
Lemma Fun_canonical Gamma t tau1 tau2:
  is_value t →
  wf_term Gamma t (TFun tau1 tau2) →
  ∃ x t', t = Lam (close x t') ∧ wf_term (x ¬ tau1 ++ Gamma) t' tau2.
Proof.
  intros Hval Hwf.
  inversion Hwf; subst; simpl in Hval; try contradiction; try congruence.
  eauto.
Qed.

The only values of type TPair tau1 tau2 are pairs.
Lemma Pair_canonical Gamma t tau1 tau2:
  is_value t →
  wf_term Gamma t (TPair tau1 tau2) →
  ∃ t1 t2, t = Pair t1 t2 ∧ wf_term Gamma t1 tau1 ∧ wf_term Gamma t2 tau2.
Proof.
  intros Hval Hwf.
  inversion Hwf; subst; simpl in Hval; try contradiction; try congruence.
  eauto.
Qed.

The only values of type TSum tau1 tau2 are left- or right-injections.
Lemma Sum_canonical Gamma t tau1 tau2:
  is_value t →
  wf_term Gamma t (TSum tau1 tau2) →
  (∃ t1, t = InjL t1 ∧ wf_term Gamma t1 tau1)
  ∨ (∃ t2, t = InjR t2 ∧ wf_term Gamma t2 tau2).
Proof.
  intros Hval Hwf.
  inversion Hwf; subst; simpl in Hval; try contradiction; try congruence.
  - left. eauto.
  - right. eauto.
Qed.

Progress

A term that is well typed in the empty environment either is a value, or can take a step.
Lemma progress_step t tau:
  wf_term nil t tau →
  is_value t ∨ ∃ t', step t t'.
Proof.
  intro Hwf. remember nil as Gamma. induction Hwf; subst.
  - exfalso. simpl in H. discriminate.
  - right. destruct IHHwf1 as [Hvalue | [t1' Hstep]]; auto.
    + eexists. constructor; eauto.
    + ∃ (Let t1' (close x t2)). constructor; auto.
  - left. simpl. trivial.
  - right. destruct IHHwf1 as [Hvalue1 | [t1' Hstep1]]; auto.
    + destruct IHHwf2 as [Hvalue2 | [t2' Hstep2]]; auto.
      × apply Fun_canonical in Hwf1; auto.
        destruct Hwf1 as [x [t1' [Heq Hwf1]]]. subst.
        eexists. econstructor; eauto.
      × ∃ (App t1 t2'). constructor; eauto.
    + ∃ (App t1' t2). constructor; eauto.
  - left. simpl. trivial.
  - destruct IHHwf1 as [Hvalue1 | [t1' Hstep1]]; auto.
    + destruct IHHwf2 as [Hvalue2 | [t2' Hstep2]]; auto.
      × left. split; assumption.
      × right. ∃ (Pair t1 t2'). constructor; auto.
    + right. ∃ (Pair t1' t2). constructor; auto.
  - right. destruct IHHwf as [Hvalue | [t' Hstep]]; auto.
    + apply Pair_canonical in Hwf; auto.
      destruct Hwf as [t1 [t2 [Heq [Hwf1 Hwf2]]]]. subst.
      simpl in Hvalue.
      ∃ t1. constructor; tauto.
    + ∃ (Fst t'). constructor; auto.
  - right. destruct IHHwf as [Hvalue | [t' Hstep]]; auto.
    + apply Pair_canonical in Hwf; auto.
      destruct Hwf as [t1 [t2 [Heq [Hwf1 Hwf2]]]]. subst.
      simpl in Hvalue.
      ∃ t2. constructor; tauto.
    + ∃ (Snd t'). constructor; auto.
  - destruct IHHwf as [Hvalue | [t' Hstep]]; auto.
    right. ∃ (InjL t'). constructor; auto.
  - destruct IHHwf as [Hvalue | [t' Hstep]]; auto.
    right. ∃ (InjR t'). constructor; auto.
  - right. destruct IHHwf1 as [Hvalue | [t' Hstep]]; auto.
    + apply Sum_canonical in Hwf1; auto.
      destruct Hwf1 as [[t' [Heq Hwf1]] | [t' [Heq Hwf1]]]; subst; simpl in Hvalue.
      × eexists. econstructor; eauto.
      × eexists. econstructor; eauto.
    + ∃ (Match t' (close x1 t1) (close x2 t2)). constructor; auto.
Qed.

Typed relations over closed terms

RelTyped tau1 tau2 is the binary relation that relates every closed term of type tau1 with any closed term of type tau2.
Definition RelTyped tau1 tau2 : rel term term :=
  Rel _ _
      (fun t1 t2 ⇒ wf_term nil t1 tau1 ∧ wf_term nil t2 tau2).

RelTyped satisfies lc_vrel.
Lemma RelTyped_lc tau1 tau2:
  lc_vrel (RelTyped tau1 tau2).
Proof.
  intros t1 t2 [H1 H2]. split; eapply wf_term_lc; eauto.
Qed.

RelTyped satisfies closed_vrel.
Lemma RelTyped_closed tau1 tau2:
  closed_vrel (RelTyped tau1 tau2).
Proof.
  intros t1 t2 [H1 H2]. split.
  - apply wf_term_fv in H1. assumption.
  - apply wf_term_fv in H2. assumption.
Qed.

RelInv reverses the arguments of RelTyped.
Lemma RelInv_RelTyped tau1 tau2:
  RelEquiv (RelInv (RelTyped tau1 tau2)) (RelTyped tau2 tau1).
Proof.
  intros v1 v2. split; intros [H1 H2]; split; assumption.
Qed.