% Proving that the mirror operation on btrees is involution % (i.e., its own inverse): % mirror . mirror = id % Primitive types: one so far, integer. % A term N of type nat is a nonnegative integer. % Constructors: 0, 1. nat: type. %name nat N. 0: nat. 1: nat -> nat. %prefix 200 1. % First we define a btree, with nats at the leaves. We could have parameterized % btree by the type of leaf values; that doesn't seem to buy us much. btree: type. %name btree B. % constructors leaf: nat -> btree. node: btree -> btree -> btree. % Next we define the mirror function % Although it is written as a relation, it truly is a function: see % the mode declaration. mirror: btree -> btree -> type. %mode mirror +B1 -B2. mr-l: mirror (leaf N) (leaf N). mr-b: mirror (node B1 B2) (node B2' B1') <- mirror B1 B1' <- mirror B2 B2'. %worlds () (mirror _ _). %total {B1} (mirror B1 _). % Twelf accepts our total assertion: mirror is indeed a total function % on btrees. % A few illustrations of mirror % A sample btree btree1 = node (node (leaf 0) (leaf 1 0)) (leaf 1 1 0). %query 1 1 mirror btree1 X. % X = node (leaf (1 1 0)) (node (leaf (1 0)) (leaf 0)). %define btree1-m = R %solve _ : (mirror btree1 R). %{ btree1-m : btree = node (leaf (1 1 0)) (node (leaf (1 0)) (leaf 0)). _ : mirror btree1 (node (leaf (1 1 0)) (node (leaf (1 0)) (leaf 0))) = mr-b mr-l (mr-b mr-l mr-l). }% %query 1 1 mirror btree1-m X. % X = node (node (leaf 0) (leaf (1 0))) (leaf (1 1 0)). % We now state the main theorem: mirror is its own inverse (involution). % That is, given the proof that mirror B B' holds we compute % the proof that mirror B' B holds. % The variables B and B' are implicitly universally quantified, as % can be seen from the type of mirror-thm reported by Twelf: % mirror-inv-thm : {B:btree} {B':btree} mirror B B' -> mirror B' B -> type. mirror-inv-thm: mirror B B' -> mirror B' B -> type. %mode mirror-inv-thm +P1 -P2. -: mirror-inv-thm mr-l mr-l. -: mirror-inv-thm (mr-b P1L P1R) (mr-b P2R P2L) <- mirror-inv-thm P1L P2L <- mirror-inv-thm P1R P2R. %worlds () (mirror-inv-thm _ _). %total {P1} (mirror-inv-thm P1 _). % Twelf agrees that the computation is total. That is, mirror-inv-thm is % the proof term for the main theorem. We have completed our proof!