Termination


Require Import Omega.
Require Export Setoid Morphisms Equivalence.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Coq.Program.Equality.
Require Export ARS.
From Chapter4 Require Export sigmacalculus.

Reduction to Unified Expressions

The collapsed term type: We have pair instead of App and Cons, comp instead of Comp and Inst, no variables anymore.
This has several advantages:
  • We have less syntactic constructs, and thus also have less cases/lemmas.
  • We get rid of the mutual inductive term syntax.
Inductive uexp := zero | lam : uexp -> uexp | pair : uexp -> uexp -> uexp | comp : uexp -> uexp -> uexp.

Notation "0" := zero.
Notation "'λ' s" := (lam s) (at level 70).
Notation "⟨ s , t ⟩" := (pair s t) (at level 75).
Notation "s ∘ t" := (comp s t) (at level 70).

Translation into the unified syntax.
Fixpoint exp_uexp (s : exp) : uexp :=
  match s with
  | Zero => 0
  | App s t => ⟨exp_uexp s, exp_uexp t⟩
  | Lam s => λ (exp_uexp s)
  | Inst s sigma => comp (exp_uexp s) (subst_exp_uexp sigma)
  | var_exp n => 0
  end
with subst_exp_uexp (sigma: subst_exp) : uexp :=
 match sigma with
 | I => 0
 | Succ => 0
 | Cons s sigma => ⟨exp_uexp s, subst_exp_uexp sigma⟩
 | Comp sigma tau => (subst_exp_uexp sigma) ∘ (subst_exp_uexp tau)
 | var_subst n => 0
 end.

Distribution Rules
Reserved Notation "s ⇝__p t" (at level 80).

Inductive pstep : uexp -> uexp -> Prop :=
| uquivLambda s sigma : (λ s) ∘ sigma ⇝__p λ (s ∘ ⟨0, sigma ∘ 0⟩)
| uquivAssoc sigma tau theta : (sigma ∘ tau) ∘ theta ⇝__p sigma ∘ (tau ∘ theta)
| uquivCompPair s1 s2 t : ⟨s1, s2⟩ ∘ t ⇝__p ⟨s1 ∘ t, s2 ∘ t⟩
where "s ⇝__p t" := (pstep s t).

Projection Rules
Reserved Notation "s ⇝__s t" (at level 99).

Inductive sub : uexp -> uexp -> Prop :=
| uquivSubLam s : λ s ⇝__s s
| uquivSubPairL s t : ⟨s,t⟩ ⇝__s s
| uquivSubPairR s t : ⟨s,t⟩ ⇝__s t
| uquivSubCompL s t : s ∘ t ⇝__s s
| uquivSubCompR s t : s ∘ t ⇝__s t
where "s ⇝__s t" := (sub s t).

