Example of ill-typed term

illtyped.v

Require Import List.
Require Import String.
Open Scope string_scope.

Definition var := string.

Inductive Expr : Set :=
| EConst                        (* The one and only constant     *)
| EVar (v : var)                (* Variables                     *)
| EApp (e1 : Expr) (e2 : Expr)  (* Application, e1 applied to e2 *)
| EAbs (x : var) (body : Expr). (* Abstraction, \x -> body       *)

(* Here we define the types for the simply typed lambda calculus *)
Inductive SimpleType :=
  | TUnit
  | TFun (arg : SimpleType) (res : SimpleType).

(* Here we define what a type environment is *)
(* Simply a mapping from variables to types *)
Definition Env := var -> option SimpleType.

(* Here is how we extend a typing environment with another variable binding *)
Definition extend (env : Env) x t :=
  fun y => if string_dec x y then Some t else env y.

(* What it means for a lambda expression to be well typed *)
(* These are the type rules for STLC *)
(* You will frequently see them in the literature with horizontal lines *)
Inductive WellTyped : Env -> Expr -> SimpleType -> Prop :=
  | WtConst :
      forall env,
        WellTyped env EConst TUnit
  | WtVar :
      forall env x t,
        env x = Some t ->
        WellTyped env (EVar x) t
  | WtAbs :
      forall env x t exp t',
        WellTyped (extend env x t) exp t' ->
        WellTyped env (EAbs x exp) (TFun t t')
  | WtApp :
      forall env f arg t t',
        WellTyped env arg t ->
        WellTyped env f (TFun t t') ->
        WellTyped env (EApp f arg) t'.

Definition bad : Expr := (EAbs "x" (EApp (EVar "x") (EVar "x"))).

Fixpoint size_of_type (t : SimpleType) : nat :=
  match t with
    | TUnit => 1
    | TFun t1 t2 => size_of_type t1 + size_of_type t2
  end.

Require Import Omega.

Lemma size_of_type_positive :
  forall t,
    size_of_type t > 0.
Proof.
  induction t.
  - auto.
  - simpl. omega.
Qed.

Lemma no_infinite_types :
  forall t1 t2,
    t1 <> TFun t1 t2.
Proof.
  unfold not.
  intros.
  assert (size_of_type t1 = size_of_type (TFun t1 t2)) by now rewrite H at 1.
  simpl in *.
  assert (size_of_type t2 > 0) by auto using size_of_type_positive.
  omega.
Qed.

Theorem bad_ill_typed :
  forall tau Gamma,
    ~ WellTyped Gamma bad tau.
Proof.
  unfold not.
  intros.
  inversion H; subst; clear H.
  inversion H4; subst; clear H4.
  inversion H5; subst; clear H5.
  inversion H2; subst; clear H2.
  unfold extend in *. simpl in H1, H3.
  inversion H1; subst; clear H1.
  inversion H3; clear H3.

  eapply no_infinite_types; eauto.
Qed.