feat: add depends on rocq concept status

[ayhon]

Description

Adds support for specifying a concept not being implemented because it depends on some other identifiers. Nothing is done with this information yet.

Fixes #327

Checklist

• My code follows the mathlib naming and code style conventions
• I have updated PORTING.md as appropriate
• I have added my name to the authors section of any appropriate files

[MackieLoeffel]

@ayhon Is this still relevant or can this be closed?

[ayhon]

I made this PR as a proof-of-concept to have a new "depends_on" status for rocq_concept. If we're not interested in implementing such a feature, this PR should be closed, but I don't know whether @lzy0505 had a look at it / had any opinions on it. Reference to the related Zulip conversation.

[lzy0505]

Sorry for the late reply. I think in general it is a nice feature.

However, I'm not sure whether the new depends_on status should be part of rocq_concept.
In my experience, I usually wanted to mark a Rocq definition/lemma that we do want to have a one-to-one map in Lean blocked by missing Rocq lemmas. rocq_concept is only for those that do not have such a clear correspondence, and I cannot use your feature to do it. Perhaps you implemented this feature for other things? Can you give some concrete examples? For my use case, we can instead add a new rocq_blocked command with a "depends-on" list.