Correctness for LLambda subst predicate

Executable Specification

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.

Reasoning

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.
induction on 1. intros. case H1.
  case H2.
  case H2.
    search.
    apply IH to H3 H4. search.
Theorem ctx_member2 : forall L K E,
  ctx L K -> member E K -> exists T, E = copy T T.
induction on 1. intros. case H1.
  case H2.
  case H2.
    search.
    apply IH to H3 H4. search.
Theorem copy_id :
  forall L K T, ctx L K -> {L |- term T} -> {K |- copy T T}.
induction on 2. intros. case H2.
  apply IH to H1 H3. apply IH to H1 H4. search.
  apply IH to _ H3.
    search.
  apply ctx_member1 to H1 H4. case H3. search.
Theorem copy_eq : forall L K T S, ctx L K -> {K |- copy T S} -> T = S.
induction on 2. intros. case H2.
  apply IH to H1 H3. apply IH to H1 H4. search.
  apply IH to _ H3. search.
  apply ctx_member2 to H1 H4. case H3. search.
Theorem subst : forall R T S, {term T} -> {subst R T S} -> R T = S.
intros.
case H2.
apply copy_id to _ H1.
inst H3 with n1 = T.
cut H5 with H4.
apply copy_eq to _ H6.
search.