%% Paths through lambda terms
%%
%% Here we prove: if all the paths in the lambda term X also exist in
%% the lambda term Y then X = Y.
%%
%% This example would really benefit from some polymorphism
Specification "path".
Close tm, path.
Define tm_var : tm -> prop by
nabla x, tm_var x.
Define path_var : path -> prop by
nabla x, path_var x.
Theorem member_prune_tm : forall E (L:olist), nabla (x:tm),
member (E x) L -> exists F, E = y\F.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Theorem member_prune_path : forall E (L:olist), nabla (x:path),
member (E x) L -> exists F, E = y\F.
induction on 1. intros. case H1.
search.
apply IH to H2. search.
Define ctxs : olist -> olist -> prop by
ctxs nil nil ;
nabla x p, ctxs (tm x :: L) (path x p :: K) := ctxs L K.
Theorem ctxs_member1 : forall X L K,
ctxs L K -> member X L ->
exists E F, X = tm E /\ tm_var E /\ member (path E F) K /\ path_var F.
induction on 1. intros. case H1.
case H2.
case H2.
search.
apply IH to H3 H4. search.
Theorem ctxs_member2 : forall X L K,
ctxs L K -> member X K -> exists E F, X = path E F /\ tm_var E /\ path_var F.
induction on 1. intros. case H1.
case H2.
case H2.
search.
apply IH to H3 H4. search.
Theorem member_path_unique : forall L K X Y F,
ctxs L K -> member (path X F) K -> member (path Y F) K -> X = Y.
induction on 2. intros. case H2.
case H3.
search.
case H1. apply member_prune_path to H4.
case H3.
case H1. apply member_prune_path to H4.
case H1. apply IH to H6 H4 H5. search.
Theorem path_exists : forall L K M,
ctxs L K -> {L |- tm M} -> exists P, {K |- path M P}.
induction on 2. intros. case H2.
apply IH to H1 H3. search.
assert ctxs (tm n1 :: L) (path n1 n2 :: K).
apply IH to H4 H3. search.
apply ctxs_member1 to H1 H4. case H3. search.
Theorem path_app : forall L K M N Y,
ctxs L K -> {L |- tm (app M N)} ->
(forall P, {K |- path (app M N) P} -> {K |- path Y P}) ->
exists YM YN, Y = app YM YN.
intros. case H2.
apply path_exists to H1 H4.
assert {K |- path (app M N) (left P)}.
apply H3 to H7.
case H8.
search.
apply ctxs_member2 to H1 H10. case H12. case H9.
apply ctxs_member1 to H1 H5. case H4. case H6.
Theorem path_abs : forall L K R Y,
ctxs L K -> {L |- tm (abs R)} ->
(forall P, {K |- path (abs R) P} -> {K |- path Y P}) ->
exists YR, Y = abs YR.
intros. case H2.
assert ctxs (tm n1 :: L) (path n1 n2 :: K).
apply path_exists to H5 H4.
assert {K |- path (abs R) (bnd P)}.
apply H3 to H7.
case H8.
search.
apply ctxs_member2 to H1 H10. case H9. case H12.
apply ctxs_member1 to H1 H5. case H4. case H6.
Theorem path_equal : forall L K X Y,
ctxs L K -> {L |- tm X} ->
(forall P, {K |- path X P} -> {K |- path Y P}) -> X = Y.
induction on 2. intros. case H2 (keep).
% X = app M N
apply path_app to H1 H2 H3.
% Apply the IH to M
assert forall P, {K |- path M P} -> {K |- path YM P}.
intros.
assert {K |- path (app M N) (left P)}.
apply H3 to H7. case H8.
search.
apply ctxs_member2 to H1 H10. case H12. case H9.
apply IH to H1 H4 H6.
% Apply the IH to M
assert forall P, {K |- path N P} -> {K |- path YN P}.
intros.
assert {K |- path (app M N) (right P)}.
apply H3 to H8. case H9.
search.
apply ctxs_member2 to H1 H11. case H13. case H10.
apply IH to H1 H5 H7.
% Finish this case
search.
% X = abs R
apply path_abs to H1 H2 H3.
% Apply the IH to (R n1)
assert forall P, {K, path n1 n2 |- path (R n1) P} ->
{K, path n1 n2 |- path (YR n1) P}.
intros.
assert {K |- path (abs R) (bnd P)}.
apply H3 to H6. case H7.
search.
apply ctxs_member2 to H1 H9. case H11. case H8.
assert ctxs (tm n1 :: L) (path n1 n2 :: K).
apply IH to H6 H4 H5.
% Finish this case
search.
% X is a variable
apply ctxs_member1 to H1 H5.
case H4.
assert {K |- path X F1}.
apply H3 to H9.
case H8. case H10.
apply ctxs_member2 to H1 H12.
case H11.
apply member_path_unique to H1 H7 H12. search.
