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 …
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
)