The Coq mailing list

[AUGER <Cedric.Auger AT lri.fr>]

Le Tue, 06 Apr 2010 13:32:57 +0200, Stéphane Lescuyer  
<stephane.lescuyer AT inria.fr> a écrit:

> I don't see what is the problem with assert, "assert (H : P)" is
> basically "cut P" with the goals generated the other way, so it is
> exactly what you asked for in your first message ; in particular, it
> does add an hypothesis named H of type P in the second goal.
> Note that assert can be used as pose as well : "assert (H := t)" will
> act as "pose (H := t); clearbody H".

In fact I doubt that assert is what andre wishes, as I think andre wanted  
to say,
 "assert (H: P)." produces an opaque term, and sometimes (it happened to  
me), we
 should want a transparent term with usable definition.

Simulating would be:

Goal exists (b: bool), b = true.
(*
-------------------------------------
1 subgoal:
(1/1) exists (b: bool), b = true
*)
pose (b:= _: bool).
(*
-------------------------------------
2 subgoals:
(1/2) bool
(2/2) exists (b: bool), b = true
*)
 exact true.
(*
b:= true: bool
-------------------------------------
1 subgoal:
(1/1) exists (b: bool), b = true
*)
exists b.
(*
b:= true: bool
-------------------------------------
1 subgoal:
(1/1) b = true
*)
split.
(*
Proof completed
*)
Qed.

I know this example is stupid, but replacing "pose (b:=_ : bool)" with
"assert (b: bool)" won't make proof script succeed.

I already tried a "refine (let H := _ : P in _).",
as it allowed me to define H, I thought, "That's cool it works!",
but then for the second goal, when I saw a "H: P" instead of a "H:= ...:  
P", I was quite disapointed.

So I have no real solution; all I can advice is
whether to give a full proof term in an "assume"
or to do a Lemma/Definition/Theorem... of the type you wanted and save it  
with Defined instead of Qed
before and then use it.

That makes me think of a maybe real solution, but I am not sure it works:
instead of a "pose (H := _ : P).", you should try a "Lemma H: P."
After that you enter in a nested proof with same hypotheses as the one you  
have and once the proof is completed,
try to put a "Defined." instead of a "Qed.", then you should not have a "K  
:= ...: P" in your hypothesis,
but you should be able to add it with "assume (K := H); unfold H in K.",  
and then continue as you wanted.

> HTH,
>
> Stéphane
>
> On Tue, Apr 6, 2010 at 1:22 PM, andré hirschowitz 
> <ah AT unice.fr>
>  wrote:
> > no, if I experiment correctly.
> >
> > assert generates two goals and does not forward to the second one the
> > formula produced for the first one.
> >
> > Thanks for your answer.
> >
> > ah
> >
> > > I think you are looking for the following?
> > >
> > >  assert (myname : mytype).


--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay