Paths through lambda terms

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.


Theorem member_prune_path : forall E L, nabla (x:path),
  member (E x) L -> exists F, E = y\F.


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.


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.


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.


Theorem path_exists : forall L K M,
  ctxs L K -> {L |- tm M} -> exists P, {K |- path M P}.

  

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.


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.


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.