% base.elf
%
% Defines irritating machinery: `absurd' and `pacifier'.


%
% `absurd' : empty type, for reasoning by contradiction.
%

absurd : type.
% `absurd' has no constructors...
%freeze absurd.    % ...let's make sure it never gets any.


%{ --------------------------------------------------------------------------------------

`pacifier' : essentially, a unit type with strange and unsound properties.
 
The purpose of `pacifier' is to get around Twelf's insistence on using subterm
ordering for everything, instead of providing direct support for user-defined
induction measures.  It depends on %trustme %reduces, so it is unsafe, but when the
below scheme is followed, it is only as unsafe as needed.

The idea is that if Twelf refuses, say, to accept that (rule2 D1 D2) is smaller than
(rule2 (rule D1) D2) in the proof of some metatheorem `goal', then:

 1. Add a premise of type `pacifier' to `goal', so  goal : pacifier -> ... -> type.

 2. Change the %total ... goal directive so that if, for example, `goal' inducts on
    its (formerly) first argument, `goal' instead uses lexicographic induction
    with `pacifier' first, then the (old) first argument.

 3. Modify the cases of the metatheorem accordingly:

    - If the case does not appeal to induction, just write _ for the pacifier argument.

    - If the case does appeal to induction, but Twelf's subterm ordering suffices to show termination,
       then write P for the pacifier argument throughout the case.

    - If the case appeals to induction and Twelf's subterm ordering fails,
         then:

              * Write P for the pacifier argument in the conclusion;

              * Add, just before (assuming the ... <- ... style) the use of the induction hypothesis,

                             <-  pacify P Psmall

              * Write Psmall for the pacifier argument in the induction hypothesis.

By writing P in both the conclusion and the i.h. in all the cases where subterm
ordering suffices, we ensure that Twelf does its usual checking for all the cases
where subterm ordering suffices: when P is the same, the lexicographic ordering
devolves to the "real" induction hypothesis.

In the cases Twelf cannot check, "pacify P Psmall" makes Twelf think that
a smaller Psmall exists, which dominates the lexicographic ordering.

Since the pacifier type has only one constructor, it should not cause
issues with output freeness or output coverage.

To call a "pacified" lemma "from the outside", pass pacifier/i.

---------------------------------------------------------------------------------------- }%

pacifier : type.

pacifier/i : pacifier.
%freeze pacifier.

pacify : pacifier -> pacifier -> type.
%name pacifier P.
%mode pacify +P1 -P2.

- : pacify pacifier/i pacifier/i.

%trustme %reduces P2 < P1 (pacify P1 P2).
%worlds () (pacify _ _).
%total  {} (pacify _ _).



%  2er:
%  a Boolean type whose constructors are "1" and "2".
%  This is occasionally convenient, but in most situations we end up 
%   having to write separate cases for "1" and "2", so it doesn't help much.
%
2er : type.
1 : 2er.
2 : 2er.
%freeze 2er.