The Coq mailing list

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

Li Long wrote:

> Thanks all for helping me!
>  
> Pierre's example does help me a lot to recognise the problem inside
> my formalization of the form
> forall ( T : Set )( A : Prop ), ( forall x : T, A ) -> A.
>  
> It seems there are times the domain that quantified variables refer to
> needs to be non-empty, or it is a implicit rule in natural deduction that
> the domain is always non-empty when there are quantified variables
> refer to. I have not met comments of the latter in literatures about 
> logic,
> and I would not like to formalize logic lemmas in the style of the 
> latter,
> because I think it reduce the power of many logic lemmas.But if the
> former is the case, how can I tell whether a non-empty premise should be
> added when formalizing a logic lemma, possibly a complicated one?


You can prove your results within a section containing some non-emptiness
hypothesis. If this hypothesis is not used in some proof, it will not appear
after closing the section.

In the following example, I add some non-emptiness hypothesis through a 
witness u.
(Notice that I could have declared H : exists u:U, u=u  as well).

The proof of L depends on this hypothesis, but not L'.
If you check L' after sections's closing you will see that this 
hypothesis doesn't
appear.

Hope this helps,

Pierre
Section Non_empty.
Variable U : Set.
Variable u : U. (* U's inhabited *)

Variable A : Prop.
Lemma L : (forall (x:U), A) -> A.
Proof.
 intro H;apply H;exact u.
Qed.

Lemma L' : forall (x:U),x = x.
auto.
Qed.

End Non_empty.

Check L.

(*
L
    : forall U : Set, U -> forall A : Prop, (U -> A) -> A
*)

Check L'.

(*
L'
    : forall (U : Set) (x : U), x = x
*)



Section Non_empty2.
Variable U : Set.
Hypothesis inh : exists u:U, True.

Variable A : Prop.
Lemma L2 : (forall (x:U), A) -> A.
Proof.
 case inh.
 auto.
Qed.
End Non_empty2.






>  
>  
> Cheers,
>  
>  
> --
> Long
>