The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Hello Norman.

You can find a formalization of 1-6 in http://color.inria.fr/ using 
named variables (no de Bruijn indices) and explicit alpha-equivalence.

Le 15/11/2012 09:51, Norman Danner a écrit :
> Hello list,
>
> I am looking for a development of the simply-typed lambda calculus that
> I could look at, as I'm having some trouble doing this on my own.  I
> suspect my difficulties are not deep.  What I'm looking for is a
> development along the following lines:
>
> 1. A definition of expressions (nothing complicated; just variables,
>     natural number constants, abstraction, and application).

The definition of terms is parameterized by a set of constants (you can 
take nat for it if you want). See 
http://color.inria.fr/doc/CoLoR.Term.Lambda.LTerm.html for the 
definitions and lemmas.

> 2. A definition of type (nothing complicated; just N and arrow types).
> 3. A notion of type context.
> 4. A definition of 'typed G t tau', where Pi : typed G t tau means that
>     Pi is a derivation that t has type tau under type context G (below,
>     G |- t : tau).

See http://color.inria.fr/doc/CoLoR.Term.Lambda.LSimple.html .

> 5. A notion of substitution on expressions.

See http://color.inria.fr/doc/CoLoR.Term.Lambda.LSubs.html .

> 6. A proof that if G, x : sigma |- t : tau and G |- s : sigma, then
>     G |- t[s/x] : tau.

See lemma tr_subs in 
http://color.inria.fr/doc/CoLoR.Term.Lambda.LSimple.html .

> 7. The standard full-function-space denotational semantics using nat
>     and -> to interpret N and arrow types, where den Pi xi is the
>     denotation of (the typing of) the expression t under environment
>     xi (i.e., really a definition of
>     den {G} {t} {tau} (Pi : typed G t tau) xi).

By "full-function-space", do you mean the set-theoretical function space 
F(A,B) that includes non-computable functions too? If so, the Coq space 
A->B is not enough.

Frederic.

> 8. A proof that if Pi is a derivation of G |- t[s/x] : tau obtained
>     from derivations Pi_t of G, x:sigma |- t:tau and
>     Pi_s of G |- s:sigma, then
>     den Pi xi = den Pi_t (xi[x |-> den Pi_s xi]).
>
> I can do 1-7 without much difficulty.  8 is killing me.  I assume it is
> because I am doing something sub-optimally somewhere in 1-7.
>
> I'm sure I'm not the first person to try to do this, and I think the
> most efficient way to solve my difficulties is to see it done right.  I
> would be grateful for pointers to solutions.  Thanks!
>
>      - Norman