%% Properties of PCF
Specification "pcf".
%% Subject reduction
Theorem subject_reduction : forall E V T,
{eval E V} -> {of E T} -> {of V T}.
induction on 1. intros. case H1.
search.
search.
search.
case H2. apply IH to H3 H4. search.
case H2. search.
case H2. apply IH to H3 H4. case H5. search.
case H2. search.
case H2. search.
case H2. apply IH to H4 H6. search.
case H2. apply IH to H4 H7. search.
search.
% P = app M N
case H2. apply IH to H3 H5. case H7.
inst H8 with n1 = N. cut H9 with H6.
apply IH to H4 H10. search.
% P = rec T1 R
case H2 (keep).
inst H4 with n1 = rec T R.
cut H5 with H2.
apply IH to H3 H6. search.
%% Type uniqueness
Theorem member_prune : forall (L:olist) E, nabla (x:tm),
member (E x) L -> exists F, E = x\F.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Define ctx : olist -> prop by
ctx nil ;
nabla x, ctx (of x A :: L) := ctx L.
Define name : tm -> prop by
nabla x, name x.
Theorem ctx_member : forall E L,
ctx L -> member E L -> exists X A, E = of X A /\ name X.
induction on 1. intros. case H1.
case H2.
case H2.
search.
apply IH to H3 H4. search.
Theorem ctx_uniq : forall L E T1 T2,
ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2.
induction on 1. intros. case H1.
case H2.
case H2.
case H3.
search.
apply member_prune to H5.
case H3.
apply member_prune to H5.
apply IH to H4 H5 H6. search.
% Some basic automation with regards to ctx_member would be great here
Theorem type_uniq : forall L E T1 T2,
ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.
induction on 2. intros. case H2.
% E = zero
case H3.
search.
apply ctx_member to H1 H5. case H4. case H6.
% E = tt
case H3.
search.
apply ctx_member to H1 H5. case H4. case H6.
% E = ff
case H3.
search.
apply ctx_member to H1 H5. case H4. case H6.
% E = succ M
case H3.
search.
apply ctx_member to H1 H6. case H5. case H7.
% E = pred M
case H3.
search.
apply ctx_member to H1 H6. case H5. case H7.
% E = is_zero M
case H3.
search.
apply ctx_member to H1 H6. case H5. case H7.
% E = if M N1 N2
case H3.
apply IH to H1 H5 H8. search.
apply ctx_member to H1 H8. case H7. case H9.
% E = abs T R
case H3.
apply IH to _ H4 H5. search.
apply ctx_member to H1 H6. case H5. case H7.
% E = app M N
case H3.
apply IH to H1 H4 H6. search.
apply ctx_member to H1 H7. case H6. case H8.
% E = rec T1 R
case H3.
search.
apply ctx_member to H1 H6. case H5. case H7.
% E is variable
apply ctx_member to H1 H5. case H4. case H6.
case H3.
apply ctx_member to H1 H8. case H7.
apply ctx_uniq to H1 H5 H8. search.
Set search_depth 30.
Query
Add = (rec (arr num (arr num num))
(add\ abs num x\ abs num y\
if (is_zero x) y (succ (app (app add (pred x)) y))))
/\
Two = succ (succ zero) /\
Three = succ (succ (succ zero)) /\
{eval (app (app Add Two) Three) V}.
