# path.thm

%% 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.