CODEWITHSUNDEEP
coq
Bruno
Bruno

Reputation: 864

Simplifying Rational Expressions and Proving Trivial Rational Equivalences in Coq

Which tactics can I use to perform simplifications of rational expressions and prove trivial rational equivalences as shown in the following example?

Require Import Coq.QArith.QArith.
Open Scope Q_scope.

Lemma Example : (0 + 0) / 1 == 0.

Upvotes: 0

Views: 98

Answers (1)

Vinz
Vinz

Reputation: 6057

I don't know much about rational in Coq, but if their implementation is constructive, you'll be able to simplify such expressions using simpl (you might need to first unfold some definitions) or compute. Since reflexivity is done modulo conversion, it should also solve such goals.

However, you might have trouble simplifying expression with free variable (for example that 

 forall q:Q, (q + 0) / 1 = q.

Maybe there's a tactic like omega dedicated to this task. You could maybe try with ring or lia.

Upvotes: 1

Related Questions