Library Postpone

Require Import Relation_Operators.
Require Import Relation_Definitions.
Require Import Coq.Structures.Equalities.
Require Import Coq.Program.Equality.
Require Import Coq.Arith.Compare_dec.
Require Import Coq.Arith.Plus.
Require Import Coq.Arith.Lt.
Require Import Omega.

Require Import Untyped.
Require Import Subst.
Require Import Rels.
Require Import Beta.
Require Import Eta.

Postponement theorem in Untyped Lambda Calculus


Module Export Postpone.

This module contains a formalised proof of the (η-)Postponement Theorem for the untyped lambda calculus.
The formalisation is based on an ``informal'' proof due to Masako Takahashi in ``Parallel Reductions in Lambda-calculus'' (Information and Computation, Volume 118, 1995).
Except for the gymnastics related to working with de Bruijn indices, the translation of the Takashi's proof is rather straightforward.

Preliminaries

We at first prove various properties about the relation between beta_par and the eta-expansion lam_k. (This is Lemma 3.3 in Takahashi).
We however do it in in a slightly different order than in the paper, because the cases of the lemma actually depend on each other in a slightly differently order than the one stated in the paper.
Firstly, an application of a k-fold eta-expansion of a lambda abstraction can be reduced simply to a substitution via parallel beta.
Lemma lam_k_beta_subst:
   k, M M' N N',
    beta_par M M'beta_par N N'
      beta_par (App (lam_k k (Lam M)) N) (subst 0 N' M').
Proof.
  induction k.
  (* k := 0 *)
  intros.
  simpl. apply beta_par_base; assumption.
  (* k := (S k) *)
  intros.
  simpl.
  apply beta_par_base. rewrite shift_0_lam_commute.
  unfold shift. simpl.
  replace M' with (subst 0 (Var 0) (shift 1 M')).
  apply IHk.
  apply beta_par_shift. assumption. apply beta_par_refl.
  apply subst_k_shift_S_k. assumption.
Qed.

Similarly, a k-fold eta-expansion of a lambda abstraction can be reduced to a single lambda abstraction via parallel beta reduction.

Lemma lam_k_beta_lam:
   k, M M',
    beta_par M M'beta_par (lam_k k (Lam M)) (Lam M').
Proof.
  induction k.
  (* k := 0 *)
  intros. simpl. apply beta_par_lam. assumption.
  (* k := (S k) *)
  intros.
  remember H as HH. clear HeqHH. apply IHk in H.
  simpl.
  constructor.
  rewrite shift_0_lam_commute.
  unfold shift. simpl.
  replace M' with (subst 0 (Var 0) (shift 1 M')).
  apply lam_k_beta_subst.
  apply beta_par_shift. assumption.
  apply beta_par_refl.
  apply subst_k_shift_S_k.
Qed.

In case of an application, we can also contract the whole eta-expansion of the applied term via parallel beta reduction

Lemma lam_k_beta_app:
   k, M M' N N',
    beta_par M M'beta_par N N'
      beta_par (App (lam_k k M) N) (App M' N').
Proof.
  induction k.
  (* k := 0 *)
  intros. simpl. apply beta_par_app. assumption. assumption.
  (* k := (S k) *)
  intros.
  rewrite lam_k_alt.
  replace (App M' N') with (subst 0 N' (App (shift 0 M') (Var 0))).
  apply lam_k_beta_subst.
  constructor. apply beta_par_shift. assumption. apply beta_par_refl.
      assumption.
  simpl. rewrite lift_0_ident. rewrite subst_shift_ident. reflexivity.
Qed.

