Built with Alectryon, running Coq+SerAPI v8.13.0+0.13.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
Require Import MyTactics.
Require Import LambdaCalculusSyntax.
Require Import LambdaCalculusValues.
Require Import LambdaCalculusReduction.

Types

Here is the syntax of simple types:

Inductive ty :=
| TyVar (x : var)
| TyFun (A B : ty).

A type environment is viewed as a total function of variables to types.

In principle, an environment should be modeled as a list of types, which represents a partial function of variables to types. This introduces a few complications, and is left as an exercise for the reader.

Definition tyenv := var -> ty.

The typing judgement

The simply-typed lambda-calculus is defined by the following three typing rules.

Inductive jt : tyenv -> term -> ty -> Prop :=
| JTVar:
    forall Gamma x T,
    Gamma x = T ->
    jt Gamma (Var x) T
| JTLam:
    forall Gamma t T U,
    jt (T .: Gamma) t U ->
    jt Gamma (Lam t) (TyFun T U)
| JTApp:
    forall Gamma t1 t2 T U,
    jt Gamma t1 (TyFun T U) ->
    jt Gamma t2 T ->
    jt Gamma (App t1 t2) U
.

The tactic [pick_jt t] picks a hypothesis [h] whose statement is a typing judgement about the term [t], and passes [h] to the Ltac continuation [k].

Thus, for instance, [pick_jt t invert] selects a typing judgement that is at hand for the term [t] and inverts it.

Ltac pick_jt t k :=
  match goal with h: jt _ t _ |- _ => k h end.

The following hint allows eauto with jt to apply the above typing rules.

The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]