On the relationship between (co)dom_rel and doma/domb

[eupp]

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 and doma/domb.

dom_rel is defined in HahnRelationsBasic.v as follows:

Definition dom_rel := fun x => exists y, r x y.

doma is defined in HahnDom.v as follows:

Definition doma := forall x y (REL: r x y), d x.

Clearly there is a connection between the two. If we fix relation r then all sets d satisfying doma r d will form partially ordered set (ordered by set inclusion) with dom_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 about doma duplicate similar lemmas for dom_rel. For example

Lemma doma_rewrite : doma r d -> r ⊆ ⦗d⦘ ⨾ r.

and

Lemma dom_rel_helper (IN : dom_rel r ⊆₁ d) : r ≡ ⦗d⦘ ⨾ r.

So my question is what doma/domb are useful for? Are they more convenient to work with in some situations compared to dom_rel/codom_rel? Why there are no lemmas relating the two?

BTW, just greped in weakestmoToImm and IMM repos. It seems that doma/domb are not used in weakestmo at all (except two usages related to IMM), and used rarely in IMM (and I suppose all these usages can be refactored to use dom_rel instead).

[vafeiadis]

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 ⊆₁.