Library SimplyTypedLambdaCalculus


Simply typed lambda-calculus


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

Require Import Util.
Require Import MatchCompNat.


Module Type LambdaConstants.

Parameter LConst: Set.

Types - S, T, U
Inductive LType: Set :=
  | LType_base : LType
  | LType_fun : LType -> LType -> LType
  | LType_prod : LType -> LType -> LType
.

Parameter type_of_const: LConst -> LType -> Prop.

End LambdaConstants.


Module LambdaCalculus(My_LambdaConstants: LambdaConstants).

Import My_LambdaConstants.

Terms - s, t, u
Inductive LTerm: Set :=
  | LTerm_const : LConst -> LTerm
  | LTerm_var : nat -> LTerm
  | LTerm_fun : LType -> LTerm -> LTerm
  | LTerm_app : LTerm -> LTerm -> LTerm
  | LTerm_pair : LTerm -> LTerm -> LTerm
  | LTerm_fst : LTerm -> LTerm
  | LTerm_snd : LTerm -> LTerm
.

Function: lifts variable i with amplitude n at depth k
Definition lift_at_depth_in_var (i: nat) (k: nat) (n: nat): nat :=
  (match_comp_nat2 i k nat
    i
    (i + n)
  )
.

Function: lifts term t with amplitude n at depth k
Fixpoint lift_at_depth_in_term (t': LTerm) (k: nat) (n: nat) {struct t'}: LTerm :=
  match t' with
    | (LTerm_const c) => (LTerm_const c)
    | (LTerm_var i) => (LTerm_var (lift_at_depth_in_var i k n))
    | (LTerm_fun T t) => (LTerm_fun T (lift_at_depth_in_term t (S k) n))
    | (LTerm_app t u) => (LTerm_app (lift_at_depth_in_term t k n)
                                     (lift_at_depth_in_term u k n))
    | (LTerm_pair t u) => (LTerm_pair (lift_at_depth_in_term t k n)
                                      (lift_at_depth_in_term u k n))
    | (LTerm_fst t) => (LTerm_fst (lift_at_depth_in_term t k n))
    | (LTerm_snd t) => (LTerm_snd (lift_at_depth_in_term t k n))
  end
.

Function: lifts term t with amplitude n
Definition lift_in_term (t: LTerm) (n: nat): LTerm :=
  (lift_at_depth_in_term t 0 n)
.

Function: substitute s for k in i, noted ik\s
Definition subst_in_var (i: nat) (k: nat) (s: LTerm): LTerm :=
  (match_comp_nat3 i k LTerm
    (LTerm_var i)
    (lift_in_term s k)
    (LTerm_var (pred i))
  )
.

Function: substitute s for k in t', noted t'k\s
Fixpoint subst_in_term (t': LTerm) (k: nat) (s: LTerm) {struct t'}: LTerm :=
  match t' with
    | (LTerm_const c) => (LTerm_const c)
    | (LTerm_var i) => (subst_in_var i k s)
    | (LTerm_fun T t) => (LTerm_fun T (subst_in_term t (S k) s))
    | (LTerm_app t u) => (LTerm_app (subst_in_term t k s) (subst_in_term u k s))
    | (LTerm_pair t u) => (LTerm_pair (subst_in_term t k s) (subst_in_term u k s))
    | (LTerm_fst t) => (LTerm_fst (subst_in_term t k s))
    | (LTerm_snd t) => (LTerm_snd (subst_in_term t k s))
  end
.

Typing context
Definition LEnv: Set := (list LType).

Relation: type assignment
Inductive WellTyped: LEnv -> LTerm -> LType -> Prop :=

  | WT_const:
    forall (G: LEnv) (c: LConst) (T: LType),
      (type_of_const c T) ->
      (WellTyped G (LTerm_const c) T)

  | WT_var:
    forall (G: LEnv) (i: nat) (T: LType),
      (List_from G i T) ->
      (WellTyped G (LTerm_var i) T)

  | WT_fun:
    forall (G: LEnv) (t: LTerm) (T U: LType),
      (WellTyped (snoc G T) t U) ->
      (WellTyped G (LTerm_fun T t) (LType_fun T U))

  | WT_app:
    forall (G: LEnv) (t u: LTerm) (T U: LType),
      (WellTyped G t (LType_fun T U)) ->
      (WellTyped G u T) ->
      (WellTyped G (LTerm_app t u) U)

  | WT_pair:
    forall (G: LEnv) (t u: LTerm) (T U: LType),
      (WellTyped G t T) ->
      (WellTyped G u U) ->
      (WellTyped G (LTerm_pair t u) (LType_prod T U))

  | WT_fst:
    forall (G: LEnv) (t: LTerm) (T U: LType),
      (WellTyped G t (LType_prod T U)) ->
      (WellTyped G (LTerm_fst t) T)

  | WT_snd:
    forall (G: LEnv) (t: LTerm) (T U: LType),
      (WellTyped G t (LType_prod T U)) ->
      (WellTyped G (LTerm_snd t) U)
.

