The Coq mailing list

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

Hi Jevgenijs,

First, thanks for your reply!

On Fri, Mar 09, 2007 at 05:55:02PM +0200, Jevgenijs Sallinens wrote:
> Quoting Edsko de Vries 
> <devriese AT cs.tcd.ie>:
> 
> >Now I can't directly do elim H, since some of the arguments of typeof
> >aren't variables. Now this occurs quite frequently, and so far I've
> >always successfully applied the technique explained in section 8.4.3
> >(Proving Semantic Properties) of Coq'Art, which introduces a new
> >variable to be bound to the expression, i.e.
> >
> >cut(forall (G':context), typeof G' t T -> G' = upd x S G ->
> >  forall pf : disjoint eq_var_dec (x :: fv s) (bv t),
> >  typeof G s S -> typeof G (subst x s t pf) T).
> >
> 
> I think you can do something like: induction 1;intros; subst G.

Perhaps I misunderstand you, but if I do what you suggest after the cut, then 
I
get the following induction hypothesis:

IHtypeof : upd x0 T1 (upd x S G) = upd x S G ->
           forall pf : disjoint eq_var_dec (x :: fv s) (bv t),
           typeof G s S -> typeof G (subst x s t pf) T2

which has the same problem that I described: the requirement that upd x0 T1 
(upd x
S G) = upd x S G is simply not true.  I have tried using a slightly different
cut:

cut(forall G':context, typeof G' t T -> forall G:context, G' = upd x S G ->
  forall pf : disjoint eq_var_dec (x :: fv s) (bv t),
  typeof G s S -> typeof G (subst x s t pf) T).

(where the original context is now also universally quantified). This gives me
the induction hypothesis

IHtypeof : forall G : context,
           upd x0 T1 (upd x S G1) = upd x S G ->
           forall pf : disjoint eq_var_dec (x :: fv s) (bv t),
           typeof G s S -> typeof G (subst x s t pf) T2

which is slightly better; if I instantiate G to (upd x0 T1 G1), I'd have to
prove that

  upd x0 T1 (upd x S G1) = upd x S (upd x0 T1 G1)

which is like the permutation lemma, but it is much easier to prove the
permutation lemma in a slightly different form (that is: if a term can be 
typed
in a context G, then it can also be typed in any permutation of G). With the
setup as above, I need a much stronger form of the permutation lemma (any
permutation of a context EQUALS the context), which may or may not be true. 

> A bit strange that you need pf within subst - it will complicate your
> proofs.

You think? If the condition proven by pf is not satisfied, then my definition
of subst is wrong (not capture avoiding). I thought it would be easier to do 
it
this way, rather than giving a more complicated definition of subst which
doesn't need this proof but is capture-avoiding by definition, since the 
latter
would be more complicated and therefore more difficult to reason about. This
way, I have a proof obligation when I call subst, but that obligation is
usually easily satisfied; but reasoning about subst is easier. -- But as I
said, I'm still very much a beginner with Coq, so if you think that it will
be easier to define subst differently (modifying it so that it calls
alpha_rename, for example), please let me know. Or are you perhaps suggesting
that I should define subst the way I have it (without calls to alpha_rename),
but also without the proof obligation?
 
At the moment, I'm still very much learning how to use Coq - it's not so
much that I need the proof that I'm working on, as that I need to learn
how to do it :) Ultimately, I need to use it to prove properties of a
type system that I am proposing, but at the moment I'm doing the proofs
for the standard simply typed lambda calculus, to get to know Coq and
get some experience with it.

Edsko