Closure of a relation R
Inductive closure (R : uexp -> uexp -> Prop) : uexp -> uexp -> Prop :=
| BaseClosure s t : R s t -> closure R s t
| uquivLamC s s' : closure R s s' -> closure R (λ s) (λ s')
| uquivPairL s s' t : closure R s s' -> closure R (⟨s,t⟩) (⟨s', t⟩)
| uquivPairR s t t' : closure R t t' -> closure R (⟨s,t⟩) (⟨s,t'⟩)
| uquivCompL s s' t : closure R s s' -> closure R (s ∘ t) (s' ∘ t)
| uquivCompR s t t' : closure R t t' -> closure R (s ∘ t) (s ∘ t').

Notation "s '⊃' t" := (closure sub s t) (at level 70).
Notation "s ≻ t" := (closure pstep s t) (at level 70).
Notation "sn⊃" := (sn (closure sub)).
Notation "sn≻" := (sn (closure pstep)).

Reserved Notation "s ≡ t" (at level 80).
Notation "s ≡ t" := (Or (closure sub) (closure pstep) s t).
Notation "s ≡+ t" := (plus (Or (closure sub) (closure pstep)) s t) (at level 70).

Notation "'sn≡'" := (sn (Or (closure sub) (closure pstep))) (at level 1).

Hint Constructors pstep closure sub.

Congruence for unified reduction
Lemma congr_lam s t : s ≡ t -> λ s ≡ λ t.
Proof. inversion 1; eauto. Qed.

Lemma congr_compL s s' t : s ≡ s' -> s ∘ t ≡ s' ∘ t.
Proof. inversion 1; eauto. Qed.

Lemma congr_compR s t t' : t ≡ t' -> s ∘ t ≡ s ∘ t'.
Proof. inversion 1; eauto. Qed.

Lemma congr_pairL s s' t : s ≡ s' -> ⟨s,t⟩ ≡ ⟨s',t⟩.
Proof. inversion 1; eauto. Qed.

Lemma congr_pairR s t t' : t ≡ t' -> ⟨s,t⟩ ≡ ⟨s,t'⟩.
Proof. inversion 1; eauto. Qed.

Hint Resolve congr_lam congr_compL congr_compR congr_pairL congr_pairR .

Notation "s ≡* t" := (star (Or (closure sub) (closure pstep)) s t) (at level 80).

Lemma uquiv_star_lam s t:
  s ≡* t -> λ s ≡* λ t.
Proof. induction 1; eauto. Qed.

Lemma uquiv_star_pairL s s' t:
  s ≡* s' -> ⟨s,t⟩ ≡* ⟨s', t⟩.
Proof. induction 1; eauto. Qed.

Lemma uquiv_star_pairR s t t':
  t ≡* t' -> ⟨s, t⟩ ≡* ⟨s, t'⟩.
Proof. induction 1; eauto. Qed.

Lemma uquiv_star_compL s s' t:
  s ≡* s' -> s ∘ t ≡* s' ∘ t.
Proof. induction 1; eauto. Qed.

Lemma uquiv_star_compR s t t':
  t ≡* t' -> s ∘ t ≡* s ∘ t'.
Proof. induction 1; eauto. Qed.

Hint Resolve uquiv_star_lam uquiv_star_pairL uquiv_star_pairR uquiv_star_compL uquiv_star_compR.

Lemma uquiv_plus_lam s t:
  s ≡+ t -> λ s ≡+ λ t.
Proof. induction 1; eauto. Qed.

Lemma uquiv_plus_pairL s s' t:
  s ≡+ s' -> ⟨s,t⟩ ≡+ ⟨s', t⟩.
Proof. induction 1; eauto. Qed.

Lemma uquiv_plus_pairR s t t':
  t ≡+ t' -> ⟨s, t⟩ ≡+ ⟨s, t'⟩.
Proof. induction 1; eauto. Qed.

Lemma uquiv_plus_compL s s' t:
  s ≡+ s' -> (s ∘ t) ≡+ (s' ∘ t).
Proof. induction 1; eauto. Qed.

Lemma uquiv_plus_compR s t t':
  t ≡+ t' -> (s ∘ t) ≡+ (s ∘ t').
Proof. induction 1; eauto. Qed.

Hint Resolve uquiv_plus_lam uquiv_plus_pairL uquiv_plus_pairR uquiv_plus_compL uquiv_plus_compR.

Steps in the orignal system can be simulated in our unified system.
Lemma equiv_uquiv :
  (forall s t, equiv_axiom s t -> exp_uexp s ≡+ exp_uexp t) /\ (forall sigma tau, equiv_axiom_subst sigma tau -> subst_exp_uexp sigma ≡+ subst_exp_uexp tau).
Proof.
  apply comb_equiv_ind; cbn; intros; eauto 20.
Qed.

Lemma sn_uquiv_equiv s :
  sn≡ (exp_uexp s) -> sn equiv_axiom s.
Proof.
  intros H%sn_plus. revert H.
  apply sn_morphism. unfold morphism. apply equiv_uquiv.
Qed.

Lemma sn_uquiv_equiv_subst sigma :
  sn≡ (subst_exp_uexp sigma) -> sn equiv_axiom_subst sigma.
Proof.
  intros H%sn_plus. revert H.
  apply sn_morphism. unfold morphism. apply equiv_uquiv.
Qed.

Reduction to Distribution Termination

Every term is strong normalizing w.r.t. projection
Lemma sn_sub_lam s :
  sn⊃ s -> sn⊃ (λ s).
Proof.
  induction 1 as [s H IH]. constructor. intros s' H'.
  inv H'; eauto. inv H0; eauto.
Qed.

Lemma sn_sub_pair s t :
  sn⊃ s -> sn⊃ t -> sn⊃ (⟨s,t⟩).
Proof.
  intros H. revert t. induction H as [s H IH].
  intros t H'. induction H' as [t H' IH'].
  constructor. intros u A. inv A; eauto. inv H0; eauto.
Qed.

Lemma sn_sub_comp s t :
  sn⊃ s -> sn⊃ t -> sn⊃ (s ∘ t).
Proof.
  intros H. revert t. induction H as [s H IH].
  intros t H'. induction H' as [t H' IH'].
  constructor. intros u A. inv A; eauto. inv H0; eauto.
Qed.

Lemma sn_sub s :
  sn⊃ s.
Proof.
  induction s; eauto using sn_sub_lam, sn_sub_pair, sn_sub_comp.
  constructor; intros; inv H; inv H0.
Qed.

Hint Resolve sn_sub.
Exchangeability.
Lemma exchangeability s s__i t__i:
  s ⊃ s__i -> s__i ≻ t__i -> exists t, s ≻ t /\ t ≡* t__i.
Proof with (eauto 20).
  intros H. revert t__i.
  induction H; intros; eauto.
  - inv H...
  - inv H0. inv H1.
    destruct (IHclosure _ H2) as (?&?&?)...
  - inv H0...
    + inv H1.
    + destruct (IHclosure _ H4) as (?&?&?)...
  - inv H0...
    + inv H1.
    + destruct (IHclosure _ H4) as (?&?&?)...
 - inv H0...
    + inv H1... all: inv H... all: inv H0...
    + destruct (IHclosure _ H4) as (?&?&?)...
  - inv H0...
    + inv H1...
    + destruct (IHclosure _ H4) as (?&?&?)...
Qed.

Strong Normalization of the distribution rules implies strong normalisation of projection and distribution.
Lemma sn_uquiv_red s :
  sn≻ s -> sn≡ s.
Proof.
  induction 1 as [s _ IH_s].
  assert (sn⊃ s) as H by eauto.
  induction H as [s sn_sub_s IH_sub_s].
  constructor. intros s' H.
  destruct H as [s s' H|s s' H]; eauto.
  apply IH_sub_s; eauto.
   - intros.
    destruct (exchangeability H H0) as (t&?&?).
    specialize (IH_s _ H1). inversion IH_s. eauto using sn_forward_star.
Qed.

Corollary sn_uquiv_red_eq s :
  sn≻ s <-> sn≡ s.
Proof.
  split; intros H.
  - now eapply sn_uquiv_red.
  - now eapply sn_orR in H.
Qed.

Termination of the Distribution Calculus

Forward Strong Normalisation Lemmas for zero, lam, and pair.
Fact sn_zero : sn≡ 0.
Proof. constructor. intros x' H. inv H. inv H0; inv H; inv H0. inv H0. inv H. Qed.

Fact sn_lam s: sn≡ s -> sn≡ (λ s).
Proof.
  intros H. depind H. constructor. intros s'' H'.
  inv H'.
  - inv H1; eauto. inv H2; eauto.
  - inv H1; eauto. inv H2.
Qed.

Fact sn_pair s: sn≡ s -> forall t, sn≡ t -> sn≡ (⟨s,t⟩).
Proof.
  intros H. depind H. intros t H_t. depind H_t.
  constructor. intros s' A. inv A.
  - inv H3; eauto.
    inv H4; eauto.
  - inv H3; eauto. now constructor.
Qed.

Hint Resolve sn_zero sn_lam sn_pair.

Fact sn_zero' : sn≻ 0.
Proof. constructor. intros x' H. inv H. inv H0; inv H; inv H0. Qed.

Fact sn_CLam s: sn≻ (λ s) -> sn≻ s.
Proof. eapply sn_morphism; eauto. Qed.

Fact sn_pairL' s t : sn≻ (⟨s,t⟩) -> sn≻ s.
Proof. eapply sn_morphism with (h := fun x => pair x t); eauto. Qed.

Fact sn_pairR' s t : sn≻ (⟨s,t⟩) -> sn≻ t.
Proof. eapply sn_morphism with (h := fun x => pair s x); eauto. Qed.

Fact sn_CCompL' s t : sn≻ (comp s t) -> sn≻ s.
Proof. eapply sn_morphism with (h := fun x => comp x t); eauto. Qed.

Fact sn_CCompR' s t : sn≻ (comp s t) -> sn≻ t.
Proof. eapply sn_morphism with (h := fun x => comp s x); eauto. Qed.

Fact sn_pair' s: sn≻ s -> forall t, sn≻ t -> sn≻ (⟨s,t⟩).
Proof.
  intros H. depind H. intros t H_t. depind H_t.
  constructor. intros s' A. inv A.
  - inv H3; eauto.
  - eauto.
  - eauto.
Qed.

Hint Resolve sn_zero' sn_CLam sn_CCompL' sn_CCompR' sn_pair'.

Renaming Epxressions

Inductive RenExp : uexp -> Prop :=
| ZeroRen : RenExp 0
| PairRen s xi : RenExp s -> RenExp xi -> RenExp (⟨s, xi⟩)
| CompRen xi zeta : RenExp xi -> RenExp zeta -> RenExp (xi ∘ zeta).

Hint Constructors RenExp.

Lemma ren_preserve s t :
  RenExp s -> s ≡ t -> RenExp t.
Proof.
  intros A H. destruct H; intros; eauto.
  - induction H; try now (inv A; eauto).
    + inv H; inv A; eauto; inv H2; eauto.
  - induction H; try now (inv A; eauto).
    + inv H; inv A; inv H1; eauto.
Qed.

Hint Resolve ren_preserve.

The more general version is useful, as we have included that we have the IH for smaller terms.
Lemma ren_sn s :
  RenExp s -> sn≡ s.
Proof with eauto.
  induction 1 as [ | |xi zeta H1 IH1 H2 IH2]; eauto.
  revert zeta H1 H2 IH2. induction IH1 as [xi IH1 IH1_sn]; intros.
  induction IH2 as [zeta IH2 IH2_sn]; eauto.
  constructor. intros theta H.
  inv H; eauto.
  - inv H0; eauto.
    inv H; eauto.
  - inv H0; eauto.
    inv H; eauto.
      * inv H1.
      * eapply IH1_sn; eauto. eapply IH1_sn; eauto.
      * eapply sn_pair; eapply IH1_sn; eauto.
Qed.

Contexts and patterns

Definition of contexts.
Inductive ctx :=
| Hole : ctx
| CZero
| CLam : ctx -> ctx
| CPair : ctx -> ctx -> ctx
| CCompL : uexp -> ctx -> ctx
| CCompR : ctx -> forall xi, RenExp xi -> ctx.

Patterns: Can fill a context.
Inductive pat :=
| Term : uexp -> pat
| Singleton : pat -> pat
| Pair : pat -> pat -> pat.

Renaming Patterns
Inductive Ren : pat -> Prop :=
| RenTerm s: RenExp s -> Ren (Term s)
| SingletonRen p : Ren p -> Ren (Singleton p)
| PairRenaming p q : Ren p -> Ren q -> Ren (Pair p q).

Hint Constructors Ren.

Filling the holes of a context.
Fixpoint fill (s: ctx) (p: pat) : option uexp :=
  match s, p with
  | Hole, Term s => Some s
  | CZero, _ => Some 0
  | CPair s t, Pair p1 p2 => match fill s p1, fill t p2 with
                           | Some s', Some t' => Some (⟨s', t'⟩)
                           | _, _ => None
                           end
  | CLam s, Singleton p => option_map lam (fill s p)
  | CCompL s t, Singleton p => option_map (comp s) (fill t p)
  | @CCompR s t _, Singleton p => option_map (fun s => s ∘ t) (fill s p)
  | _, _ => None
  end.

Composition of two patterns
Inductive compRel : pat -> pat -> pat -> Prop :=
 | compRelTerm s xi : compRel (Term s) (Term xi) (Term (comp s xi))
 | compRelSingleton p1 p2 p3 : compRel p1 p2 p3 -> compRel (Singleton p1) (Singleton p2) (Singleton p3)
 | compRelPair p1 p2 p3 q1 q2 q3 : compRel p1 p2 p3 -> compRel q1 q2 q3 -> compRel (Pair p1 q1) (Pair p2 q2) (Pair p3 q3).

Hint Constructors compRel.

Splitting

Inductive split : pat -> pat -> Prop :=
| patSplitApp s t: split (Term (⟨s,t⟩)) (Pair (Term s) (Term t))
| patSplitLambda s : split (Term (λ s)) (Singleton (Term s))
| patSplitComp sigma tau : split (Term (sigma ∘ tau)) (Singleton (Term tau))

| patSingleton p p' : split p p' -> split (Singleton p) (Singleton p')
| patPairL p p' q : split p p' -> split (Pair p q) (Pair p' q)
| patPairR p q q' : split q q' -> split (Pair p q) (Pair p q').

Hint Constructors split.

Notation "'sn__split'" := (sn split) (at level 2).

Lemma sn_split_singleton p :
  sn__split p -> sn__split (Singleton p).
Proof.
  intros H. depind H. constructor. intros p'' H'.
  inv H'. eauto.
Qed.

Lemma sn_split_pair p q :
  sn__split p -> sn__split q -> sn__split (Pair p q).
Proof.
  intros H. revert q. induction H. intros.
  induction H1.
  constructor. intros. inv H3; eauto.
Qed.

Lemma sn_split_term s :
  sn__split (Term s).
Proof.
  induction s.
  1-3: try now (constructor; intros; inv H; inv H0).
  - constructor. intros. inv H.
    eapply sn_split_singleton; eauto.
  - constructor. intros. inv H.
    eapply sn_split_pair; eauto.
  - constructor. intros. inv H.
    eapply sn_split_singleton; eauto.
Qed.

Lemma sn_split p :
  sn__split p.
Proof.
  induction p; eauto using sn_split_singleton, sn_split_pair, sn_split_term.
Qed.

Hint Resolve sn_split.

Reduction for Patterns

Reduction in the leaves only.
Inductive leaf_step : pat -> pat -> Prop :=
| leafTermStep s s': s ≡ s' -> leaf_step (Term s) (Term s')
| leafSingleton p p' : leaf_step p p' -> leaf_step (Singleton p) (Singleton p')
| leafPairL p p' q: leaf_step p p' -> leaf_step (Pair p q) (Pair p' q)
| leafPairR p q q' : leaf_step q q' -> leaf_step (Pair p q) (Pair p q').
Hint Constructors leaf_step.

Notation "'sn__leaf'" := (sn leaf_step) (at level 2).

Lemma sn_leaf_Term s:
  sn≡ s -> sn__leaf (Term s).
Proof.
  induction 1 as [s H IH].
  constructor. intros s' H'.
  inv H'. eauto.
Qed.

Lemma sn_leaf_Singleton p :
  sn__leaf p -> sn__leaf (Singleton p).
Proof.
  induction 1 as [p H IH].
  constructor. intros p' H'.
  inv H'. eauto.
Qed.

Lemma sn_leaf_pair p q :
  sn__leaf p -> sn__leaf q -> sn__leaf (Pair p q).
Proof.
  intros H. revert q.
  induction H as [p H IH]. intros p' H'.
  induction H' as [p' H' IH']. constructor. intros u H''. inv H''; eauto.
Qed.

Lemma sn_leaf_Ren p:
  Ren p -> sn__leaf p.
Proof.
  intros H. induction H; eauto using sn_leaf_Term, sn_leaf_Singleton, sn_leaf_pair.
  now apply sn_leaf_Term, ren_sn.
Qed.

Hint Resolve sn_leaf_Ren.

Automation
Ltac saturate := repeat (progress (
 match goal with
 | [ H: Ren (Term _) |- _] => inv H
 | [ H : Ren (Singleton _) |- _] => inv H
 | [ H : Ren (Pair _ _) |- _] => inv H
 | [ H: forall x, plus equiv_axiom ?s x -> sn≡ x |- _] => extend (SNI H)
 | [ H: forall x, plus split ?s x -> sn__split x |- _] => extend (SNI H)
 | [ H: forall x, plus leaf_step ?s x -> sn__leaf x |- _] => extend (SNI H)
 | [ H : equiv_axiom Zero ?s |- _] => inv H
 | [ H : equiv_axiom (var_exp ?n) ?s |- _] => inv H
 | [ H : equiv_axiom I ?s |- _] => inv H
 | [ H : equiv_axiom Succ ?s |- _] => inv H
 | [ H : equiv_axiom (var_subst ?n) ?s |- _] => inv H
 | [ H: zero ≻ ?s |- _] => inv H
 | [ H : zero ⇝__p ?s |- _] => inv H
 end)).

Ltac autofill := simpl;
                 repeat (match goal with [H : fill ?e ?u = ?s |- context[fill ?e ?u]] => rewrite H
                                     | [H : ?s = fill ?e ?u |- context[fill ?e ?u]] => rewrite <- H
                  end); reflexivity.

Ltac auto_destruct :=
                  lazymatch goal with
                  | [H : option_map _ (fill ?C ?u) = _ |- _] => destruct (fill C u) eqn:?; inv H
                  | [H : match (fill ?C ?u) with |Some s => _ | None => _ end = ?t |- _] => destruct (fill C u) eqn:?; inv H
                  | [H : match ?u with |Singleton s => _ | _ => _ end = ?t |- _] => destruct u eqn:?; inv H
                                                                                                        | [H : fill Hole ?s = _ |- _] => inv H
                  end.

Preservation

Lemma preservation :
  forall s, sn≻ s -> forall (p__s : pat), forall (p__xi : pat), Ren p__xi
      -> forall p__t, compRel p__s p__xi p__t -> forall C, fill C p__s = Some s -> forall t, Some t = fill C p__t -> sn≻ t.
Proof with (do 2 try (split; [now (saturate; eauto 6; try autofill) |]); saturate; eauto; try autofill).
  intros s sn__s.
  rewrite sn_uquiv_red_eq in sn__s. induction sn__s as [s H IH__s].
  assert (sn__s: sn≻ s) by (eapply sn_uquiv_red_eq; eauto); clear H.
  intros p__s. assert (H : sn__split p__s) by eauto. induction H as [p__s H IH__ps].
  assert (sn__ps : sn__split p__s) by eauto; clear H.
  intros p__xi Ren__xi.
  assert (sn__leaf p__xi) as sn__xi by eauto. revert Ren__xi.
  induction sn__xi as [p__xi _ IH__xi]. intros Ren__xi p__t comp C H1 t H2.
  constructor. intros t' A.
  enough ((exists s', s ≡ s' /\ exists C p__s', fill C p__s' = Some s' /\ exists p__xi, Ren p__xi /\ exists p__t', compRel p__s' p__xi p__t' /\ Some t' = fill C p__t')
          \/ (exists p__s', split p__s p__s' /\ exists p__xi, Ren p__xi /\ exists C, fill C p__s' = Some s /\ exists p__t', compRel p__s' p__xi p__t' /\ Some t' = fill C p__t')
          \/ (exists p__xi', leaf_step p__xi p__xi' /\ Ren p__xi' /\ exists p__t', compRel p__s p__xi' p__t' /\ Some t' = fill C p__t') )as [(?&?&?&?&?&?&?&?&?&?)|[(?&?&?&?&?&?&?&?&?)|(?&?&?&?&?&?)]].
  - eapply IH__s...
  - eapply IH__ps...
  - eapply IH__xi...
  - clear IH__s IH__ps IH__xi. revert t t' A s sn__s H1 H2.
    revert p__s sn__ps p__xi Ren__xi p__t comp. induction C; intros.
    +
Empty Context
      cbn in *; repeat auto_destruct. inv comp0; inv H2.
      inversion A as [| | | | | ? ? xi']; subst...
     *
Primitive step of the context. In each case we get smaller with splitting.
       right. left. inversion H as [s' |s1 s2|s1 s2]; subst.
       -- exists (Singleton (Term s'))...
          exists (Singleton (Term (pair 0 (comp xi 0))))...
          exists (CLam Hole)...
       -- exists (Singleton (Term s2))...
          exists (Singleton (Term xi))...
          exists (CCompL s1 Hole)...
       -- exists (Pair (Term s1) (Term s2))...
          exists (Pair (Term xi) (Term xi))...
          exists (CPair Hole Hole)...
     *
Step in the left part of composition.
        left. exists s'...
        exists Hole. exists (Term s')...
        exists (Term xi)...
     *
Step in the right part of composition.
       right. right.
       exists (Term xi')...
    +
Context for CZero
      cbn in *. inv H2. inv A. inv H.
    +
Context for lambda.
      cbn in *; symmetry in H2; repeat auto_destruct.
      inv A. inv H. inv comp0.
      rename p2 into p__xi. rename p0 into p__s. rename p into p__t. rename u into t. rename u0 into s. rename s' into t'.
      edestruct IHC with (p__s := p__s) (p__xi := p__xi) (s := s) (t := t) (t' := t') as [(s'&?&C'&p__s''&?&p__xi'&?&?&?&?)|[(p__s'&?&p__xi'&?&C'&?&?&?&?)|(p__xi'&?&?&?&?&?)]]...
           ** left. exists (λ s')...
              exists (CLam C'). exists (Singleton p__s'')...
             exists (Singleton p__xi')... eexists...
           ** right. left.
             exists (Singleton p__s')...
             exists (Singleton p__xi')... exists (CLam C')...
             eexists...
           ** right. right.
              exists (Singleton p__xi')... eexists...
    +
Context for pairs.
      cbn in H1, H2; symmetry in H2. repeat auto_destruct.
      inv comp0. rename u into t1. rename u0 into t2. rename u1 into s1. rename u2 into s2.
      rename p1 into p__t1. rename p2 into p__t2. rename p3 into p__s1. rename p4 into p__s2.
      rename p5 into xi__1. rename q2 into xi__2.
      inv A.
      * inv H.
      * rename s' into t1'.
        edestruct IHC1 with (p__s := p__s1) (p__xi := xi__1) (s := s1) (t := t1) (t' := t1') as [(s1'&?&C1'&p__s1'&?&xi__1'&?&?&?&?)|[(p__s1'&?&xi__1'&?&C1'&?&?&?&?)|(xi__1'&?&?&?&?&?)]]...
        -- eapply sn_pairL'; eauto.
        -- left. exists (pair s1' s2)...
           exists (CPair C1' C2).
           exists (Pair p__s1' p__s2)...
           exists (Pair xi__1' xi__2). split...
           eexists...
        -- right. left. exists (Pair p__s1' p__s2)...
           exists (Pair xi__1' xi__2)...
           exists (CPair C1' C2)...
           eexists...
        -- right. right.
           exists (Pair xi__1' xi__2)...
           eexists...
      * rename t'0 into t2'.
        edestruct IHC2 with (p__s := p__s2) (p__xi := xi__2) (s := s2) (t := t2) (t' := t2') as [(s2'&?&C2'&p__s2'&?&xi__2'&?&?&?&?)|[(p__s2'&?&xi__2'&?&C2'&?&?&?&?)|(xi__2'&?&?&?&?&?)]]...
        -- eapply sn_pairR'; eauto.
        -- left. exists (pair s1 s2')...
           exists (CPair C1 C2').
           exists (Pair p__s1 p__s2')...
           exists (Pair xi__1 xi__2'). split...
           eexists...
        -- right. left. exists (Pair p__s1 p__s2')...
           exists (Pair xi__1 xi__2')...
           exists (CPair C1 C2')...
           eexists...
        -- right. right.
           exists (Pair xi__1 xi__2')...
           eexists...
    +
Context for compositions with hole on the right side.
      cbn in H1, H2; symmetry in H2; repeat auto_destruct.
      rename u0 into t. rename u1 into s. rename p into p__t. rename p0 into p__s.
      inv comp0. rename p2 into p__xi.
      inv A.
      * left. inversion H as [u_|u1 u2|u1 u2].
        -- exists (λ (comp u_ (pair zero (comp s 0))))...
           assert (RenSucc: RenExp 0) by eauto.
           exists (CLam (CCompL u_ (CPair CZero (CCompR C RenSucc)))).
           exists (Singleton (Singleton (Pair (Term zero) (Singleton p__s))))...
           exists (Singleton (Singleton (Pair (Term zero) (Singleton p__xi))))...
           eexists...
        -- exists (comp u1 (comp u2 s))...
           exists (CCompL u1 (CCompL u2 C))...
           exists (Singleton (Singleton p__s))...
           exists (Singleton (Singleton p__xi))...
           eexists...
        -- exists (pair (comp u1 s) (comp u2 s))...
           exists (CPair (CCompL u1 C) (CCompL u2 C)).
           exists (Pair (Singleton p__s) (Singleton p__s))...
           exists (Pair (Singleton p__xi) (Singleton p__xi))...
           eexists...
      * rename s' into u'.
        left. exists (u' ∘ s)...
        exists (CCompL u' C). exists (Singleton p__s)...
        exists (Singleton p__xi)... eexists...
      * rename t'0 into t'.
        edestruct IHC with (p__s := p__s) (p__xi := p__xi) (s := s) (t := t) (t' := t') as [(s'&?&C'&p__s''&?&p__xi'&?&?&?&?)|[(p__s'&?&p__xi'&?&C'&?&?&?&?)|(p__xi'&?&?&?&?&?)]]...
        -- left. eexists (comp u s')...
           exists (CCompL u C'). exists (Singleton p__s'')...
           exists (Singleton p__xi')... eexists...
        -- right. left. eexists (Singleton p__s')...
           exists (Singleton p__xi')... exists (CCompL u C')...
           eexists...
        -- right. right. exists (Singleton p__xi')...
           eexists...
    +
Context for compositions with hole on the left side.
      cbn in H1, H2; symmetry in H2; repeat auto_destruct.
      rename u0 into s. rename u into t. rename p into p__t. rename p0 into p__s.
      inv comp0. rename p2 into p__xi. inv A.
      * left. inv H.
        -- destruct C; inv Heqo0; inv Heqo; repeat auto_destruct.
           ++ inv H2.
           ++ exists (λ (comp u (pair zero (comp xi 0))))...
             assert (RenExp (pair zero (comp xi 0))) by eauto .
             exists (CLam (CCompR C H)).
             exists (Singleton (Singleton p0))...
             exists (Singleton p__xi)...
             eexists...
         -- destruct C; inv Heqo0; inv Heqo; repeat auto_destruct.
            ++ inv H2. rename tau into zeta. exists sigma...
                 exists Hole. exists (Term sigma)...
                 exists (Term (comp zeta xi))...
            ++ exists (comp sigma (comp u xi))...
                 exists (CCompL sigma (CCompR C r)). exists (Singleton (Singleton p0))...
                  exists (Singleton p__xi)... eexists...
            ++ exists (comp u (comp tau xi))...
                 exists (CCompR C (CompRen r0 r)).
                 exists (Singleton p0)...
                 exists p__xi... eexists...
         -- destruct C; inv Heqo; repeat auto_destruct.
             ** inv H2.
             ** simpl in Heqo0. repeat auto_destruct.
                exists (pair (comp u xi) (comp u0 xi))...
             exists (CPair (CCompR C1 r) (CCompR C2 r)).
             exists (Pair (Singleton p3) (Singleton p4))...
             inv H2. exists (Pair (Singleton p5) (Singleton q2))...
             eexists...
      * rename s' into t'.
        edestruct IHC with (p__s := p__s) (p__xi := p__xi) (s := s) (t := t) (t' := t') as [(s'&?&C'&p__s''&?&p__xi'&?&?&?&?)|[(p__s'&?&p__xi'&?&C'&?&?&?&?)|(p__xi'&?&?&?&?&?)]]...
        -- left. eexists (comp s' xi)...
           exists (CCompR C' r). exists (Singleton p__s'')...
           exists (Singleton p__xi')... eexists...
        -- right. left. eexists (Singleton p__s')...
           exists (Singleton p__xi')... exists (CCompR C' r)...
           eexists...
        -- right. right. exists (Singleton p__xi')...
           eexists...
      * rename t'0 into xi'. left. exists (s ∘ xi')...
        assert (RenExp xi') as r'...
        eexists (CCompR C r'). exists (Singleton p__s)...
        exists (Singleton p__xi)... eexists...
Qed.

Shifting for reductions.
Lemma sn_pstep_shift s :
  sn≻ s -> sn≻ (s ∘ 0).
Proof.
  intros H.
  apply preservation with (s := s) (p__s := Term s) (p__xi := Term 0) (C := Hole) (p__t := Term (s ∘ 0)); eauto.
Qed.

Shifting for the whole system follows.
Lemma sn_uexp_shift sigma :
  sn≡ sigma -> sn≡ (sigma ∘ 0).
Proof.
  rewrite <- !sn_uquiv_red_eq. eapply sn_pstep_shift.
Qed.

Termination


Lemma sn_uexp_comp s:
  sn≡ s -> forall t, sn≡ t -> sn≡ (s ∘ t).
Proof with (saturate; eauto).
  induction 1 as [s H IH].
  induction 1 as [t H' IH'].
  constructor. intros u H''. inv H''.
  - inv H0; eauto.
    inv H1; eauto.
  - inv H0; eauto.
    inv H1; eauto 8.
    eapply sn_lam.
    eapply IH...
    eapply sn_pair... eapply sn_uexp_shift...
Qed.

Lemma sn_uexp s:
  sn≡ s.
Proof. induction s; eauto using sn_uexp_comp. Qed.

Lemma sn_exp s :
  sn equiv_axiom s.
Proof. apply sn_uquiv_equiv, sn_uexp. Qed.

Lemma sn_subst sigma :
  sn equiv_axiom_subst sigma.
Proof. apply sn_uquiv_equiv_subst, sn_uexp. Qed.