The Coq mailing list

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

I checked it for my previous example, and it works
(but I had no hypothesis, so I am not sure it really works)

Goal exists b: bool, b = true.
 Lemma b: bool.
  exact true.
 Defined.
 exists b.
 split.
Qed.

Which (if I am correct), means that Jean-François Monin example scheme  
would be:

Goal forall x : X, exists y: Y, complicated_property x y.
intros x.
  Lemma y: Y.
   apply many_functions_in_order_to_build_y_from_x.
  Defined.
  exists y.
  (* Here you may want to use "unfold y." *)
  apply many_lemmas_for_proving_complicated_property_x_y.
Qed.

and should work.
This solution is not as convenient as having a dedicated tactic, but:
* the number of characters you have to type with this method minus the  
numbers you should have with a tactic is below 20,
  which is largely acceptable
* the Lemma...Defined makes the proof more readable IMO.
Flaws remain:
* we have a new defined term outside of our proof, which name is "y" and  
type is:
forall (H0: ...) (H1: ...) ..., Y.
And we should want to erase this term.
* This technique cannot be used inside Ltac.

A trick to solve the first flaw would have been to open a section before  
"Goal" then use "Let" instead of "Lemma"
and close our section, but this doesn't seem to work (the Let is unusable  
once defined in our goal).

Le Tue, 06 Apr 2010 14:07:45 +0200, Jean-Francois Monin  
<jean-francois.monin AT imag.fr> a écrit:

> As far as i understand, the very value of H may be useful
> and defining it in one step may be hard.
>
> Example:
>
> Goal forall x : X, exists y: Y, complicated_property x y.
> intros x. pose (y: Y).
>   apply many_functions_in_order_to_build_y_from_x.
>   exists y. apply many_lemmas_for_proving_complicated_property_x_y.
> Qed.
>
> Here neither cut nor assert is the answer.
>
> JF


--
Cédric AUGER

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