The Coq mailing list

[Jean-Christophe Filliatre <Jean-Christophe.Filliatre AT lri.fr>]

> I wouldn't _mind_ that of course :-), but what I was thinking
> of was something like having the possibility to write:
> 
>       (divide x y (LATEST y#0))
> 
> where "(LATEST T)" means the latest object of type T that has
> been introduced (better syntax would be nice of course).  I
> was talking about _expressions,_ not about tactics.

Something like the  Type Checking Conditions of PVS  would be cleaner,
and closer to  the mathematical usage, where your write  (f x), and do
the proof that  x is within the domain of f  separately. We could have
an explicit notation for a forthcoming proof, like `?', and just write
(divide x y ?).

If it is the case that the  expected proof is the latest thing of that
type  introduced  in the  context,  then we  can  imagine  that it  is
automatically inserted, without any goal being created.

But if  we introduce a  notation for ``the  lastest thing of  type t''
then some users are going to require other notations for other objects
of  the context,  other  implicits proof  terms,  etc. I  definitively
prefer to get a subgoal, even if it is a trivial one.

> I mean, I want to be able to use these kind of expressions in
> a Check etc., and in that case there certainly is not the
> possibility to add proof obligations.  I even might not be
> inside a goal when I do the Check: so there is not anything
> like "proving" possible then.

I don't  understand what would  be the meaning  of the last  object of
type T if you are not inside de  goal. If it is a constant c, then you
can  give it  directly, writing  directly (divide  x y  c)  instead of
(divide x y (LATEST y#0)).

-- 
Jean-Christophe FILLIATRE
  
mailto:Jean-Christophe.Filliatre AT lri.fr
  http://www.lri.fr/~filliatr