% 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!