Equivalence of single and double eigenvariable definitions of copy

Executable Specification

[View copy.mod]

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] [Show All Proofs] [Hide All Proofs]

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

%% Equivalence of single and double eigenvariable definitions of copy

Theorem member_nabla : forall L E, nabla x,
  member (E x) L -> exists E1, E = (y\E1). [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.

Define ctxs nil nil.
Define ctxs (copy X Y :: L1) (copy2 X Y :: L2) := ctxs L1 L2.


%% copy implies copy2

% show that copy2 could descend under abstractions like copy

Theorem copy2_align : forall M N L, nabla z,
  {L, copy2 z z |- copy2 (M z) (N z)} ->
    nabla x y, {L, copy2 x y |- copy2 (M x) (N y)}. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  case H2.
    search.
    apply member_nabla to H3. search.
  apply IH to H2. apply IH to H3. search.
  apply IH to H2. search.

Theorem ctxs_member1 : forall X Y L K,
  ctxs L K -> member (copy X Y) L -> member (copy2 X Y) K. [Show Proof][Hide Proof]
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}. [Show Proof][Hide Proof]
induction on 2. intros. case H2.
  apply ctxs_member1 to H1 H3. search.
  apply IH to H1 H3. apply IH to H1 H4. search.
  apply IH to _ H3. apply copy2_align to 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)}. [Show Proof][Hide Proof]
induction on 1. intros. case H1.
  case H2.
    search.
    apply member_nabla to H3. apply member_nabla to H3. search.
  apply IH to H2. apply IH to H3. search.
  apply IH to H2. search.

Theorem ctxs_member2 : forall X Y L K,
  ctxs L K -> member (copy2 X Y) K -> member (copy X Y) L. [Show Proof][Hide Proof]
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}. [Show Proof][Hide Proof]
induction on 2. intros. case H2.
  apply ctxs_member2 to H1 H3. search.
  apply IH to H1 H3. apply IH to H1 H4. search.
  apply IH to _ H3. apply copy_align to H4. search.