% Some examples of reasoning about lambda terms
% 
% Alwen Tiu
% 21 April 2008
%
% This specification is written for and verified in the Abella proof assistant. 
% The prover can be found here:
%   http://abella.cs.umn.edu/
%
% This specification is verified in Abella version 1.1.

Define nabla x, name x.

Define term M := name M.
Define term (app M N) := term M /\ term N.
Define term (lam M) := nabla x, term (M x).

Define fresh A B := name A /\ name B /\ (A = B -> false).
Define fresh A (app M N) := fresh A M /\ fresh A N.
Define fresh A (lam M) := nabla x, fresh A (M x).

Define abstract A A (x\x) := name A.
Define abstract A B (x\B) := name A /\ name B /\ (A = B -> false).
Define abstract A (app M N) (x\ app (R x) (T x)) := abstract A M R /\ abstract A N T.
Define abstract A (lam M) (x\ lam (T x)) := nabla y, abstract A (M y) (x\ T x y).

Define subst X M X M := name X.
Define subst X M Y Y := name X /\ name Y /\ (X = Y -> false).
Define subst X M (app N1 N2) (app R1 R2) := subst X M N1 R1 /\ subst X M N2 R2.
Define subst X M (lam N) (lam R) := nabla y, subst X M (N y) (R y).


% Freshness and scopes
Theorem forall M, nabla x, term M -> fresh x M.
induction on 1.
intros. case H1. case H2.
unfold. search. search. intros. case H3.
apply IH to H2 with x = n1.
apply IH to H3 with x = n1.
search.
apply IH to H2 with x = n2.
search.

% Closure under meta level application

Theorem clo1 : forall M N, nabla x, term (M x) -> term N -> term (M N).
induction on 1.
intros. case H1. case H3. search. search.
apply IH to H3 H2.
apply IH to H4 H2.
search.
apply IH to H3 H2 with M = (x\M1 x n2), N = N, x = n1.
search.

Theorem forall M N, term (lam M) -> term N -> term (M N).
intros. case H1. case H3. apply clo1 to H3 H2. search.

Theorem clo2 : forall A M N, nabla x, name A -> term (M x) -> fresh A N -> fresh A (M x) -> fresh A (M N).
induction on 2. intros. case H2. case H1. case H5.
search. search. search. 
case H4. case H8. apply IH to H1 H5 H3 H7. apply IH to H1 H6 H3 H8.
search. case H4. case H7. apply IH to H1 H5 H3 H6. search.

Theorem forall A M N, name A -> term (lam M) -> fresh A N -> fresh A (lam M) -> fresh A (M N).
intros. case H2. case H5. case H4. case H7. 
apply clo2 to H1 H5 H3 H6. search.

% Abstractions

Theorem forall M, nabla x, term (M x) -> abstract x (M x) M.
induction on 1.
intros. case H1. case H2. search. unfold.
search. search. intros. case H3. search.
apply IH to H2. apply IH to H3. search.
apply IH to H2. search.


Theorem forall M, nabla x, forall N, term (M x) -> abstract x (M x) N -> M = N.
induction on 1.
intros. case H1. case H3. case H2. search.
case H2. search. apply H6 to _. case H2.
case H6. apply IH to H3 H5 with M = M1, x = n1, N = R n1.
apply IH to H4 H6 with M = N1, x = n1, N = T n1.
search. case H2. case H5.
apply IH to H3 H4 with M = (x\M1 x n2), x = n1, N = (x\T n1 x n2).
search.

Theorem forall A M N, name A -> term M -> abstract A M N -> fresh A (lam N).
induction on 2.
intros. case H1. case H2. case H4. case H3.
assert fresh n1 n2. unfold. search. search. search. intros. case H8.
search. case H3. assert fresh n1 n2. unfold.
search. search. intros.  case H6. search.
apply H7 to _. case H3. case H7.
assert name n1. apply IH to H8 H4 H6. apply IH to H8 H5 H7.
case H9.  case H12. case H10. case H13.
search. case H3. case H6. assert name n1. apply IH to H6 H4 H5.
case H7. case H9. search.

% Substitution

Theorem forall M N, nabla y, forall R, term M -> term (N y) -> subst y M (N y) R -> R = (N M).
induction on 2.
intros.
case H2.
case H4.
case H3.
search.
case H3.
search.
apply H7 to _.
case H3.
case H7.
apply IH to H1 H4 H6 with M = M, N = M1, y = n1, R = R1 n1.
apply IH to H1 H5 H7 with M = M, N = N1, y = n1, R = R2 n1.
search.
case H3.
case H6.
apply IH to H1 H4 H5 with M = M, N = (x\M1 x n2), y = n1, R = R1 n1 n2.
search.


Theorem forall M N, nabla y, term M -> term (N y) -> subst y M (N y) (N M).
induction on 2.
intros. case H2. case H3. search.
unfold. search. search. intros.
case H4. search. 
apply IH to H1 H3. apply IH to H1 H4. search.
apply IH to H1 H3. search.