0
$\begingroup$

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?

Improve this question
$\endgroup$
4
  • $\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

0

Reset to default

Your Answer

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

Browse other questions tagged or ask your own question.