The Coq mailing list

[Virgile Prevosto <virgile.prevosto AT m4x.org>]

Hello,

Le jeu 13 oct 2005 13:01:32 CEST, Pierre Casteran
<pierre.casteran AT labri.fr>
 a ecrit:

>   When developping some large proof segmented in sections, I met the 
> following scheme.
> 
> Section S.
>   Hypothesis H : P.
> 
>  Lemma difficult_lemma : Q.
>  Admitted. (* But I presume that H is used in this proof *)
> 
>  Theorem corollary : R.
>   Proof.
>     ... apply difficult_lemma.
>  Qed.
> 
>  End S.
> 
>  Since there is no proof term for the lemma, if the corollary doesn't
> apply directly H, the discharging mechanism makes the type of
> corollary being R (and not P -> R). That means that all the
> development after S's closing will be inconsistent when I (at least)
> prove the lemma.
> 

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