The Coq mailing list

[Sunil Kothari <skothari AT uwyo.edu>]

Hello All,
   I was wondering if there are any machine checked proofs (in any theorem 
prover) of replacement lemma [1,2] . I reproduce the lemma as stated by 
Wright and Felleisen in [1] below:
If
1. D is a derivation concluding  \Gamma |-  C [t]: \tau,
2. D1 is a sub-derivation of D concluding \Gamma’ |- t :\tau',
3. D1 occurs in D in the position corresponding to the hole ([]) in C, and
4. ’\Gamma |- t’ : \tau' is derivable.
Then  \Gamma |- C[t’] :\tau is derivable . 

Also, I wanted to know if there is a corresponding lemma in a constraint 
setting where the sequent becomes a 4-place relation. For example, \Gamma, E 
|- t: \tau, where E denotes a list of equational constraints.  If there is 
such a lemma, has it been formalized in any theorem prover ?

Any pointers/references will be highly appreciated.

Thanks,
Sunil



References:
[1] Andrew K. Wright and Matthias Felleisen. A syntactic approach to type
soundness. Information and Computation, 115(1):38-94, 1994.
[2] J. Roger Hindley and Jonathan P. Seldin. Introduction to Combinators
and /\-Calculus. Cambridge University Press, 1986.