Open eupp opened 4 years ago
The only reason to use doma
/domb
is automation.
It's easier to prove facts stated in terms of doma r d
than about dom_rel r ⊆₁ d
by [e]auto
. The point is that [e]auto
's proof search matches on the head constant, and doma
is a much more descriptive than ⊆₁
.
This is not an actual "issue", but rather a question about the design of the library.
I am a bit confused about the relationship between
(co)dom_rel
anddoma
/domb
.dom_rel
is defined inHahnRelationsBasic.v
as follows:doma
is defined inHahnDom.v
as follows:Clearly there is a connection between the two. If we fix relation
r
then all setsd
satisfyingdoma r d
will form partially ordered set (ordered by set inclusion) withdom_rel r
as a minimal element.However, I cannot find any lemma in
Hahn
that relate these two definitions (please, correct me if I am wrong). Moreover some lemmas aboutdoma
duplicate similar lemmas fordom_rel
. For exampleand
So my question is what
doma
/domb
are useful for? Are they more convenient to work with in some situations compared todom_rel
/codom_rel
? Why there are no lemmas relating the two?BTW, just
grep
ed inweakestmoToImm
andIMM
repos. It seems thatdoma
/domb
are not used inweakestmo
at all (except two usages related to IMM), and used rarely inIMM
(and I suppose all these usages can be refactored to usedom_rel
instead).