Type uniqueness for simply typed lambda calculus using only LG-omega

Executable Specification

[View type-uniq.sig] [View type-uniq.mod]
sig type-uniq.

kind    tm, ty    type.

type    app       tm -> tm -> tm.
type    abs       ty -> (tm -> tm) -> tm.

type    arrow     ty -> ty -> ty.

type    of        tm -> ty -> o.

module type-uniq.

of (abs T R) (arrow T U) :- pi x\ (of x T => of (R x) U).
of (app M N) T :- of M (arrow U T), of N U.

Reasoning

[View type-uniq-lg.thm]

Click on a command or tactic to see a detailed view of its use.

Specification "type-uniq".

Theorem member_prune : forall E L, nabla (x:tm),
  member (E x) L -> exists F, E = y\F.

% Since LG-omega does not allow nabla in the head of a definition, we must
% explicitly restrict structure and occurences of the variable X
Define ctx : olist -> prop by
  ctx nil ;
  ctx (of X T :: L) := (forall M N, X = app M N -> false) /\
                       (forall T R, X = abs T R -> false) /\
                       (forall T', member (of X T') L -> false) /\
                       ctx L.

Theorem ctx_member :
  forall E L,
  ctx L -> member E L ->
  exists X T, (E = of X T)
           /\ (forall M N, X = app M N -> false)
           /\ (forall T R, X = abs T R -> false).

Theorem ctx_app_absurd : forall L M N T,
  ctx L -> member (of (app M N) T) L -> false.

Theorem ctx_abs_absurd : forall L R T S,
  ctx L -> member (of (abs S R) T) L -> false.

Theorem uniq : forall L E T1 T2,
  ctx L -> member (of E T1) L -> member (of E T2) L -> T1 = T2.

Theorem ctx_extend : forall T L, nabla x,
  ctx L -> ctx (of x T :: L).

Theorem det_of : forall L E T1 T2,
  ctx L -> {L |- of E T1} -> {L |- of E T2} -> T1 = T2.