twelf formalization and type safety for simply typed lambda calculus with n-ary tuples

stlc-tuples.elf

%%%% Formalization of a simply typed lambda-calculus with n-ary tuples.

% I decided to do this because it seemed like something small and
% interesting that was definitely not on the twelf wiki as a case
% study or a tutorial. n-ary tuples are a great feature in that they
% add no expressive power over pairs but are a much bigger pain to
% machine formalize!
%
% Doing it on paper is mostly just a matter of sprinkling "subscript i"
% and "..." around, but is otherwise pretty straightforward.
% Doing it in twelf, all the different ...s need to basically be their own
% type, and all the reasoning spelled out in detail. None of it is that hard,
% though, but...
%
% One hack I used is that for the places where we needed metatheorems
% saying it was possible to access or update a vec, instead of
% including a proof that the index was less than the length, we
% include a proof of another access to a vec of the same length.
% This is hardly a hack in the of-vec-member?? metatheorems
% (three identically stated and proved theorems with different modes),
% where one of the main purposes is in relating different lookups,
% but is a hack for exp-vec-can-update, which proves we can update
% a vec that we can access.
%
% Also I don't think my twelf style is very good.

nat : type.  %name nat N.
nat/z : nat.
nat/s : nat -> nat.
z = nat/z. s = nat/s.

%% STLC
tp : type.  %name tp T.
exp : type.  %name exp E.

% Vecs, which we need to duplicate for exps and tps, because we have
% no code reuse in twelf.
tp-vec : nat -> type.  %name tp-vec L.
tp-vec/nil : tp-vec z.
tp-vec/cons : tp -> tp-vec N -> tp-vec (s N).

exp-vec : nat -> type.  %name exp-vec L.
exp-vec/nil : exp-vec z.
exp-vec/cons : exp -> exp-vec N -> exp-vec (s N).

% Syntax
tbase : tp.
tarr : tp -> tp -> tp.
ttuple : tp-vec N -> tp.

lam : tp -> (exp -> exp) -> exp.
app : exp -> exp -> exp.
tuple : exp-vec N -> exp.
pi : exp -> nat -> exp.

% Core operations on vectors
tp-vec-member : tp-vec N -> nat -> tp -> type.
tp-vec-member/z : tp-vec-member (tp-vec/cons T _) z T.
tp-vec-member/s : tp-vec-member (tp-vec/cons _ L) (s N) T
                   <- tp-vec-member L N T.

exp-vec-member : exp-vec N -> nat -> exp -> type.
exp-vec-member/z : exp-vec-member (exp-vec/cons T _) z T.
exp-vec-member/s : exp-vec-member (exp-vec/cons _ L) (s N) T
                    <- exp-vec-member L N T.