Finally, k+1 eta-expansions can always be contracted to only one eta-expansion via parallel beta reduction.
Lemma lam_S_k_beta:
   k, M M',
    beta_par M M'
      beta_par (lam_k (S k) M) (lam_k 1 M').
Proof.
  induction k.
  (* k := 0 *)
  intros. simpl.
  constructor. constructor. apply beta_par_shift. assumption.
  apply beta_par_refl.
  (* k := (S k) *)
  intros.
  rewrite lam_k_alt.
  apply lam_k_beta_lam.
  constructor. apply beta_par_shift. assumption. apply beta_par_refl.
Qed.

It now remains to prove the crucial Lemma 3.4 from Takahashi, stating that postponement holds for the case of parallel beta and eta reductions.
Before we can do that, we need one auxiliary fact:
Parallel beta is closed under eta-expansion.

Lemma beta_par_lam_k_closed:
   k, M N,
    beta_par M Nbeta_par (lam_k k M) (lam_k k N).
Proof.
  induction k.
  intros.
  simpl. assumption.
  intros.
  simpl. constructor. constructor. apply beta_par_shift. apply IHk. assumption.
  apply beta_par_refl.
Qed.

We can now prove the postponement theorem for the specific case of parallel reductions. This is Lemma 3.4 in Takahashi.

Lemma postpone_par:
   M P N,
    eta_par M Pbeta_par P N
        ( P', beta_par M P' eta_par P' N).
Proof.
  intros.
  generalize dependent M.
  rename H0 into H.
  dependent induction H.
  (* P = (Var n) = N *)
      intros.
       M. split.
      apply beta_par_refl.
      assumption.
  (* P = (Lam P1) *)
      intro K.
      intros.
      rename M' into N1.
      rename M into P.
      rename K into M.
      apply eta_par_lam_k_lam in H0.
      do 3 destruct H0.
      rewrite H1; clear H1; clear M.
      apply IHbeta_par in H0.
      do 2 destruct H0.
       (Lam x1).
      split.
      apply lam_k_beta_lam. assumption.
      constructor. assumption.

   (* App case *)
      intros MM HH.
      apply eta_par_lam_k_app in HH.
      destruct HH. do 3 destruct H1.
      destruct H2.
      rewrite H3; clear H3; clear MM.
      apply IHbeta_par1 in H1.
      apply IHbeta_par2 in H2.
      do 2 destruct H1.
      do 2 destruct H2.
      (* This feels like a weird choice, but seems to work. *)
       (lam_k x (App x2 x3)).
      split.
      Focus 2.
      induction x.
      simpl. constructor; assumption.
      simpl. apply eta_par_base with (lam_k x (App x2 x3)).
      reflexivity. assumption.
      induction x.
      simpl. constructor; assumption.
      simpl. constructor. constructor.
      apply beta_par_shift. assumption. apply beta_par_refl.

   (* subst case *)
      intros.
      apply eta_par_lam_k_app in H1.
      do 4 destruct H1. destruct H2.
      rewrite H3. clear H3. clear M0.
      apply eta_par_lam_k_lam in H1.
      do 3 destruct H1. rewrite H3. clear H3. clear x0.
      apply IHbeta_par1 in H1.
      apply IHbeta_par2 in H2.
      do 2 destruct H1.
      do 2 destruct H2.
       (lam_k x (subst 0 x4 x0)).
      split.

      apply beta_par_lam_k_closed.
      apply lam_k_beta_subst. assumption. assumption.

      apply lam_k_eta_red.
      apply eta_par_subst_closed.
      assumption.
      assumption.
Qed.

We now define the beta-eta relation and its reflexive-transitive closure
We need a couple of auxiliary statements about the relationships between the parallel and reflexive-transitive versions of beta and eta reductions which appear in the conclusions of the postponement theorem.
They make it more convenient to do the rewriting while proving the main result.
Firstly, since the reflexive-transitive closures are equivalent to the transitive closures of the parallel relations, the following holds:

Lemma star_exists_iff_par_exists:
   M N,
  ( P, bstar M P eta_star P N)
  ( P, beta_par_trans M P eta_par_trans P N).
Proof.
  split; intros;
  do 2 destruct H;
   x; split;
  do 2 (try
          apply bstar_eq_closure_of_beta_par ||
          apply eta_star_eq_closure_of_eta_par;
       assumption).
Qed.

Also, it is obviously sufficient to show this to hold for parallel beta, in order for it to also hold for the transitive closure:

Lemma par_impl_par_trans:
   M N,
    ( P, beta_par M P eta_par P N) →
    ( P, beta_par_trans M P eta_par_trans P N).
Proof.
  intros. destruct H. destruct H as [H1 H2].
   x.
  split; constructor; assumption.
Qed.

Finally, a couple of "one-sided" rewrites for convenience within the proof.

Lemma rewrite_existential_eta:
   M N,
  ( P, beta_par M P eta_star P N)
  ( P, beta_par M P eta_par_trans P N).
Proof.
  split; intros;
  do 2 destruct H;
   x; split;
  do 2 (try
          apply bstar_eq_closure_of_beta_par ||
          apply eta_star_eq_closure_of_eta_par;
       assumption).
Qed.

Lemma rewrite_existential_beta:
   M N,
  ( P, bstar M P eta_par P N)
  ( P, beta_par_trans M P eta_par P N).
Proof.
  split; intros;
  do 2 destruct H;
   x; split;
  do 2 (try
          apply bstar_eq_closure_of_beta_par ||
          apply eta_star_eq_closure_of_eta_par;
       assumption).
Qed.

We now build up to the full postponement lemma by proving a series of simpler lemmas
Here we consider the case where we postpone eta_star in the presence of only a parallel beta.

Lemma eta_baby_postpone_eta:
   M P N,
    eta_star M Pbeta_par P N
      ( P', beta_par M P' eta_star P' N).
Proof.
  intros ? ? ? H1 H2.
  apply rewrite_existential_eta.
  generalize dependent N.
  dependent induction H1.
  intros.
  assert (HH: P', beta_par x P' eta_par P' N).
  apply eta_imp_eta_par in H.
  apply postpone_par with y; assumption.
  destruct HH. destruct H0.
   x0. split. assumption. constructor. assumption.

  intros. N.
  split. assumption. constructor. apply eta_par_refl.

  intros.

  fold eta_star in H1_, H1_0.
  apply IHclos_refl_trans2 in H2.
  destruct H2. destruct H.
  apply IHclos_refl_trans1 in H.
  destruct H. destruct H.
   x1.
  split. assumption.
  apply t_trans with x0; assumption.
Qed.

Similarly, here we consider only the postponement of eta_par in the presence bstar:

Lemma eta_baby_postpone_beta:
   M P N,
    eta_par M Pbstar P N
      ( P', bstar M P' eta_par P' N).
Proof.
  intros ? ? ? H1 H2.
  apply rewrite_existential_beta.
  generalize dependent M.
  dependent induction H2.
  intros.
  assert (HH: P', beta_par M P' eta_par P' y).
  apply bred_imp_beta_par in H.
  apply postpone_par with x; assumption.
  destruct HH. destruct H0.
   x0. split. constructor. assumption. assumption.

  intros. M.
  split. constructor. apply beta_par_refl. assumption.

  intros.

  fold bstar in H2_, H2_0.
  apply IHclos_refl_trans1 in H1.
  destruct H1. destruct H.
  apply IHclos_refl_trans2 in H0.
  destruct H0. destruct H0.
   x1.
  split. apply t_trans with x0; assumption. assumption.
Qed.

We now combine all the previous lemmas to prove a simplified version of the eta-postponement where we consider separate eta_star and bstar reductions, rather than a single reduction of their union.

Theorem eta_postponement_basic:
   M N P,
    eta_star M Pbstar P N → ( P', bstar M P' eta_star P' N).
Proof.
  intros.
  rewrite eta_star_eq_closure_of_eta_par in ×.
  rewrite bstar_eq_closure_of_beta_par in ×.
  rewrite star_exists_iff_par_exists.
  generalize dependent M.
  dependent induction H0.
  intros.
  assert (HH:
            ( P, beta_par M P eta_star P y) →
            ( P, beta_par_trans M P eta_par_trans P y)).
  intros.
  destruct H1. destruct H1.
  apply beta_par_imp_bstar in H1.
  apply bstar_eq_closure_of_beta_par in H1.
  apply eta_star_eq_closure_of_eta_par in H2.
   x0.
  split; assumption.

  assert (HH2:
            ( P, beta_par M P eta_star P y)).

  apply eta_baby_postpone_eta with x.
  apply eta_star_eq_closure_of_eta_par. assumption. assumption.
  apply HH. assumption.

  fold beta_par_trans in H0_, H0_0.
  intros.
  apply IHclos_trans1 in H.
  destruct H. destruct H.
  apply IHclos_trans2 in H0.
  destruct H0. destruct H0.

   x1.
  split. apply t_trans with x0; assumption. assumption.
Qed.

The eta postponement theorem

Finally, we prove the full eta-postponement theorem using the separate reduction version in eta_postponement_basic.

Theorem eta_postponement:
   M N,
    beta_eta_star M N → ( P, bstar M P eta_star P N).
Proof.
  intros.
  dependent induction H.

  destruct H.
     y. split. constructor. assumption. apply rt_refl.
     x. split. apply rt_refl. constructor. assumption.

   x. split. apply rt_refl. apply rt_refl.

  rename H into H1. rename H0 into H2.
  fold beta_eta_star in H1, H2.

  destruct IHclos_refl_trans1 as [xy]. destruct H as [A1 A2].
  destruct IHclos_refl_trans2 as [yz]. destruct H as [B1 B2].

  assert (H: xyz, bstar xy xyz eta_star xyz yz).
  apply eta_postponement_basic with y; assumption.

  do 2 destruct H.
   x0.

  split. apply rt_trans with xy; assumption.
  apply rt_trans with yz; assumption.
Qed.

End Postpone.