Require Import List.
Require Import Arith.
Require Import Omega.

Require Import Util.
Require Import MatchCompNat.
Require Import SimplyTypedLambdaCalculus.

Module LambdaCalculusNormalization(Constants: LambdaConstants).

Module My_LambdaCalculus := LambdaCalculus(Constants).

Import My_LambdaCalculus.
Import Constants.

Fixpoint polySubst_in_term (t: LTerm) (k: nat) (us': (list LTerm)) {struct us'}: LTerm :=
  match us' with
    | nil => t
    | (u :: us) => (polySubst_in_term (subst_in_term t (k + (length us)) u) k us)
  end
.

Lemma PolySubstitution_preserves_typing:
  forall (G1 Us G2: LEnv) (T: LType) (t: LTerm) (us: (list LTerm)),
    (Forall2 (fun u U => (WellTyped G1 u U)) us Us) ->
    (WellTyped (G1 ++ Us ++ G2) t T) ->
    (WellTyped (G1 ++ G2) (polySubst_in_term t (length G2) us) T)
.

Lemma PolySubstitution_preserves_typing_cor1:
  forall (G1 Us: LEnv) (t: LTerm) (T: LType) (us: (list LTerm)),
    (WellTyped (G1 ++ Us) t T) ->
    (Forall2 (fun u U => (WellTyped G1 u U)) us Us) ->
    (WellTyped G1 (polySubst_in_term t 0 us) T)
.

