The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hey,

>   There are still some problems with these definitions:
>     your types Term and welltyped are empty (no base case), so any 
> proposition of the
>   forms "forall t:Term, P t "and "forall G t, welltyped G t -> ..." are 
> trivially provable.

Well, yes, that's true, but that's not true in the full proof. For the
base cases, Q will have to proven differently; I just tried to make the
example as small as I could possibly make it.

> Moreover, shouldn't context be an inductive type , with f g (and 
> empty_context)  as constructors ?

I dont understand, why should that be the case? My "real" definition of
a context is a association list with the property that it means any
variable to at most one type:

Definition propCxt (l : list (Var * type)) := 
  forall (x:Var) (T1 T2:type), In (x,T1) l /\ In (x,T2) l -> T1 = T2.
  Definition context : Set := {l : list (Var * type) | propCxt l}.

But I figured that for the same of a minimal example, I'd abstract away
from that. f and g are different calls to a function "upd" which updates
the context in a particular way. 

I do think however that my "minimal" example is in fact self-contained;
it should be possible to complete the proof (granted, taking advantage
of the fact that the terms don't have a base case will allow you to
prove anything, but that's beside the point).

Edsko