# If I make some new structure like Q, then can I use 'rewrite' tactic for my new structure in Coq?

From $$\mathbb{Q}$$, the set of all rational numbers, I make some new structure $$I$$, and also make strict order and (equivalence) equality on $$I$$.

I want to use rewrite tactic for my defined relations (strict order, or equality). For example,

H : a < const_I 0
H0 : const_I 0 == b


I want to write

rewrite H0 in H.


However, this writing tells me that "not a rewritable relation".

Is there a way to use some new defined relations with 'rewrite' tactic?

• A MWE would help. Are you trying to rewrite with an equivalence relation instead of a true equality? Commented Sep 2, 2022 at 2:55
• If so how do you know that the inequality is still true after the rewrite? You would need a lemma showing your order respects the equivalence relation. I think Coq has generalized rewriting for this purpose. Commented Sep 2, 2022 at 3:00
• Coq surely needs to prevent you from naming the < relation as == and rewriting. So you should first prove theorems about your == to convince Coq it is rewritable.
– Trebor
Commented Sep 2, 2022 at 5:38
• Yes, there is! It's called generalized rewriting. As the others are saying, you need to prove some extra lemmas, and then rewrite will do the job. Commented Sep 2, 2022 at 9:01