Fixpoint Reductible (G: LEnv) (t: LTerm) (T': LType) {struct T'}: Prop :=
  (WellTyped G t T') /\
  (Acc (symRel RedTerm) t) /\
  match T' with

    | LType_base =>
      (Acc (symRel RedTerm) t)

    | (LType_fun T U) =>
      forall (G': LEnv) (u: LTerm),
        (Reductible (G' ++ G) u T) ->
        (Reductible (G' ++ G) (LTerm_app t u) U)

    | (LType_prod T U) =>
      (Reductible G (LTerm_fst t) T) /\
      (Reductible G (LTerm_snd t) U)
  end
.


Lemma Reductible_implies_WellTyped:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (Reductible G t T) ->
    (WellTyped G t T)
.


Lemma Reductible_implies_SN:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (Reductible G t T) ->
    (Acc (symRel RedTerm) t)
.


Lemma Reductible2:
  forall (G: LEnv) (t: LTerm),
    (Reductible G t LType_base) ->
    (Acc (symRel RedTerm) t)
.

Lemma Reductible3:
  forall (G: LEnv) (t: LTerm) (T U: LType),
    (Reductible G t (LType_fun T U)) ->
    forall (G': LEnv) (u: LTerm),
      (Reductible (G' ++ G) u T) ->
      (Reductible (G' ++ G) (LTerm_app t u) U)
.

Lemma Reductible3_cor:
  forall (G: LEnv) (t u: LTerm) (T U: LType),
    (Reductible G t (LType_fun T U)) ->
    (Reductible G u T) ->
    (Reductible G (LTerm_app t u) U)
.


Lemma Reductible4:
  forall (G: LEnv) (t: LTerm) (T U: LType),
    (Reductible G t (LType_prod T U)) ->
    (Reductible G (LTerm_fst t) T)
.

Lemma Reductible5:
  forall (G: LEnv) (t: LTerm) (T U: LType),
    (Reductible G t (LType_prod T U)) ->
    (Reductible G (LTerm_snd t) U)
.

Hint Resolve Reductible_implies_WellTyped Reductible_implies_SN Reductible2
             Reductible3 Reductible3_cor Reductible4 Reductible5 : reductible_db.

Lemma Reductible_base:
  forall (G: LEnv) (t: LTerm),
    (WellTyped G t LType_base) ->
    (Acc (symRel RedTerm) t) ->
    (Reductible G t LType_base)
.


Lemma Reductible_fun:
  forall (G: LEnv) (t: LTerm) (T U: LType),
    (WellTyped G t (LType_fun T U)) ->
    (Acc (symRel RedTerm) t) ->
    (forall (G': LEnv) (u: LTerm),
      (Reductible (G' ++ G) u T) ->
      (Reductible (G' ++ G) (LTerm_app t u) U)
    ) ->
    (Reductible G t (LType_fun T U))
.


Lemma Reductible_prod:
  forall (G: LEnv) (t: LTerm) (T U: LType),
    (WellTyped G t (LType_prod T U)) ->
    (Acc (symRel RedTerm) t) ->
    (Reductible G (LTerm_fst t) T) ->
    (Reductible G (LTerm_snd t) U) ->
    (Reductible G t (LType_prod T U))
.



Lemma Reductible_left_weakening:
  forall (G G': LEnv) (t: LTerm) (T: LType),
    (Reductible G t T) ->
    (Reductible (G' ++ G) t T)
.











Lemma SN_var_intro:
  forall (i: nat),
    (Acc (symRel RedTerm) (LTerm_var i))
.



Lemma polySubst_in_const:
  forall (c: LConst) (k: nat) (us: (list LTerm)),
    (polySubst_in_term (LTerm_const c) k us) =
    (LTerm_const c)
.




Lemma polySubst_in_fun:
  forall (T: LType) (t: LTerm) (k: nat) (us: (list LTerm)),
    (polySubst_in_term (LTerm_fun T t) k us) =
    (LTerm_fun T (polySubst_in_term t (S k) us))
.





Lemma polySubst_in_app:
  forall (t u: LTerm) (k: nat) (us: (list LTerm)),
    (polySubst_in_term (LTerm_app t u) k us) =
    (LTerm_app (polySubst_in_term t k us)
               (polySubst_in_term u k us))
.




Lemma polySubst_in_pair:
  forall (t u: LTerm) (k: nat) (us: (list LTerm)),
    (polySubst_in_term (LTerm_pair t u) k us) =
    (LTerm_pair (polySubst_in_term t k us)
                (polySubst_in_term u k us))
.




Lemma polySubst_in_fst:
  forall (t: LTerm) (k: nat) (us: (list LTerm)),
    (polySubst_in_term (LTerm_fst t) k us) =
    (LTerm_fst (polySubst_in_term t k us))
.




Lemma polySubst_in_snd:
  forall (t: LTerm) (k: nat) (us: (list LTerm)),
    (polySubst_in_term (LTerm_snd t) k us) =
    (LTerm_snd (polySubst_in_term t k us))
.




Lemma polySubst_in_var1:
  forall (us: (list LTerm)) (i: nat),
    i >= (length us) ->
    (polySubst_in_term (LTerm_var i) 0 us) = (LTerm_var (i - (length us)))
.








Lemma polySubst_by_snoc:
  forall (t u: LTerm) (k: nat) (us: (list LTerm)),
    (polySubst_in_term t k (snoc us u)) =
    (subst_in_term (polySubst_in_term t (S k) us) k u)
.





Lemma polySubst_of_var_invariant:
  forall (i k: nat) (us: (list LTerm)),
    i < k ->
    (polySubst_in_term (LTerm_var i) k us) = (LTerm_var i)
.





Lemma lift_in_var_by_zero:
  forall (i k: nat),
    (lift_at_depth_in_var i k 0) = i
.



Lemma lift_in_term_by_zero:
  forall (t: LTerm) (k: nat),
    (lift_at_depth_in_term t k 0) = t
.









Lemma Permuting_lifting_and_polySubstitution:
  forall (t: LTerm) (i: nat) (us: (list LTerm)) (n: nat),
    (lift_in_term (polySubst_in_term t i us) n) =
    (polySubst_in_term (lift_in_term t n) (i + n) us)
.





Lemma polySubst_in_var_variant:
  forall (u: LTerm) (us: (list LTerm)) (i: nat),
    (List_from us i u) ->
    (polySubst_in_term (LTerm_var i) 0 us) = u
.



















Lemma Reductible_subject_reduction:
  forall (T: LType) (G: LEnv) (t t': LTerm),
    (Reductible G t T) ->
    (RedTerm t t') ->
    (Reductible G t' T)
.



















Lemma Reductible_subject_reduction_star:
  forall (T: LType) (G: LEnv) (t t': LTerm),
    (Reductible G t T) ->
    (RedTermStar t t') ->
    (Reductible G t' T)
.




Module Type PreReductible.

Parameter PreRed: LEnv -> LTerm -> LType -> Prop.

Parameter PreRed_implies_WellTyped:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (WellTyped G t T)
.

Parameter PreRed_left_weakening:
  forall (G G': LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (PreRed (G' ++ G) t T)
.

Parameter PreRed_implies_SN:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (Acc (symRel RedTerm) t)
.

Parameter PreRed_subject_reduction:
  forall (G: LEnv) (t t': LTerm) (T: LType),
    (PreRed G t T) ->
    (RedTerm t t') ->
    (PreRed G t' T) \/ (Reductible G t' T)
.

Parameter PreRed_not_a_function:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (U: LType) (u: LTerm),
      t <> (LTerm_fun U u)
.

Parameter PreRed_not_a_pair:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (u1 u2: LTerm),
      t <> (LTerm_pair u1 u2)
.

End PreReductible.

Module ProveReductible(PR: PreReductible).

Import PR.

Inductive ClosRed (G: LEnv): LTerm -> LType -> Prop :=

  | ClosRed_base:
    forall (t: LTerm) (T: LType),
      (PreRed G t T) ->
      (ClosRed G t T)

  | ClosRed_app:
    forall (t u: LTerm) (T U: LType),
      (ClosRed G t (LType_fun T U)) ->
      (Reductible G u T) ->
      (ClosRed G (LTerm_app t u) U)

  | ClosRed_fst:
    forall (t: LTerm) (T U: LType),
      (ClosRed G t (LType_prod T U)) ->
      (ClosRed G (LTerm_fst t) T)

  | ClosRed_snd:
    forall (t: LTerm) (T U: LType),
      (ClosRed G t (LType_prod T U)) ->
      (ClosRed G (LTerm_snd t) U)
.

Lemma ClosRed_left_weakening:
  forall (G G': LEnv) (t: LTerm) (T: LType),
    (ClosRed G t T) ->
    (ClosRed (G' ++ G) t T)
.






Lemma ClosRed_implies_WellTyped:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (ClosRed G t T) ->
    (WellTyped G t T)
.






Lemma ClosRed_not_a_function:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (ClosRed G t T) ->
    forall (U: LType) (u: LTerm),
      t <> (LTerm_fun U u)
.





Lemma ClosRed_not_a_pair:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (ClosRed G t T) ->
    forall (u1 u2: LTerm),
      t <> (LTerm_pair u1 u2)
.





Lemma ClosRed_subject_reduction:
  forall (G: LEnv) (t t': LTerm) (T: LType),
    (ClosRed G t T) ->
    (RedTerm t t') ->
    (ClosRed G t' T) \/ (Reductible G t' T)
.

















Lemma ClosRed_implies_SN_aux1:
  forall (G: LEnv) (t u: LTerm) (T U: LType),
    (ClosRed G t (LType_fun T U)) ->
    (Acc (symRel RedTerm) t) ->
    (Reductible G u T) ->
    (Acc (symRel RedTerm) u) ->
    (Acc (symRel RedTerm) (LTerm_app t u))
.







Lemma ClosRed_implies_SN_aux2:
  forall (G: LEnv) (t: LTerm) (T U: LType),
    (ClosRed G t (LType_prod T U)) ->
    (Acc (symRel RedTerm) t) ->
    (Acc (symRel RedTerm) (LTerm_fst t))
.





Lemma ClosRed_implies_SN_aux3:
  forall (G: LEnv) (t: LTerm) (T U: LType),
    (ClosRed G t (LType_prod T U)) ->
    (Acc (symRel RedTerm) t) ->
    (Acc (symRel RedTerm) (LTerm_snd t))
.





Theorem ClosRed_implies_SN:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (ClosRed G t T) ->
    (Acc (symRel RedTerm) t)
.






Lemma ClosRed_implies_Reductible:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (ClosRed G t T) ->
    (Reductible G t T)
.









Lemma PreRed_implies_Reductible:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (Reductible G t T)
.


End ProveReductible.


Inductive PreRed_const (G: LEnv): LTerm -> LType -> Prop :=

  | PreRed_const_intro:
    forall (c: LConst) (T: LType),
      (WellTyped G (LTerm_const c) T) ->
      (PreRed_const G (LTerm_const c) T)
.

Module PreReductible_const.

Definition PreRed: LEnv -> LTerm -> LType -> Prop := PreRed_const.

Lemma PreRed_implies_WellTyped:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (WellTyped G t T)
.


Lemma PreRed_left_weakening:
  forall (G G': LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (PreRed (G' ++ G) t T)
.


Lemma PreRed_implies_SN:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (Acc (symRel RedTerm) t)
.


Lemma PreRed_subject_reduction:
  forall (G: LEnv) (t t': LTerm) (T: LType),
    (PreRed G t T) ->
    (RedTerm t t') ->
    (PreRed G t' T) \/ (Reductible G t' T)
.


Lemma PreRed_not_a_function:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (U: LType) (u: LTerm),
      t <> (LTerm_fun U u)
.


Lemma PreRed_not_a_pair:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (u1 u2: LTerm),
      t <> (LTerm_pair u1 u2)
.


End PreReductible_const.

Module ProveReductible_const := ProveReductible(PreReductible_const).

Lemma Constants_are_reductible:
  forall (G: LEnv) (c: LConst) (T: LType),
    (WellTyped G (LTerm_const c) T) ->
    (Reductible G (LTerm_const c) T)
.



Inductive PreRed_var (G: LEnv): LTerm -> LType -> Prop :=

  | PreRed_var_intro:
    forall (i: nat) (T: LType),
      (WellTyped G (LTerm_var i) T) ->
      (PreRed_var G (LTerm_var i) T)
.

Module PreReductible_var.

Definition PreRed: LEnv -> LTerm -> LType -> Prop := PreRed_var.

Lemma PreRed_implies_WellTyped:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (WellTyped G t T)
.


Lemma PreRed_left_weakening:
  forall (G G': LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (PreRed (G' ++ G) t T)
.


Lemma PreRed_implies_SN:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (Acc (symRel RedTerm) t)
.


Lemma PreRed_subject_reduction:
  forall (G: LEnv) (t t': LTerm) (T: LType),
    (PreRed G t T) ->
    (RedTerm t t') ->
    (PreRed G t' T) \/ (Reductible G t' T)
.


Lemma PreRed_not_a_function:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (U: LType) (u: LTerm),
      t <> (LTerm_fun U u)
.


Lemma PreRed_not_a_pair:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (u1 u2: LTerm),
      t <> (LTerm_pair u1 u2)
.


End PreReductible_var.

Module ProveReductible_var := ProveReductible(PreReductible_var).

Lemma Variables_are_reductible:
  forall (G: LEnv) (i: nat) (T: LType),
    (WellTyped G (LTerm_var i) T) ->
    (Reductible G (LTerm_var i) T)
.



Inductive PreRed_fstProj (G: LEnv): LTerm -> LType -> Prop :=

  | PreRed_fstProj_intro:
    forall (t u: LTerm) (T U: LType),
      (Reductible G t T) ->
      (WellTyped G u U) ->
      (Acc (symRel RedTerm) u) ->
      (PreRed_fstProj G (LTerm_fst (LTerm_pair t u)) T)
.

Module PreReductible_fstProj.

Definition PreRed: LEnv -> LTerm -> LType -> Prop := PreRed_fstProj.

Lemma PreRed_implies_WellTyped:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (WellTyped G t T)
.



Lemma PreRed_left_weakening:
  forall (G G': LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (PreRed (G' ++ G) t T)
.



Lemma PreRed_implies_SN:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (Acc (symRel RedTerm) t)
.








Lemma PreRed_subject_reduction:
  forall (G: LEnv) (t t': LTerm) (T: LType),
    (PreRed G t T) ->
    (RedTerm t t') ->
    (PreRed G t' T) \/ (Reductible G t' T)
.







Lemma PreRed_not_a_function:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (U: LType) (u: LTerm),
      t <> (LTerm_fun U u)
.


Lemma PreRed_not_a_pair:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (u1 u2: LTerm),
      t <> (LTerm_pair u1 u2)
.


End PreReductible_fstProj.

Module ProveReductible_fstProj := ProveReductible(PreReductible_fstProj).

Lemma First_projections_are_reductible:
  forall (G: LEnv) (t u: LTerm) (T U: LType),
    (Reductible G t T) ->
    (WellTyped G u U) ->
    (Acc (symRel RedTerm) u) ->
    (Reductible G (LTerm_fst (LTerm_pair t u)) T)
.



Inductive PreRed_sndProj (G: LEnv): LTerm -> LType -> Prop :=

  | PreRed_sndProj_intro:
    forall (t u: LTerm) (T U: LType),
      (WellTyped G t T) ->
      (Acc (symRel RedTerm) t) ->
      (Reductible G u U) ->
      (PreRed_sndProj G (LTerm_snd (LTerm_pair t u)) U)
.

Module PreReductible_sndProj.

Definition PreRed: LEnv -> LTerm -> LType -> Prop := PreRed_sndProj.

Lemma PreRed_implies_WellTyped:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (WellTyped G t T)
.



Lemma PreRed_left_weakening:
  forall (G G': LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (PreRed (G' ++ G) t T)
.



Lemma PreRed_implies_SN:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (Acc (symRel RedTerm) t)
.








Lemma PreRed_subject_reduction:
  forall (G: LEnv) (t t': LTerm) (T: LType),
    (PreRed G t T) ->
    (RedTerm t t') ->
    (PreRed G t' T) \/ (Reductible G t' T)
.







Lemma PreRed_not_a_function:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (U: LType) (u: LTerm),
      t <> (LTerm_fun U u)
.


Lemma PreRed_not_a_pair:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (u1 u2: LTerm),
      t <> (LTerm_pair u1 u2)
.


End PreReductible_sndProj.

Module ProveReductible_sndProj := ProveReductible(PreReductible_sndProj).

Lemma Second_projections_are_reductible:
  forall (G: LEnv) (t u: LTerm) (T U: LType),
    (WellTyped G t T) ->
    (Acc (symRel RedTerm) t) ->
    (Reductible G u U) ->
    (Reductible G (LTerm_snd (LTerm_pair t u)) U)
.



Inductive PreRed_appFun (G: LEnv): LTerm -> LType -> Prop :=

  | PreRed_appFun_intro:
    forall (t u: LTerm) (T U: LType),
      (WellTyped (snoc G T) t U) ->
      (Acc (symRel RedTerm) t) ->
      (Reductible G u T) ->
      (Reductible G (subst_in_term t 0 u) U) ->
      (PreRed_appFun G (LTerm_app (LTerm_fun T t) u) U)
.

Module PreReductible_appFun.

Definition PreRed: LEnv -> LTerm -> LType -> Prop := PreRed_appFun.

Lemma PreRed_implies_WellTyped:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (WellTyped G t T)
.



Lemma PreRed_left_weakening:
  forall (G G': LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (PreRed (G' ++ G) t T)
.



Lemma PreRed_implies_SN:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    (Acc (symRel RedTerm) t)
.











Lemma PreRed_subject_reduction:
  forall (G: LEnv) (t t': LTerm) (T: LType),
    (PreRed G t T) ->
    (RedTerm t t') ->
    (PreRed G t' T) \/ (Reductible G t' T)
.










Lemma PreRed_not_a_function:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (U: LType) (u: LTerm),
      t <> (LTerm_fun U u)
.


Lemma PreRed_not_a_pair:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (PreRed G t T) ->
    forall (u1 u2: LTerm),
      t <> (LTerm_pair u1 u2)
.


End PreReductible_appFun.

Module ProveReductible_appFun := ProveReductible(PreReductible_appFun).

Lemma Lambda_redices_are_reductible:
  forall (G: LEnv) (t u: LTerm) (T U: LType),
    (WellTyped (snoc G T) t U) ->
    (Acc (symRel RedTerm) t) ->
    (Reductible G u T) ->
    (Reductible G (subst_in_term t 0 u) U) ->
    (Reductible G (LTerm_app (LTerm_fun T t) u) U)
.



Lemma SN_subst_inversion:
  forall (t u: LTerm),
    (Acc (symRel RedTerm) (subst_in_term t 0 u)) ->
    (Acc (symRel RedTerm) t)
.





Lemma SN_pair_intro:
  forall (t u: LTerm),
    (Acc (symRel RedTerm) t) ->
    (Acc (symRel RedTerm) u) ->
    (Acc (symRel RedTerm) (LTerm_pair t u))
.





Lemma SN_fun_intro:
  forall (t: LTerm) (T: LType),
    (Acc (symRel RedTerm) t) ->
    (Acc (symRel RedTerm) (LTerm_fun T t))
.





Theorem WellTyped_implies_Reductible_aux:
  forall (G1 Us : LEnv) (t : LTerm) (T : LType) (us : list LTerm),
    (WellTyped (G1 ++ Us) t T) ->
    (Forall2 (fun (u : LTerm) (U : LType) => (Reductible G1 u U)) us Us) ->
    (Reductible G1 (polySubst_in_term t 0 us) T)
.










































Theorem WellTyped_implies_Reductible:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (WellTyped G t T) ->
    (Reductible G t T)
.



Theorem WellTyped_implies_SN:
  forall (G: LEnv) (t: LTerm) (T: LType),
    (WellTyped G t T) ->
    (Acc (symRel RedTerm) t)
.


End LambdaCalculusNormalization.