Library Lvw
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.
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 x ⇒ match pos x F with None ⇒ #100 | Some t ⇒ # t end
| bapp s t ⇒ app (convert' F s) (convert' F t)
| blam x s ⇒ lam (convert' (x:: F) s)
| bter t ⇒ t
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).
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.
Fixpoint subst (s : term) (k : nat) (u : term) :=
match s with
| var n ⇒ if decision (n = k) then u else (var n)
| app s t ⇒ app (subst s k u) (subst t k u)
| lam s ⇒ lam (subst s (S k) u)
end.
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).
Inductive dclosed : nat → term → Prop :=
| dclvar k n : k > n → dclosed k (var n)
| dclApp k s t : dclosed k s → dclosed k t → dclosed k (s t)
| dcllam k s : dclosed (S k) s → dclosed k (lam s).
Lemma dclosed_closed_k s k u : dclosed k s → subst s k u = s.
Lemma dclosed_gt k s : dclosed k s → ∀ m, m > k → dclosed m s.
Lemma dclosed_closed s k u : dclosed 0 s → subst s k u = s.
Lemma closed_k_dclosed k s : (∀ n u, n ≥ k → subst 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).
Reserved Notation "s '>>' t" (at level 50).
Inductive step : term → term → Prop :=
| 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) s → dclosed k t → dclosed k (subst s k t).
Lemma closed_step s t : s >> t → closed s → closed t.
Lemma comb_proc_red s : closed s → proc s ∨ ∃ t, s >> t.
Goal ∀ s, closed s → ((¬ ∃ t, s >> t) ↔ proc s).
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.
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'.
Reserved Notation "s '==' t" (at level 50).
Inductive equiv : term → term → Prop :=
| eqStep s t : step s t → s == t
| eqRef s : s == s
| eqSym s t : t == s → s == t
| eqTrans s t u: s == t → t == u → s == u
where "s '==' t" := (equiv s t).
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 >* t → s == t.
Lemma equiv_lambda s t : s == (lam t) → s >* (lam t).
Lemma equiv_lambda' u t : lambda t → u == t → u >* t.
Lemma eqStarT s t u : s >* t → t == u → s == 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 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 t → s == lam t' → lam t = lam t'.