Correctness for LLambda subst predicate

Executable Specification

[View subst.sig] [View subst.mod]
sig subst.

kind    tm      type.

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

type    term    tm -> o.
type    copy    tm -> tm -> o.
type    subst   (tm -> tm) -> tm -> tm -> o.

module subst.

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

copy (app N M) (app P Q) :- copy N P, copy M Q.
copy (abs R) (abs S) :- pi x\ copy x x => copy (R x) (S x).

subst R T S :- pi x\ copy x T => copy (R x) S.


[View subst.thm]

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

Specification "subst".

Define ctx : olist -> olist -> prop by
  ctx nil nil ;
  ctx (term X :: L) (copy X X :: K) := ctx L K.

Theorem ctx_member1 : forall L K E,
  ctx L K -> member E L -> exists T, E = term T /\ member (copy T T) K.

Theorem ctx_member2 : forall L K E,
  ctx L K -> member E K -> exists T, E = copy T T.

Theorem copy_id :
  forall L K T, ctx L K -> {L |- term T} -> {K |- copy T T}.

Theorem copy_eq : forall L K T S, ctx L K -> {K |- copy T S} -> T = S.

Theorem subst : forall R T S, {term T} -> {subst R T S} -> R T = S.