module debruijn.
add z C C.
add (s A) B (s C) :- add A B C.
% H here is the height (depth) of lambda abstractions
ho2db (app M N) H (dapp DM DN) :- ho2db M H DM, ho2db N H DN.
ho2db (lam R) H (dlam DR) :- pi x\ depth x H => ho2db (R x) (s H) DR.
ho2db X H (dvar DX) :- depth X HX, add HX DX H.
Click on a command or tactic to see a detailed view of its use.
%% Translation between higher-order and debruijn lambda terms %% %% A similar result is shown for Twelf at %% http://twelf.plparty.org/wiki/Concrete_representation %% They seem to need many contorsions which are unrelated to the %% actual task of the translation. They also define both a forward %% and backward translation, whereas we use a single translation and %% prove it deterministic in both directions. Their key difficulty %% is that they cannot use hypothetical assumptions like our (depth X N) %% since regular worlds are not powerful enough to specify the %% form of contexts which are created (e.g. they cannot show the %% natural number N must be unique). %% General property of member Theorem member_prune : forall E L, nabla x, member (E x) L -> exists F, E = y\F. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H2. search. %% Properties of addition Define nat z. Define nat (s X) := nat X. Define le X X. Define le X (s Y) := le X Y. Theorem le_dec : forall X Y, le (s X) Y -> le X Y. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H2. search. Theorem le_absurd : forall X, nat X -> le (s X) X -> false. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. apply le_dec to H4. apply IH to H3 H5. Theorem add_le : forall A B C, {add A B C} -> le B C. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H2. search. Theorem add_absurd : forall A C, nat C -> {add A (s C) C} -> false. [Show Proof][Hide Proof] intros. apply add_le to H2. apply le_absurd to H1 H3. Theorem add_zero : forall A C, nat C -> {add A C C} -> A = z. [Show Proof][Hide Proof] intros. case H2. search. case H1. apply add_absurd to H4 H3. % add is deterministic in its first argument Theorem add_det1 : forall A1 A2 B C, nat C -> {add A1 B C} -> {add A2 B C} -> A1 = A2. [Show Proof][Hide Proof] induction on 2. intros. case H2. apply add_zero to H1 H3. search. case H3. case H1. apply add_absurd to H5 H4. case H1. apply IH to H6 H4 H5. search. % add is deterministic in its second argument Theorem add_det2 : forall A B1 B2 C, {add A B1 C} -> {add A B2 C} -> B1 = B2. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. search. case H2. apply IH to H3 H4. search. %% Theorems specific to our translation Define ctx nil z. Define nabla x, ctx (depth x H :: L) (s H) := ctx L H. Define nabla x, name x. Theorem ctx_nat : forall L H, ctx L H -> nat H. [Show Proof][Hide Proof] induction on 1. intros. case H1. search. apply IH to H2. search. Theorem ctx_world : forall E L H, ctx L H -> member E L -> exists X HX, E = depth X HX /\ name X. [Show Proof][Hide Proof] induction on 1. intros. case H1. case H2. case H2. search. apply member_prune to H4. apply IH to H3 H4. search. Theorem depth_name : forall L H X HX, ctx L H -> {L |- depth X HX} -> name X. [Show Proof][Hide Proof] intros. case H2. apply ctx_world to H1 H3. search. Theorem member_depth_det2 : forall L H X H1 H2, ctx L H -> member (depth X H1) L -> member (depth X H2) L -> H1 = H2. [Show Proof][Hide Proof] induction on 2. intros. case H2. case H3. search. case H1. apply member_prune to H4. case H3. case H1. apply member_prune to H4. case H1. apply IH to H6 H4 H5. search. Theorem depth_det2 : forall L H X H1 H2, ctx L H -> {L |- depth X H1} -> {L |- depth X H2} -> H1 = H2. [Show Proof][Hide Proof] intros. case H2. case H3. apply member_depth_det2 to H1 H4 H5. search. Theorem ctx_member_absurd : forall X H1 H2 L, ctx L H1 -> member (depth X H2) L -> le H1 H2 -> false. [Show Proof][Hide Proof] induction on 2. intros. case H2. case H1. apply ctx_nat to H4. apply le_absurd to H5 H3. case H1. apply member_prune to H4. apply le_dec to H3. apply IH to H5 H4 H6. Theorem member_depth_det1 : forall L H X1 X2 HX, ctx L H -> member (depth X1 HX) L -> member (depth X2 HX) L -> X1 = X2. [Show Proof][Hide Proof] induction on 2. intros. case H2. case H3. search. case H1. apply ctx_member_absurd to H5 H4 _. case H3. case H1. apply ctx_member_absurd to H5 H4 _. case H1. apply IH to H6 H4 H5. search. Theorem depth_det1 : forall L H X1 X2 HX, ctx L H -> {L |- depth X1 HX} -> {L |- depth X2 HX} -> X1 = X2. [Show Proof][Hide Proof] intros. case H2. case H3. apply member_depth_det1 to H1 H4 H5. search. Theorem add_ignores_ctx : forall L H A B C, ctx L H -> {L |- add A B C} -> {add A B C}. [Show Proof][Hide Proof] induction on 2. intros. case H2. apply ctx_world to H1 H3. search. apply IH to H1 H3. search. %% ho2db is deterministic in its third argument %% ie, higher-order --> debruijn is unique Theorem ho2db_det3 : forall L M D1 D2 H, ctx L H -> {L |- ho2db M H D1} -> {L |- ho2db M H D2} -> D1 = D2. [Show Proof][Hide Proof] induction on 2. intros. case H2. apply ctx_world to H1 H4. case H3. apply ctx_world to H1 H6. apply IH to H1 H4 H6. apply IH to H1 H5 H7. search. apply depth_name to H1 H6. case H8. case H3. apply ctx_world to H1 H5. apply ctx_nat to H1. apply IH to _ H4 H5. search. apply depth_name to H1 H5. case H7. case H3. apply ctx_world to H1 H6. apply depth_name to H1 H4. case H8. apply depth_name to H1 H4. case H7. apply depth_det2 to H1 H4 H6. apply add_ignores_ctx to H1 H5. apply add_ignores_ctx to H1 H7. apply add_det2 to H8 H9. search. Theorem ho2db_det3_simple : forall M D1 D2, {ho2db M z D1} -> {ho2db M z D2} -> D1 = D2. [Show Proof][Hide Proof] intros. apply ho2db_det3 to _ H1 H2. search. %% ho2db is deterministic in its first argument %% ie, debruijn --> higher-order is unique %% proof is mostly the same as ho2db_det3 except with fewer cases Theorem ho2db_det1 : forall L M1 M2 D H, ctx L H -> {L |- ho2db M1 H D} -> {L |- ho2db M2 H D} -> M1 = M2. [Show Proof][Hide Proof] induction on 2. intros. case H2. apply ctx_world to H1 H4. case H3. apply ctx_world to H1 H6. apply IH to H1 H4 H6. apply IH to H1 H5 H7. search. case H3. apply ctx_world to H1 H5. apply ctx_nat to H1. apply IH to _ H4 H5. search. case H3. apply ctx_world to H1 H6. apply add_ignores_ctx to H1 H5. apply add_ignores_ctx to H1 H7. apply ctx_nat to H1. apply add_det1 to H10 H8 H9. apply depth_det1 to H1 H4 H6. search. Theorem ho2db_det1_simple : forall M1 M2 D, {ho2db M1 z D} -> {ho2db M2 z D} -> M1 = M2. [Show Proof][Hide Proof] intros. apply ho2db_det1 to _ H1 H2. search.