(***************************************************************************
* Safety for Simply Typed Lambda Calculus (CBV) - Full Beta Reduction      *
* Brian Aydemir & Arthur Charguéraud, July 2007, Coq v8.1                  *
***************************************************************************)

Set Implicit Arguments.
Require Import Metatheory.

Require Import 
  STLC_Core_Definitions 
  STLC_Core_Infrastructure
  STLC_Core_Soundness.

(* ********************************************************************** *)
(** * Definitions *)

(** Full beta reduction *)

Inductive fullred : trm -> trm -> Prop :=
  | fullred_red : forall t1 t2,
      body t1 -> 
      term t2 ->
      fullred (trm_app (trm_abs t1) t2) (t1 ^^ t2) 
  | fullred_app1 : forall t1 t1' t2, 
      term t2 ->
      fullred t1 t1' -> 
      fullred (trm_app t1 t2) (trm_app t1' t2) 
  | fullred_app2 : forall t1 t2 t2',
      term t1 ->
      fullred t2 t2' ->
      fullred (trm_app t1 t2) (trm_app t1 t2') 
  | fullred_abs : forall L t1 t1', 
     (forall x, x \notin L -> fullred (t1 ^ x) (t1' ^ x)) ->
     fullred (trm_abs t1) (trm_abs t1').

Notation "t -->> t'" := (fullred t t') (at level 68).

(* ********************************************************************** *)
(** * Infrastructure *)

Lemma fullred_regular : forall e e',
  fullred e e' -> term e /\ term e'.
Proof.
  induction 1; use value_regular.
  split; apply_fresh term_abs as x; forward* (H0 x).
Qed.

Hint Extern 1 (term ?t) =>
  match goal with
  | H: fullred t _ |- _ => apply (proj1 (fullred_regular H))
  | H: fullred _ t |- _ => apply (proj2 (fullred_regular H))
  end.

Hint Constructors fullred.

(* ********************************************************************** *)
(** * Proofs *)

Lemma preservation_for_full_reduction : forall E t t' T,
  E |= t ~: T ->
  t -->> t' ->
  E |= t' ~: T.
Proof.
  introv Typ. gen t'.
  induction Typ; intros t' Red; inversions Red.
  apply_fresh* typing_abs as x.
  inversions Typ1. pick_fresh x.
    rewrite* (@subst_intro x). apply_empty* typing_subst.
  apply* typing_app.
  apply* typing_app.
Qed.