# Executable Specification

[View path.sig] [View path.mod]
```sig path.

kind    tm, path          type.

type    app               tm -> tm -> tm.
type    abs               (tm -> tm) -> tm.

type    done              path.
type    left, right       path -> path.
type    bnd               (path -> path) -> path.

type    tm                tm -> o.
type    path              tm -> path -> o.

```
```module path.

tm (app M N) :- tm M, tm N.
tm (abs R) :- pi x\ tm x => tm (R x).

path (app M N) (left P) :- path M P.
path (app M N) (right P) :- path N P.
path (abs R) (bnd S) :- pi x\ pi p\ path x p => path (R x) (S p).

```

# Reasoning

[View path.thm]

Click on a command or tactic to see a detailed view of its use.

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