Relation: reduction of terms
Inductive RedTerm: LTerm -> LTerm -> Prop :=

  | R_fun:
    forall (T: LType) (t t': LTerm),
      (RedTerm t t') ->
      (RedTerm (LTerm_fun T t) (LTerm_fun T t'))

  | R_app_left:
    forall (t t' u: LTerm),
      (RedTerm t t') ->
      (RedTerm (LTerm_app t u) (LTerm_app t' u))

  | R_app_right:
    forall (t u u': LTerm),
      (RedTerm u u') ->
      (RedTerm (LTerm_app t u) (LTerm_app t u'))

  | R_app_redex:
    forall (T: LType) (t u: LTerm),
      (RedTerm (LTerm_app (LTerm_fun T t) u) (subst_in_term t 0 u))

  | R_pair_left:
    forall (t t' u: LTerm),
      (RedTerm t t') ->
      (RedTerm (LTerm_pair t u) (LTerm_pair t' u))

  | R_pair_right:
    forall (t u u': LTerm),
      (RedTerm u u') ->
      (RedTerm (LTerm_pair t u) (LTerm_pair t u'))

  | R_fst_cong:
    forall (t t': LTerm),
      (RedTerm t t') ->
      (RedTerm (LTerm_fst t) (LTerm_fst t'))

  | R_fst_redex:
    forall (t u: LTerm),
      (RedTerm (LTerm_fst (LTerm_pair t u)) t)

  | R_snd_cong:
    forall (t t': LTerm),
      (RedTerm t t') ->
      (RedTerm (LTerm_snd t) (LTerm_snd t'))

  | R_snd_redex:
    forall (t u: LTerm),
      (RedTerm (LTerm_snd (LTerm_pair t u)) u)
.


Successive variable liftings
Lemma Successive_variable_liftings:
  forall (n1 n2 m: nat) (i: nat) (k: nat),
    (lift_at_depth_in_var (lift_at_depth_in_var i k (n1 + n2)) (k + n2) m) =
    (lift_at_depth_in_var i k (n1 + n2 + m))
.



Successive type liftings (auxiliary)
Lemma Successive_type_liftings_aux:
  forall (n1 n2 m: nat) (t: LTerm) (k: nat),
    (lift_at_depth_in_term (lift_at_depth_in_term t k (n1 + n2)) (k + n2) m) =
    (lift_at_depth_in_term t k (n1 + n2 + m))
.










Permuting type lifting and substitution (auxiliary)
Lemma Permuting_type_lifting_and_substitution_aux:
  forall (s: LTerm) (k1 n: nat) (t: LTerm) (k2: nat),
    (lift_at_depth_in_term (subst_in_term t (k1 + k2) s) k2 n) =
    (subst_in_term (lift_at_depth_in_term t k2 n) (k1 + k2 + n) s)
.

























Lemma Permuting_type_lifting_and_substitution:
  forall (t: LTerm) (i: nat) (s: LTerm) (n: nat),
    (lift_in_term (subst_in_term t i s) n) =
    (subst_in_term (lift_in_term t n) (i + n) s)
.

Lemma Permuting_type_liftings_aux:
  forall (k1 n1 n2: nat) (t: LTerm) (k2: nat),
    (lift_at_depth_in_term (lift_at_depth_in_term t k2 n2) (k1 + n2 + k2) n1) =
    (lift_at_depth_in_term (lift_at_depth_in_term t (k1 + k2) n1) k2 n2)
.

















Permuting type lifting and substitution 2 (auxiliary)
Lemma Permuting_type_lifting_and_substitution_2_aux:
  forall (s: LTerm) (k1 n: nat) (t: LTerm) (k2: nat),
    (lift_at_depth_in_term (subst_in_term t k2 s) (k1 + k2) n) =
    (subst_in_term (lift_at_depth_in_term t (S (k1 + k2)) n) k2
      (lift_at_depth_in_term s k1 n))
.






























Lemma Type_lifting_stronger_than_substitution_aux:
  forall (n d: nat) (s t: LTerm) (k: nat),
    (subst_in_term (lift_at_depth_in_term t k (S (n + d))) (n + k) s) =
    (lift_at_depth_in_term t k (n + d))
.

















Lemma Type_lifting_stronger_than_substitution:
  forall (n d: nat) (s t: LTerm),
    (subst_in_term (lift_in_term t (S (n + d))) n s) =
    (lift_in_term t (n + d))
.


Permuting type substitutions
Lemma Permuting_type_substitutions:
  forall (s s': LTerm) (k: nat) (t: LTerm) (n: nat),
    (subst_in_term (subst_in_term t n s) (n + k) s') =
    (subst_in_term (subst_in_term t (S (n + k)) s') n (subst_in_term s k s'))
.


































Lemma Substitution_in_reduction:
  forall (s t t': LTerm),
    (RedTerm t t') ->
    forall (k: nat),
      (RedTerm (subst_in_term t k s) (subst_in_term t' k s))
.














Inductive RedTermStar: LTerm -> LTerm -> Prop :=
  | RedTerm_step: forall (t t': LTerm), (RedTerm t t') -> (RedTermStar t t')
  | RedTerm_refl: forall (t: LTerm), (RedTermStar t t)
  | RedTerm_trans: forall (t u t': LTerm), (RedTermStar t u) -> (RedTermStar u t') ->
    (RedTermStar t t')
.


Lemma RS_fun:
  forall (t t': LTerm) (T: LType),
    (RedTermStar t t') ->
    (RedTermStar (LTerm_fun T t) (LTerm_fun T t'))
.




Lemma RS_app_left:
  forall (t t' u: LTerm),
    (RedTermStar t t') ->
    (RedTermStar (LTerm_app t u) (LTerm_app t' u))
.




Lemma RS_app_right:
  forall (t u u': LTerm),
    (RedTermStar u u') ->
    (RedTermStar (LTerm_app t u) (LTerm_app t u'))
.




Lemma RS_pair_left:
  forall (t t' u: LTerm),
    (RedTermStar t t') ->
    (RedTermStar (LTerm_pair t u) (LTerm_pair t' u))
.




Lemma RS_pair_right:
  forall (t u u': LTerm),
    (RedTermStar u u') ->
    (RedTermStar (LTerm_pair t u) (LTerm_pair t u'))
.




Lemma RS_fst_cong:
  forall (t t': LTerm),
    (RedTermStar t t') ->
    (RedTermStar (LTerm_fst t) (LTerm_fst t'))
.




Lemma RS_snd_cong:
  forall (t t': LTerm),
    (RedTermStar t t') ->
    (RedTermStar (LTerm_snd t) (LTerm_snd t'))
.




Lemma Reduction_in_lifting:
  forall (t t': LTerm) (n: nat),
    (RedTerm t t') ->
    forall (k: nat),
      (RedTerm (lift_at_depth_in_term t k n) (lift_at_depth_in_term t' k n))
.
















Lemma Reduction_in_substitution:
  forall (s s': LTerm),
    (RedTerm s s') ->
    forall (t: LTerm) (k: nat),
      (RedTermStar (subst_in_term t k s) (subst_in_term t k s'))
.


















Lemma Substitution_in_reduction_star:
  forall (s t t': LTerm) (k: nat),
    (RedTermStar t t') ->
    (RedTermStar (subst_in_term t k s) (subst_in_term t' k s))
.




Lemma Reduction_in_substitution_star:
  forall (s s': LTerm) (t: LTerm) (k: nat),
    (RedTermStar s s') ->
    (RedTermStar (subst_in_term t k s) (subst_in_term t k s'))
.




Lemma Reduction_and_substitution_star:
  forall (t t' s s': LTerm) (k: nat),
    (RedTermStar t t') ->
    (RedTermStar s s') ->
    (RedTermStar (subst_in_term t k s) (subst_in_term t' k s'))
.




Weakening of declaration by the right
Lemma Weakening_of_declaration_by_the_right:
  forall (G1 G2 G3: LEnv) (i: nat) (T: LType),
    (List_from (G1 ++ G3) i T) ->
    (List_from
      (G1 ++ G2 ++ G3)
      (lift_at_depth_in_var i (length G3) (length G2))
      T)
.







Weakening of well-typing by the right (auxiliary)
Lemma Weakening_of_well_typing_by_the_right_aux:
  forall (G1 G2 G: LEnv) (t: LTerm) (T: LType),
    (WellTyped G t T) ->
    forall (G3: LEnv),
      G = (G1 ++ G3) ->
      (WellTyped (G1 ++ G2 ++ G3)
         (lift_at_depth_in_term t (length G3) (length G2)) T)
.


















Weakening_of_well-typing by the right
Lemma Weakening_of_well_typing_by_the_right:
  forall (G G': LEnv) (t: LTerm) (T: LType),
    (WellTyped G t T) ->
    (WellTyped (G ++ G') (lift_in_term t (length G')) T)
.


Substitution preserves typing
Lemma Substitution_preserves_typing:
  forall (G1 G2: LEnv) (T U: LType) (t u: LTerm),
    (WellTyped G1 u U) ->
    (WellTyped (G1 ++ (U :: G2)) t T) ->
    (WellTyped (G1 ++ G2) (subst_in_term t (length G2) u) T)
.















Lemma Substitution_preserves_typing_snoc:
  forall (G : LEnv) (T U : LType) (t u: LTerm),
    (WellTyped G u U) ->
    (WellTyped (snoc G U) t T) ->
    (WellTyped G (subst_in_term t 0 u) T)
.



Weakening of well-typing by the left
Lemma Weakening_of_well_typing_by_the_left:
  forall (G1 G2: LEnv) (t: LTerm) (T: LType),
    (WellTyped G2 t T) ->
    (WellTyped (G1 ++ G2) t T)
.









Theorem Subject_reduction:
  forall (G: LEnv) (t t': LTerm) (T: LType),
    (WellTyped G t T) ->
    (RedTerm t t') ->
    (WellTyped G t' T)
.













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




End LambdaCalculus.