% A simple example of the strengthening problem and two simple solutions
%
% The example is motivated by the `demote' in the lambda-a calculus.
% Our calculus here is untyped lambda-calculus with terms marked
% by either 1 or 0. The challenge is to implement a function that
% converts terms marked by 1 into those marked by 0 -- and show its
% totality.
% Showing totality requires strengthening, as shown below.
% Astonishingly, the most naive definition of strengthening works.
% I wanted to structure a world, so to specify that some
% hypotheses are not independent but related. So, discharging one related
% hypothesis automatically discharges its related partner. But that
% turns out unnecessary.
% The strengthening problem has been discussed at POPL2008 with Bob Harper
% and Karl Crary. Karl suggested an approach (outlined below) that
% needed intentional equality. That turns out unnecessary.
% I can't believe how simple the final solution is.
%
% There is the second solution, near the end of the file. It is round-about,
% requiring us to define a different sort of terms, which are nevertheless
% isomorphic to the original ones. The isomorphism has to be proven
% constructively, too -- although it is boilerplate. The desired 
% transformation now includes two steps: transforming the source 
% expression into the isomorphic form, and changing the mark of the latter.
% Albeit indirect, the solution avoids strengthening altogether.

mark: type.				% There are two marks for terms
0: mark.
1: mark.

% Marked lambda-calculus terms
exp: mark -> type.		%name exp E.
a: exp M -> exp M -> exp M.
l: (exp M -> exp M) -> exp M.

% A sample term
t1 : exp 1 = a (l [x] (l [y] (a x y))) (l [x] x).

% Let us illustrate the problem of the naive copying
cp1: exp 1 -> exp 0 -> type.
%mode cp1 +E1 -E2.
cp1-a: cp1 (a E1 E2) (a E1' E2')
       	 <- cp1 E2 E2'
         <- cp1 E1 E1'.
cp1-l: cp1 (l E1) (l E1')
       <- ({x}{x'} cp1 x x' -> cp1 (E1 x) (E1' x')).
%block cp1-l-bl : block {x:exp 1} {x':exp 0} {D:cp1 x x'}.
%worlds (cp1-l-bl) (cp1 _ _).
%%total {E1} (cp1 E1 _).

%{
If we uncomment the %total declaration, we get:

Totality: Output of subgoal not covered
Output coverage error --- missing cases:
{E1:exp 1 -> exp 1} {E2:exp 1 -> exp 0 -> exp 0}
   |- {x:exp 1} {x':exp 0} cp1 x x' -> cp1 (E1 x) (E2 x x').

Indeed, Twelf says that in the clause cp1-l, E' is in scope of both
x and x' -- it depends on both hypotheses x and x'. The pattern match
(E' x') assumes that E' does not depend on x. But there is no proof of that.
So, we need strengthening: we need to prove to Twelf that E' really
does not depend on x.

Karl Crary suggested the following solution: first, introduce 
cp-total: cp E E -> type.
When proving it, use a lemma
foo: ({x}{y} cp x y -> cp (E x) (E' x y)) -> 
({x}{y} exp-eq (E' x y) (E'' y)).
Build exp-eq family to prove the lemma.

As it turns out, a simpler approach suffices.
}%

% Astonishingly, proving strengthening is straightforward: the marks
% in the type of terms do help. We observe from the definition of exp
% that a term of the type exp 0 cannot have any subterm of the type exp 1. 
% We merely need to express this obvious fact in the form Twelf understands.
% See the strength family.

% Forward declaration of the new copying relation and the block declaration.
cp2: exp 1 -> exp 0 -> type.
%block cp2-l-bl : block {x:exp 1} {x':exp 0} {d:cp2 x x'}.

% Strengthening: asserting that exp 0 cannot depend on any hypothesis of
% the type exp 1. The following is the constructive proof.
strength : (exp 1 -> exp 0) -> exp 0 -> type.
%mode strength +H -E.
-: strength ([x] E) E.		% for E that is patently independent of x
-: strength ([x] (a (E1 x) (E2 x))) (a E1' E2')
   <- strength E1 E1'
   <- strength E2 E2'.
-: strength ([x] (l [x'] (E x' x))) (l E')
   <- {x':exp 0} strength (E x') (E' x').
%block strength-bl : block {x':exp 0}.
%worlds (strength-bl | cp2-l-bl) (strength _ _).
%covers strength +H -E.
%total {E} (strength E _).

% Using strengthening is trivial, too.

% cp2: exp 1 -> exp 0 -> type.
%mode cp2 +E1 -E2.
cp2-a: cp2 (a E1 E2) (a E1' E2')
       	 <- cp2 E2 E2'
         <- cp2 E1 E1'.
cp2-l: cp2 (l E1) E1''
       <- ({x}{x'} cp2 x x' -> cp2 (E1 x) (E1' x x'))
       <- strength ([x] (l (E1' x))) E1''.
%worlds (cp2-l-bl) (cp2 _ _).
%total {E1} (cp2 E1 _).

% Example
%query 1 1 (cp2 t1 T).
% T = a (l ([e:exp 0] l ([e1:exp 0] a e e1))) (l ([e:exp 0] e)).


% The second, round-about solution.
% It is deterministic, however.
% Rather than transforming (exp 1) to (exp 0) directly, we introduce 
% terms (expi M) isomorphic to (exp M), transform (exp 1) to (expi 1)
% and then transform (expi 1) to (exp 0).
% The advantage is that terms (exp M) cannot appear in (expi M) and vice
% versa, so (exp M) cannot depend on assumptions of the type {x:expi M}
% and vice versa. We thus avoid strengthening altogether.

% Marked lambda-calculus terms
expi: mark -> type.		%name expi _Ei.
a2: expi M -> expi M -> expi M.
l2: (expi M -> expi M) -> expi M.

% Stating that (exp M) are isomorphic to (expi M).
% We only need one direction however: given any term (exp M), we can
% always obtain the corresponding (expi M).
exp-expi: exp M -> expi M -> type.
%mode exp-expi +E1 -E2.
-: exp-expi (a E1 E2) (a2 E1' E2')
   <- exp-expi E2 E2'
   <- exp-expi E1 E1'.
-: exp-expi (l E1) (l2 E1')
   <- {e:exp M} {e2:expi M}
      exp-expi e e2 ->
      exp-expi (E1 e) (E1' e2).
%block bl-exp-expi : 
       some {M:mark} 
       block {e:exp M} {e2:expi M} {t:exp-expi e e2}.
%worlds (bl-exp-expi) (exp-expi _ _).
%total {E} (exp-expi E _).

% The main transformation
% The source term is (expi 1) rather than (exp 1).
cpaux: expi 1 -> exp 0 -> type.
%mode cpaux +E1 -E2.
cpa-a: cpaux (a2 E1 E2) (a E1' E2')
       	 <- cpaux E2 E2'
         <- cpaux E1 E1'.
cpa-l: cpaux (l2 E1) (l E1')
       <- ({x:expi 1}{x':exp 0} cpaux x x' -> cpaux (E1 x) (E1' x')).
%block bl-cpaux : block {x:expi 1} {x':exp 0} {t:cpaux x x'}.
%worlds (bl-cpaux) (cpaux _ _).
%total {E1} (cpaux E1 _).

% Putting it all together
cpi: exp 1 -> exp 0 -> type.
%mode cpi +E1 -E2.
-: cpi E1 E2 <- exp-expi E1 E1' <- cpaux E1' E2.
%worlds () (cpi _ _).
%total {} (cpi _ _).

% Example
%query 1 2 (cpi t1 T).