Do multiple theorems allow the same name?

Using Coq
1

We need to make a name correspond to many different (but similar) theorems.
For example, unordered sets {a, b}, Obviously a∈{a, b} and b∈{a, b}
Similar trivial theorems should have the same name.
Otherwise the context will be full of garbage lemmas …

2

By definition in coq a theorem is a name (associated to a proof). Hence you cannot have two theorems with the same name. So yes the environment is filled with thousands of (necessarily distinct) names.

Require Import Ensembles.
Search In.
Full_intro: forall (U : Type) (x : U), In U (Full_set U) x
In_singleton: forall (U : Type) (x : U), In U (Singleton U x) x
Couple_r: forall (U : Type) (x y : U), In U (Couple U x y) y
Couple_l: forall (U : Type) (x y : U), In U (Couple U x y) x
Triple_m: forall (U : Type) (x y z : U), In U (Triple U x y z) y
Triple_l: forall (U : Type) (x y z : U), In U (Triple U x y z) x
Triple_r: forall (U : Type) (x y z : U), In U (Triple U x y z) z
...

Usually that is not a problem:

  • Search is quite a powerful tool to narrow your search.
  • Modules help for structuring the name space.
  • Trivial lemmas are put in hint database and you never need to name them again.
Require Import Ensembles.

Search In Couple. (* list lemmas about both In and Couple. *)

Hint Resolve Couple_l Couple_r: mySetDb.

Goal In _ (Couple _ 2 3) 2.
Proof.
  auto with mySetDb.
Qed.

Goal In _ (Couple _ 2 3) 3.
Proof.
  auto with mySetDb.
Qed.

(edited: removed useless calls to unfold)