The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Thank you Virgile,

  That is exactly what I needed.

  I just added an "Opaque" after the Definition. After having filled
 the Admitted with a full proof, there was nothing to change in the rest
  of the proof.

 Cheers,

Pierre



Selon Virgile Prevosto 
<virgile.prevosto AT m4x.org>:


>
> We had more or less the same issue in Focal. A possible solution would
> be to rely on an auxiliary (admitted) lemma, and define difficult_lemma
> with an explicit reference to H. It is not very elegant, but it works:
>
> Parameter P Q:Prop.
> Section S.
> Hypothesis H : P.
>
>   Lemma difficult_lemma_aux : Q.
>   Admitted.
>
>   Definition difficult_lemma : Q :=
>     let _ := H in
>       difficult_lemma_aux.
>
>   Theorem corollary : Q.
>       apply difficult_lemma.
>       Qed.
> End S.
>
> Check difficult_lemma.
> (* difficult_lemma : P -> Q *)
>
> Check corollary.
> (* corollary : P -> Q *)
>
> --
> E tutto per oggi, a la prossima volta
> Virgile
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran

http://www.labri.fr/Perso/~casteran/

(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.