Type uniqueness for the simply-typed lambda-calculus


[View type-uniq-single.thm]

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

%% A single logic approach

Kind     tm, ty       type.

Type     app          tm -> tm -> tm.
Type     abs          ty -> (tm -> tm) -> tm.
Type     arr          ty -> ty -> ty.

Type     bind         tm -> ty -> o.

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

Define ctx : olist -> prop by
  ctx nil ;
  nabla x, ctx (bind x A :: L) := ctx L.

Define of : olist -> tm -> ty -> prop by
  nabla x, of (L x) x A := nabla x, member (bind x A) (L x) ;
  of L (app M N) B := exists A, of L M (arr A B) /\ of L N A ;
  of L (abs A R) (arr A B) := nabla x, of (bind x A :: L) (R x) B.

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

Theorem type_uniq : forall L E T1 T2,
  ctx L -> of L E T1 -> of L E T2 -> T1 = T2.