Equivalence of single and double eigenvariable definitions of copy

Executable Specification

[View copy.sig] [View copy.mod]
sig copy.

kind    tm             type.

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

type    copy, copy2    tm -> tm -> o.

module copy.

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

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

Reasoning

[View copy.thm]

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

Specification "copy".

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


Define ctxs : olist -> olist -> prop by
  ctxs nil nil ;
  ctxs (copy X Y :: L1) (copy2 X Y :: L2) := ctxs L1 L2.

Define name : tm -> prop by
  nabla x, name x.

Theorem ctx_mem1 : forall F L1 L2,
  ctxs L1 L2 -> member F L1 -> exists X Y, F = copy X Y.

Theorem ctx_mem2 : forall F L1 L2,
  ctxs L1 L2 -> member F L2 -> exists X Y, F = copy2 X Y.


%% copy implies copy2

% show that copy2 could descend under abstractions like copy

Theorem copy2_align : forall M N K L, nabla z,
  ctxs K L ->
  {L, copy2 z z |- copy2 (M z) (N z)} ->
    nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}.

Theorem ctxs_member1 : forall X Y L K,
  ctxs L K -> member (copy X Y) L -> member (copy2 X Y) K.

Theorem copy_copy2 : forall L K M N,
  ctxs L K -> {L |- copy M N} -> {K |- copy2 M N}.


%% copy2 implies copy

% show that copy could descend under abstractions like copy2

Theorem copy_align : forall M N L, nabla x y,
  {L, copy x y |- copy (M x) (N y)} ->
    nabla z, {L, copy z z |- copy (M z) (N z)}.

Theorem ctxs_member2 : forall X Y L K,
  ctxs L K -> member (copy2 X Y) K -> member (copy X Y) L.

Theorem copy2_copy : forall L K M N,
  ctxs L K -> {K |- copy2 M N} -> {L |- copy M N}.