# Library LN_STLC_basic_Infrastructure

Set Implicit Arguments.

Require Import LNameless_Isomorphism.
Require Import LNameless_STLC_Iso.
Require Import LN_Template_One_Sort.
Require Export LN_STLC_basic_Definitions.

## Pure Lambda Calculus

Reference: Chargueraud's POPLmark contribution using Locally Nameless style and cofinite quantification

Many of the generic properties about substitution, environments are already proved in a generic

Notation "[ z ~> u ] t" := (Tfsubst t z u) (at level 68).

## Regularity of relations

A typing relation holds only if the environment has no duplicated keys and the pre-term is locally-closed.

Lemma typing_regular : forall E e T,
typing E e T -> uniq E /\ TwfT e.
Proof.
split; induction H; eauto; try gconstructor.
pick_fresh y; forward~ H0 as Huniq; eauto; inversion* Huniq.
Qed.

The value predicate only holds on locally-closed terms.

Lemma value_regular : forall e,
value e -> TwfT e.
Proof.
induction 1; auto*.
Qed.

A reduction relation only holds on pairs of locally-closed terms.

Lemma TwfT_abs_inv : forall (T:trm),
TwfT (trm_abs T) ->
exists L, forall x, x `notin` L -> TwfT (T ^ x).
Proof.
intros.
unfold TwfT in * |-; simpl in * |-.
dependent destruction H.
dependent destruction H; inversion H0; subst; dependent destruction H1.
dependent destruction H; intuition. simpl in * |-.
exists L; intros.
generalize (H1 x H2); intro H3; clear H1.
dependent destruction H3; auto.
gunfold; auto.
Qed.

Lemma red_regular : forall e e',
red e e' -> TwfT e /\ TwfT e'.
Proof with eauto using value_regular.
split; induction H; try gconstructor; eauto...
clear NotInTac NotInTac0.

generalize (TwfT_abs_inv H); intro H2; inversion H2.
pick fresh y for (x `union` Tfv t1);destruct_notin.
assert (TwfT (trm_fvar a)); [gconstructor | idtac].
rewrite (Tbfsubst_var_intro t1 (trm_fvar a) NotInTac); simpl.
apply TwfT_Tfsubst; eauto.

generalize (value_regular H0); intros.
generalize (TwfT_abs_inv H); intro H2; inversion H2.
pick fresh y for (x `union` Tfv t1);destruct_notin.
rewrite (Tbfsubst_var_intro t1 t2 NotInTac); simpl.
apply TwfT_Tfsubst; auto.
Qed.