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
    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
    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
    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
    Sep 2, 2022 at 9:01


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.