exp-vec-update : exp-vec N -> nat -> exp -> exp-vec N -> type.
exp-vec-update/z : exp-vec-update (exp-vec/cons _ L) z E (exp-vec/cons E L).
exp-vec-update/s : exp-vec-update (exp-vec/cons X L) (s I) E (exp-vec/cons X L')
                    <- exp-vec-update L I E L'.

% If we can access, then we can update
% The point of this is that we don't want to have to reason directly
% about what indexes are valid, so we use the ability to access a
% member to prove that we can also update it.

exp-vec-can-update : exp-vec-member V I _ -> {E : exp} exp-vec-update V I E V' -> type.
- : exp-vec-can-update exp-vec-member/z _ exp-vec-update/z.
- : exp-vec-can-update (exp-vec-member/s D) E (exp-vec-update/s D')
     <- exp-vec-can-update D E D'.

%mode exp-vec-can-update +X1 +X2 -X3.
%worlds () (exp-vec-can-update _ _ _).
%total {D} (exp-vec-can-update D _ _).

%% Back to the STLC

% Static semantics
of : exp -> tp -> type.
of-vec : exp-vec N -> tp-vec N -> type.

of/app : of (app E1 E2) T2
          <- of E1 (tarr T1 T2)
          <- of E2 T1.
of/lam : of (lam T1 ([x] E x)) (tarr T1 T2)
          <- ({x : exp} {dx : of x T1} of (E x) T2).

of/tuple : of (tuple Es) (ttuple Ts)
            <- of-vec Es Ts.

of/pi : of (pi E I) T
         <- of E (ttuple Ts)
         <- tp-vec-member Ts I T.

of-vec/nil : of-vec exp-vec/nil tp-vec/nil.
of-vec/cons : of-vec (exp-vec/cons E Es) (tp-vec/cons T Ts)
               <- of E T
               <- of-vec Es Ts.


% Dynamic semantics
% I am doing eager evalutation specifically because it made products suck more.
value : exp -> type.
value/lam : value (lam T E).

values-first : {K:nat} exp-vec N -> type.
values-first/z : values-first z _.
values-first/s : values-first (s K) (exp-vec/cons V L)
                  <- value V
                  <- values-first K L.

value/tuple : value (tuple Es)
               <- values-first N (Es : exp-vec N).

steps : exp -> exp -> type.

steps/app1 : steps (app E1 E2) (app E1' E2)
              <- steps E1 E1'.
steps/app2 : steps (app V1 E2) (app V1 E2')
              <- value V1
              <- steps E2 E2'.
steps/beta : steps (app (lam _ ([x] Ef x)) V) (Ef V)
              <- value V.

steps/tuple : steps (tuple (Es : exp-vec N)) (tuple Es')
               <- values-first I Es
               <- exp-vec-member Es I E
               <- steps E E'
               <- exp-vec-update Es I E' Es'.

steps/pi-compat : steps (pi E I) (pi E' I)
                   <- steps E E'.

steps/pi : steps (pi (tuple Vs) I) V
            <- value (tuple Vs)
            <- exp-vec-member Vs I V.

%% Lemmas/functions relating of-vec to its exp-vec and tp-vec

% Argh! We need to index into of-vec a bunch, but we need to do it
% with three different polarities.
% These genuinely all *do* need at least one of the vec-members
% as input, so using that isn't too hacky.

of-vec-member+- : {N : nat}
                   of-vec Es Ts
                   -> exp-vec-member Es N E
                   -> tp-vec-member Ts N T
                   -> of E T
                   -> type.

- : of-vec-member+- z (of-vec/cons _ Dof) exp-vec-member/z tp-vec-member/z Dof.
- : of-vec-member+- (s N) (of-vec/cons L _) (exp-vec-member/s ME) (tp-vec-member/s MT) Dof
     <- of-vec-member+- N L ME MT Dof.

%mode of-vec-member+- +X1 +X2 +X3 -X4 -X5.
%worlds () (of-vec-member+- _ _ _ _ _).
%total {N} (of-vec-member+- N _ _ _ _).

of-vec-member-+ : {N : nat}
                   of-vec Es Ts
                   -> exp-vec-member Es N E
                   -> tp-vec-member Ts N T
                   -> of E T
                   -> type.

- : of-vec-member-+ z (of-vec/cons _ Dof) exp-vec-member/z tp-vec-member/z Dof.
- : of-vec-member-+ (s N) (of-vec/cons L _) (exp-vec-member/s ME) (tp-vec-member/s MT) Dof
     <- of-vec-member-+ N L ME MT Dof.

%mode of-vec-member-+ +X1 +X2 -X3 +X4 -X5.
%worlds () (of-vec-member-+ _ _ _ _ _).
%total {N} (of-vec-member-+ N _ _ _ _).

of-vec-member++ : {N : nat}
                   of-vec Es Ts
                   -> exp-vec-member Es N E
                   -> tp-vec-member Ts N T
                   -> of E T
                   -> type.

- : of-vec-member++ z (of-vec/cons _ Dof) exp-vec-member/z tp-vec-member/z Dof.
- : of-vec-member++ (s N) (of-vec/cons L _) (exp-vec-member/s ME) (tp-vec-member/s MT) Dof
     <- of-vec-member++ N L ME MT Dof.

%mode of-vec-member++ +X1 +X2 +X3 +X4 -X5.
%worlds () (of-vec-member++ _ _ _ _ _).
%total {N} (of-vec-member++ N _ _ _ _).

of-vec-update : of-vec Es Ts
                 -> exp-vec-update Es I E Es'
                 -> tp-vec-member Ts I T
                 -> of E T
                 -> of-vec Es' Ts
                 -> type.

- : of-vec-update
     (of-vec/cons DofR _)
     exp-vec-update/z
     tp-vec-member/z
     DofE
     (of-vec/cons DofR DofE).

- : of-vec-update
     (of-vec/cons DofR DofE')
     (exp-vec-update/s UpR)
     (tp-vec-member/s MemR)
     DofE
     (of-vec/cons DofV DofE')
     <- of-vec-update DofR UpR MemR DofE DofV.

%mode of-vec-update +X1 +X2 +X3 +X4 -X5.
%worlds () (of-vec-update _ _ _ _ _).
%total {T} (of-vec-update _ T _ _ _).


% Preservation

preserves : of E T -> steps E E' -> of E' T -> type.

% oh nice, we get all the inversion for free

- : preserves
     (of/app Dof2 Dof1)
     (steps/app1 Ds : steps (app E1 E2) (app E1' E2))
     (of/app Dof2 Dind)
     <- preserves Dof1 Ds Dind.

- : preserves
     (of/app Dof2 Dof1)
     (steps/app2 Ds _ : steps (app E1 E2) (app E1 E2'))
     (of/app Dind Dof1)
     <- preserves Dof2 Ds Dind.

- : preserves
     (of/app Dof2 (of/lam ([x] [dx] Dof x dx)))
     (steps/beta _ : steps (app (lam _ ([x] Ef x)) V) (Ef V))
     (Dof V Dof2).

- : preserves
     (of/pi
        (TMem : tp-vec-member Ts I T)
        (of/tuple DofVs)
        : of (pi (tuple _) I) _)
     ((steps/pi
        (VMem : exp-vec-member Vs I V)
        Dvalue
        ): steps (pi (tuple _) I) _)
     DofV
     <- of-vec-member++ I DofVs VMem TMem DofV.

- : preserves
     (of/tuple DofEs : of (tuple Es) (ttuple Ts))
     (steps/tuple
        (VU : exp-vec-update Es I E' Es')
        (DstepsE : steps E E')
        (VM : exp-vec-member Es I E)
        (VFirst : values-first I Es)
        )
     (of/tuple DofEs')
     <- of-vec-member+- I DofEs VM TM DofE
     <- preserves DofE DstepsE DofE'
     <- of-vec-update DofEs VU TM DofE' DofEs'.

- : preserves
     (of/pi TMem DofE)
     (steps/pi-compat Dsteps)
     (of/pi TMem DofE')
     <- preserves DofE Dsteps DofE'.

%mode preserves +X1 +X2 -X3.
%worlds () (preserves _ _ _).
%total {D} (preserves _ D _).

% Progress

unstuck : exp -> type.
unstuck/value : value E -> unstuck E.
unstuck/steps : steps E E' -> unstuck E.

unstuck-vec : exp-vec N -> type.
unstuck-vec/value : values-first N (Es : exp-vec N) -> unstuck-vec Es.
unstuck-vec/steps : values-first K (Es : exp-vec N)
                     -> exp-vec-member Es K E
                     -> steps E E'
                     -> unstuck-vec Es.

progress-app : of E1 (tarr T1 T2)
                -> of E2 T1
                -> unstuck E1
                -> unstuck E2
                -> unstuck (app E1 E2)
                -> type.

% canonical forms for free too!

- : progress-app _ _ (unstuck/steps Ds) _ (unstuck/steps (steps/app1 Ds)).

- : progress-app _ _ (unstuck/value Dv) (unstuck/steps Ds)
     (unstuck/steps (steps/app2 Ds Dv)).

- : progress-app _ _ (unstuck/value value/lam) (unstuck/value Dv)
     (unstuck/steps (steps/beta Dv)).

%mode progress-app +X1 +X2 +X3 +X4 -X5.
%worlds () (progress-app _ _ _ _ _).
%total {} (progress-app _ _ _ _ _).

progress-pi : of E (ttuple Ts)
               -> tp-vec-member Ts I T
               -> unstuck E
               -> unstuck (pi E I)
               -> type.

- : progress-pi Dof TM (unstuck/steps Dsteps) (unstuck/steps (steps/pi-compat Dsteps)).

- : progress-pi
     (of/tuple DVs)
     TM
     (unstuck/value (value/tuple VF))
     (unstuck/steps (steps/pi VM (value/tuple VF)))
     <- of-vec-member-+ _ DVs VM TM _.

%mode progress-pi +X1 +X2 +X3 -X4.
%worlds () (progress-pi _ _ _ _).
%total {} (progress-pi _ _ _ _).

progress-tuple : of-vec Es Ts
                  -> unstuck-vec Es
                  -> unstuck (tuple Es)
                  -> type.

- : progress-tuple
     Dof
     (unstuck-vec/value Vf)
     (unstuck/value (value/tuple Vf)).

- : progress-tuple
     Dof
     (unstuck-vec/steps (Vf : values-first K _) VM Dsteps)
     (unstuck/steps
        (steps/tuple Upd Dsteps VM Vf))
     <- exp-vec-can-update VM _ Upd.

%mode progress-tuple +X1 +X2 -X3.
%worlds () (progress-tuple _ _ _).
%total {} (progress-tuple _ _ _).

% Helper output factoring lemma for constructing an unstuck-vec
progress-vec-help : unstuck E
                     -> unstuck-vec Es
                     -> unstuck-vec (exp-vec/cons E Es)
                     -> type.

- : progress-vec-help
     (unstuck/steps Dsteps)
     _
     (unstuck-vec/steps values-first/z exp-vec-member/z Dsteps).

- : progress-vec-help
     (unstuck/value DV)
     (unstuck-vec/value Vf)
     (unstuck-vec/value (values-first/s Vf DV)).

- : progress-vec-help
     (unstuck/value DV)
     (unstuck-vec/steps Vf Mem Dsteps)
     (unstuck-vec/steps
        (values-first/s Vf DV)
        (exp-vec-member/s Mem)
        Dsteps).

%mode progress-vec-help +X1 +X2 -X3.
%worlds () (progress-vec-help _ _ _).
%total {} (progress-vec-help _ _ _).


progress : of E T -> unstuck E -> type.

progress-vec : of-vec Es Ts -> unstuck-vec Es -> type.

%mode progress +X1 -X2.
%mode progress-vec +X1 -X2.

- : progress (of/lam _) (unstuck/value value/lam).

- : progress
     (of/app Dof2 Dof1)
     Un
     <- progress Dof1 Un1
     <- progress Dof2 Un2
     <- progress-app Dof1 Dof2 Un1 Un2 Un.

- : progress
     (of/pi TM Dof)
     Un
     <- progress Dof Un1
     <- progress-pi Dof TM Un1 Un.

- : progress
     (of/tuple DofEs)
     Un
     <- progress-vec DofEs Un1
     <- progress-tuple DofEs Un1 Un.

- : progress-vec of-vec/nil (unstuck-vec/value values-first/z).

- : progress-vec (of-vec/cons DEs DE) Out
     <- progress DE Un
     <- progress-vec DEs Uns
     <- progress-vec-help Un Uns Out.

%worlds () (progress _ _) (progress-vec _ _).
%total (D D') (progress D _) (progress-vec D' _).



%% Pointless screwing around

% An evaluator. It always terminates, but twelf doesn't know that.
% It will fail if the term is bad.
full-eval : of E T -> exp -> type.
full-eval-help : of E T -> unstuck E -> exp -> type.

- : full-eval (D : of E T) E'
     <- progress D U
     <- full-eval-help D U E'.
fe/done : full-eval-help (D : of E T) (unstuck/value _) E.
fe/step : full-eval-help (D : of E T) (unstuck/steps Dsteps) E''
           <- preserves D Dsteps D'
           <- full-eval D' E''.


%% Test terms
unit : tp = ttuple tp-vec/nil.
empty : exp = tuple exp-vec/nil.
triple : exp -> exp -> exp -> exp = [x] [y] [z] tuple (exp-vec/cons x (exp-vec/cons y (exp-vec/cons z exp-vec/nil))).
testexpr = pi (
                 triple (pi (triple empty empty empty) (s z))
                 (app (lam unit ([x] x)) empty) empty)
            (s z).

%solve DofE : of testexpr T.
%solve _ :  full-eval DofE E'.