# Syntax of the weak call-by-value lambda calculus

Inductive term : Type :=
| var (n : nat) : term
| app (s : term) (t : term) : term
| lam (s : term).

Coercion app : term >-> Funclass.
Coercion var : nat >-> term.

Notation "'#' v" := (var v) (at level 1).
Notation "(λ s )" := (lam s) (right associativity, at level 0).

Instance term_eq_dec : eq_dec term.

Definition term_eq_dec_proc s t := if decision (s = t) then true else false.

# Notation using binders

Inductive bterm : Type :=
| bvar (x : string) : bterm
| bapp (s t : bterm) : bterm
| blam (x : string) (s : bterm) : bterm
| bter (s : term) : bterm.

Instance eq_dec_string : eq_dec string.

Fixpoint convert' (F : list string) (s : bterm) : term := match s with
| bvar xmatch pos x F with None#100 | Some t# t end
| bapp s tapp (convert' F s) (convert' F t)
| blam x slam (convert' (x:: F) s)
| bter tt
end.

Coercion bvar : string >-> bterm.
Coercion bapp : bterm >-> Funclass.
Definition convert := convert' [].
Coercion convert : bterm >-> term.

Notation ".\ x , .. , y ; t" := ((blam x .. (blam y t) .. )) (at level 100, right associativity).
Notation "'λ' x , .. , y ; t" := ((blam x .. (blam y t) .. )) (at level 100, right associativity).

Notation "'!' s" := (bter s) (at level 0).

# Important terms

Definition R := (lam (lam (#0 (lam (#2 #2 #1 #0)))))
(lam (lam (#0 (lam (#2 #2 #1 #0))))).

Definition I : term := .\"x"; "x".
Definition K : term := .\"x","y"; "x".

Definition omega : term := .\"x"; "x" "x".
Definition Omega : term := omega omega.

# Substitution

Fixpoint subst (s : term) (k : nat) (u : term) :=
match s with
| var nif decision (n = k) then u else (var n)
| app s tapp (subst s k u) (subst t k u)
| lam slam (subst s (S k) u)
end.

# Important definitions

Definition closed s := n u, subst s n u = s.

Definition lambda s := t, s = lam t.

Definition proc s := closed s lambda s.

Lemma lambda_lam s : lambda (lam s).

## Alternative definition of closedness

Inductive dclosed : nattermProp :=
| dclvar k n : k > ndclosed k (var n)
| dclApp k s t : dclosed k sdclosed k tdclosed k (s t)
| dcllam k s : dclosed (S k) sdclosed k (lam s).

Lemma dclosed_closed_k s k u : dclosed k ssubst s k u = s.

Lemma dclosed_gt k s : dclosed k s m, m > kdclosed m s.

Lemma dclosed_closed s k u : dclosed 0 ssubst s k u = s.

Lemma closed_k_dclosed k s : ( n u, n ksubst s n u = s) → dclosed k s.

Lemma closed_dcl s : closed s dclosed 0 s.

Lemma closed_app (s t : term) : closed (s t) → closed s closed t.

Lemma dec_dclosed k s : dec (dclosed k s).

# Reduction

Reserved Notation "s '>>' t" (at level 50).

Inductive step : termtermProp :=
| stepApp s t : app (lam s) (lam t) >> subst s 0 (lam t)
| stepAppR s t t' : t >> t'app s t >> app s t'
| stepAppL s s' t : s >> s'app s t >> app s' t
where "s '>>' t" := (step s t).

Lemma closed_subst s t k : dclosed (S k) sdclosed k tdclosed k (subst s k t).

Lemma closed_step s t : s >> tclosed sclosed t.

Lemma comb_proc_red s : closed sproc s t, s >> t.

Goal s, closed s → ((¬ t, s >> t) proc s).

# Properties of the reduction relation

Theorem uniform_confluence : uniform_confluent step.

Notation "x '>^' n y" := (pow step n x y) (at level 50).

Lemma confluence : confluent step.

Lemma step_value s v :
lambda v → (lam s) v >> subst s 0 v.

## Properties of the reflexive, transitive closure of reduction

Notation "s '>*' t" := (star step s t) (at level 50).

Instance star_PreOrder : PreOrder (star step).

Lemma star_trans_l s s' t :
s >* s's t >* s' t.

Lemma star_trans_r s s' t :
s >* s' → (lam t) s >* (lam t) s'.

# Equivalence

Reserved Notation "s '==' t" (at level 50).

Inductive equiv : termtermProp :=
| eqStep s t : step s ts == t
| eqRef s : s == s
| eqSym s t : t == ss == t
| eqTrans s t u: s == tt == us == u
where "s '==' t" := (equiv s t).

## Properties of the equivalence relation

Instance equiv_Equivalence : Equivalence equiv.

Lemma equiv_ecl s t : s == t ecl step s t.

Lemma church_rosser s t : s == t u, s >* u t >* u.

Lemma star_equiv s t :
s >* ts == t.

Lemma equiv_lambda s t : s == (lam t)s >* (lam t).

Lemma equiv_lambda' u t : lambda tu == tu >* t.

Lemma eqStarT s t u : s >* tt == us == u.

Lemma eqApp s s' u u' : s == s'u == u's u == s' u'.

Instance equiv_app_proper :
Proper (equiv ==> equiv ==> equiv) app.

# Definition of convergence

Definition converges s := t, s == lam t.

Lemma converges_equiv s t : s == t → (converges s converges t).

Instance converges_proper :
Proper (equiv ==> iff) converges.

Lemma eq_lam s t : lam s == lam t s = t.

Lemma unique_normal_forms (s t t' : term) : s == lam ts == lam t'lam t = lam t'.

# Eta expansion

Lemma Eta (s : term ) t : closed slambda t → (lam (s #0)) t == s t.

# Useful lemmas

Lemma pow_trans_lam t v s k n :
pow step n t (lam v) → pow step (S k) t s m, m < n pow step m s (lam v).

Lemma powSk t t' s : t >> t't' >* s k, pow step (S k) t s.