From Chapter9 Require Export reduction.

Lemma sn_mstep {n} (s t : tm n):
  star step s t -> sn step s -> sn step t.
Proof.
  eauto using sn_forward_star.
Qed.

Inductive SN : forall {n}, tm n -> Prop :=
| SNeu n (M: tm n): SNe M -> SN M
| SAbs n A (M: tm (S n)) : SN M -> SN (lam A M)
| SRed n (M M': tm n): SNRed M M' -> SN M' -> SN M
with SNe : forall {n}, tm n -> Prop :=
| SVar n (x: fin n) : SNe (ids x)
| SApp n (R: tm n) M : SNe R -> SN M -> SNe (app R M)
with SNRed : forall {n}, tm n -> tm n -> Prop :=
| SBeta n A (M : tm (S n)) N M': SN N -> M' = M[N..] -> SNRed (app (lam A M) N) M'
| SAppl n (R R': tm n) M : SNRed R R' -> SNRed (app R M) (app R' M).

Scheme SN_ind_2 := Minimality for SN Sort Prop
                   with SNe_ind_2 := Minimality for SNe Sort Prop
                    with redSN_ind_2 := Minimality for SNRed Sort Prop.
Combined Scheme SN_multind from SN_ind_2, SNe_ind_2, redSN_ind_2.

Lemma sn_appL {n} (s : tm n) (t : tm n) :
  sn step (app s t) -> sn step s.
Proof. apply (@sn_morphism _ _ _ _ (fun s => app s t)); eauto using @step. Qed.

Lemma sn_subst_tm {m n} (f : fin m -> tm n) (s : tm m) :
  sn step (subst_tm f s) -> sn step s.
Proof. apply sn_morphism. eauto using step_inst. Qed.

Lemma closed_lam {n} (s : tm (S n)) A:
  sn step s -> sn step (lam A s).
Proof.
  induction 1 as [M H IH]. constructor. intros M' C. inv C. auto.
Qed.

Lemma closed_appR n (M: tm n) (N: tm n) :
  sn step (app M N) -> sn step N.
Proof. eapply sn_morphism. eauto. Qed.

Set Implicit Arguments.
Unset Strict Implicit.

Inductive redsn : forall n, tm n -> tm n -> Prop :=
 | redsn_beta n A (M: tm (S n)) (N: tm n) : sn step N -> redsn (app (lam A M) N) (subst_tm (N.:ids) M)
 | redsn_app n (R R' : tm n) (M : tm n) : redsn R R' -> redsn (app R M) (app R' M).

Lemma fundamental_backwards n (M: tm (S n)) (N: tm n) A:
   sn step N -> sn step (subst_tm (N.: ids) M) -> sn step (app (lam A M) N).
Proof.
  intros sn_N sn_M'.
  assert (H: sn step M) by (now apply sn_subst_tm in sn_M').
  revert M H sn_M'. induction sn_N as [N sn_N IH_N].
  induction 1 as [M sn_M IH_M]. intros H. constructor. intros M' C. inv C.
  - constructor. intros M' H'. inv H. now apply H.
  - inv C. rename b2 into M'. eapply IH_M. assumption.
    eauto using sn_mstep, mstep_beta.
  - eapply IH_N; eauto.
    + eauto using sn_mstep, mstep_beta.
Qed.

Fixpoint neutral n (M: tm n) :=
  match M with
  | var_tm x => True
  | app s t => neutral s
  | _ => False
  end.

Lemma neutral_preservation n (M N: tm n):
  neutral M -> step M N -> neutral N.
Proof. intros H. induction 1; simpl in *; intuition. Qed.

Lemma sn_confluence n (M: tm n):
  forall M' M'', redsn M M' -> step M M'' -> M' = M'' \/ exists M''', redsn M'' M''' /\ star step M' M'''.
Proof.
  induction M as [x | T M IHM | M1 IHM1 M2 IHM2]; intros M' M'' D E; inv D; inv E.
  - now left.
  - inv E. right. eexists. split.
    + now constructor.
    + apply mstep_inst. eauto.
  - right. eexists. split. econstructor. inv H; eauto. apply mstep_beta; eauto.
  - inv D.
  - destruct (IHM _ _ D E) as [IH|(M''&IH1&IH2)].
    + subst. now left.
    + right. eexists. split.
      * econstructor. eassumption.
      * eapply mstep_app. assumption. constructor.
  - right. eexists. split.
    + constructor. eassumption.
    + eapply mstep_app. constructor. eauto.
Qed.

Lemma redsn_backwards n (M M': tm n):
 redsn M M' -> sn step M' -> sn step M.
Proof.
 induction 1 as [|n M M' N H IH].
 - intros D. eapply fundamental_backwards; eauto.
 - intros D. specialize (IH (sn_appL _ _ D)).
   assert (sn_N: sn step N) by (now apply closed_appR in D).
   revert M IH M' D H. induction sn_N as [N sn_N IH_N]. induction 1 as [M sn_M IH_M].
   constructor. intros M_N C. inv C.
   + inv H.
   + destruct (sn_confluence H C) as [E|(M'''&C1&C2)].
     * now subst.
     * eapply IH_M with (M' := M'''); eauto.
       eapply sn_mstep; [|eassumption]. eapply mstep_app; eauto.
   + eapply IH_N; eauto.
     * inv D. apply H. now constructor.
Qed.

Lemma sn_app_neutral n (N : tm n) :
   sn step N -> forall (M: tm n), neutral M -> sn step M -> sn step (app M N).
Proof.
  induction 1 as [N sn_N IH_N].
  induction 2 as [M sn_M IH_M].
  constructor. intros M' C. inv C.
  - contradiction.
  - eauto using neutral_preservation.
  - eauto using sn.
Qed.

Lemma SN_sn :
  (forall n (M: tm n), SN M -> sn step M)
/\ (forall n (M: tm n), SNe M -> sn step M /\ neutral M)
/\ (forall n (M: tm n) M', SNRed M M' -> redsn M M') .
Proof.
  apply SN_multind; intros.
  - intuition.
  - now apply closed_lam.
  - eauto using redsn_backwards.
  - split; [|now constructor].
    + constructor. intros M H. inv H.
  - split; [|intuition].
    + now apply sn_app_neutral.
  - subst. now constructor.
  - now constructor.
Qed.

Ltac invTm :=
match goal with
|[_ : var_tm _ = ren_tm ?R ?M' |- _] => inv M'; simpl in *; try congruence
|[_ : lam _ _ = ren_tm ?R ?M' |- _] => inv M'; simpl in *; try congruence
|[_ : app _ _ = ren_tm ?R ?M' |- _] => inv M'; simpl in *; try congruence
|[H: lam _ _ = lam _ _ |- _] => inv H
|[H: app _ _ = app _ _|- _] => inv H
|[H: ids _ = ids _|- _] => inv H
end.

Hint Constructors SN SNe SNRed.

Lemma anti_rename:
  (forall n (M: tm n), SN M -> forall n' M' (R: fin n' -> fin n), M = ren_tm R M' -> SN M')
 /\ (forall n (M: tm n), SNe M -> forall n' M' (R: fin n' -> fin n), M = ren_tm R M' -> SNe M')
 /\ (forall n (M N: tm n), SNRed M N -> forall n' (R: fin n' -> fin n) M', M = ren_tm R M' -> exists N', N = ren_tm R N' /\ SNRed M' N').
Proof.
  apply SN_multind; intros; repeat invTm; asimpl in *; subst; eauto.
  - destruct (H0 _ _ _ (eq_refl _)) as (M''&->&?).
    eapply SRed; eauto.
  - destruct M'; simpl in *; try congruence.
    inv H; now constructor.
  - exists (M'0_1 [M'0_2..]).
    split. now asimpl. constructor; eauto.
  - destruct (H0 _ _ _ (eq_refl (ren_tm R0 M'1))) as (N'&->&A2).
    exists (app N' M'2). split; [reflexivity| now constructor].
Qed.

Lemma rename :
  (forall n (M: tm n), SN M -> forall n' (R: fin n -> fin n'), SN (ren_tm R M))
  /\ (forall n (M: tm n), SNe M -> forall n' (R: fin n -> fin n'), SNe (ren_tm R M))
  /\ (forall n (M N: tm n), SNRed M N -> forall n' (R: fin n -> fin n'), SNRed (ren_tm R M) (ren_tm R N)).
Proof.
  apply SN_multind; intros; asimpl in *; eauto.
  - constructor.
  - intros. subst. constructor. auto. now asimpl.
Qed.

Lemma ext_SN n (M: tm n) (p: fin n) :
  SN (app M (var_tm p)) -> SN M.
Proof.
  intros H. remember (app M (var_tm p)) as Mp. revert M p HeqMp.
  induction H; intros; subst.
  - inv H. now constructor.
  - inv HeqMp.
  - inv H.
    + apply SAbs. eapply anti_rename. exact H0.
      instantiate (1 := p..). substify. now asimpl.
    + eapply SRed. exact H. eapply IHSN. reflexivity.
Qed.

Fixpoint Red {n} (A : ty) : tm n -> Prop :=
  match A with
  | Base => fun s => SN s
  | Fun A B => fun s =>
      forall n' (S : fin n -> fin n') (t : tm n'), Red A t -> Red B (app (ren_tm S s) t)
  end.

Definition RedS {n n'} (S: fin n -> tm n') (Gamma: fin n -> ty) :=
  forall i, Red (Gamma i) (S i).

Lemma rename_red m n (f : fin m -> fin n) (s : tm m) A :
  Red A s -> Red A (ren_tm f s).
Proof.
  revert s. destruct A as [| A B]; intros s; cbn.
  - intros H. now apply rename.
  - intros H n' g t lt. asimpl. now apply H.
Qed.

Lemma cr A:
  (forall n (M: tm n), Red A M -> SN M) /\ (forall n (M: tm n), SNe M -> Red A M) /\ (forall n (M M': tm n), SNRed M M' -> Red A M' -> Red A M).
Proof.
  induction A as [|A IHA B IHB].
  - repeat split; intros.
    + assumption.
    + now apply SNeu.
    + now apply SRed with (M' := M').
  - repeat split; intros.
    + eapply anti_rename with (R := shift) (M := ren_tm shift M); [|reflexivity].
      eapply ext_SN, IHB. cbn in H. apply H, IHA. apply SVar with (x:= var_zero).
    + intros g' R N H'. apply IHB.
      apply SApp. now apply rename. now intuition.
    + intros g' R N rn. apply IHB with (M' := app (ren_tm R M') N).
     * constructor. now apply rename.
     * apply H0, rn.
Qed.

Lemma red_var n (p: fin n) A:
  Red A (var_tm p).
Proof. apply cr, SVar. Qed.

From Chapter9 Require Export preservation.

Lemma main_lemma n (M: tm n) A Gamma:
  Gamma |- M : A -> forall n' (S: fin n -> tm n'), RedS S Gamma -> Red A (subst_tm S M).
Proof.
  induction 1; intros.
  - cbn. apply H.
    - intros m R N rn.
    eapply cr.
    + cbn. econstructor.
      * eapply cr; eauto.
      * reflexivity.
    + asimpl. eapply IHhas_type. intros [|]; eauto.
      * cbn. unfold funcomp. renamify. apply rename_red. eauto.
  - cbn. specialize (IHhas_type2 _ _ H1).
    specialize (IHhas_type1 _ _ H1 n' id _ IHhas_type2).
    asimpl in IHhas_type1. eauto.
Qed.

Lemma id_red g Gamma: @RedS g g ids Gamma.
Proof. intros i. now apply red_var. Qed.

Lemma norm n (M: tm n) (A: ty) Gamma: Gamma |- M : A -> SN M.
Proof.
  intros C.
  assert (H := main_lemma C (@id_red n Gamma)).
  asimpl in H. now apply cr in H.
Qed.