The Coq mailing list

["Jojgov, G.I." <g.i.jojgov AT TUE.nl>]

Hello,

 

In the two examples below I see different behaviour of Coq when it generalizes Hypotheses in a section after it was closed:

 

Section X.

Variable k:nat.

Hypothesis pos_k: 0<k.

Axiom Test_X:forall P:nat-> Prop, 0<k .

End X.

 

Section Y.

Variable k:nat.

Hypothesis pos_k: 0<k.

Lemma Test_Y:forall P:nat-> Prop, 0<k .

intros.

assumption.

Save.

End Y.

 

 

It seems that because the Hypothesis pos_k in section X is not used, it is not generalized:

 

Check Test_X.

> Test_X

>  : forall k : nat, (nat -> Prop) -> 0 < k

 

Check Test_Y.

> Test_X

>  : forall k : nat, 0 < k -> (nat -> Prop) -> 0 < k

 

Is there a way to force Coq to generalize hypotheses that are not used so that the type of Test_X becomes the same as that of Test_Y without actually using pos_k in a proof?

 

Thanks in advance,

 

Georgi