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?

  • $\begingroup$ A MWE would help. Are you trying to rewrite with an equivalence relation instead of a true equality? $\endgroup$
    – Jason Rute
    Commented Sep 2, 2022 at 2:55
  • 4
    $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Commented Sep 2, 2022 at 3:00
  • 1
    $\begingroup$ 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. $\endgroup$
    – Trebor
    Commented Sep 2, 2022 at 5:38
  • 4
    $\begingroup$ 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. $\endgroup$
    – Ana Borges
    Commented Sep 2, 2022 at 9:01


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.