# copy.thm

%% Equivalence of single and double eigenvariable definitions of copy Specification "copy". Theorem member_fresh : forall (L:olist) E, nabla (x:tm), 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 ; 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. induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. Theorem ctx_mem2 : forall F L1 L2, ctxs L1 L2 -> member F L2 -> exists X Y, F = copy2 X Y. induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. %% 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)}. induction on 2. intros. case H2. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. search. case H4. case H3. search. apply member_fresh to H5. apply ctx_mem2 to H1 H5. case H3. search. Theorem ctxs_member1 : forall X Y L K, ctxs L K -> member (copy X Y) L -> member (copy2 X Y) K. induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. Theorem copy_copy2 : forall L K M N, ctxs L K -> {L |- copy M N} -> {K |- copy2 M N}. induction on 2. intros. case H2. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. apply copy2_align to H1 H4. search. apply ctx_mem1 to H1 H4. case H3. apply ctxs_member1 to H1 H4. search. %% 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)}. intros. inst H1 with n2 = n1. search. Theorem ctxs_member2 : forall X Y L K, ctxs L K -> member (copy2 X Y) K -> member (copy X Y) L. induction on 1. intros. case H1. case H2. case H2. search. apply IH to H3 H4. search. Theorem copy2_copy : forall L K M N, ctxs L K -> {K |- copy2 M N} -> {L |- copy M N}. induction on 2. intros. case H2. apply IH to H1 H3. apply IH to H1 H4. search. apply IH to _ H3. apply copy_align to H4. search. apply ctx_mem2 to H1 H4. case H3. apply ctxs_member2 to H1 H4. search.