How to proof a simple statement about rational numbers

Using Coq
1

Hello!

I’m completely stuck with this. Could anybody give me a hint how to proof the following?

Require Import QArith.
Local Open Scope Q_scope.

Lemma example1 : forall (v : Q), (12.0 = (2.0 * (v - 4.0))) -> v = 10.0.
2

Unfortunately, this is wrong, as can be seen by proving the following property:

Goal (12.0 = (2.0 * (10.0 - 4.0))) -> False.
Proof. discriminate. Qed.

The important point is that the type Q is a just a non-normalized pair of integers. So, you can use this type to perform arithmetic, but you cannot use it to perform reasoning, especially when it comes to equality.

Instead, you need to use a different notion of equality:

Require Import QArith Lqa.
Local Open Scope Q_scope.

Lemma example1 : forall (v : Q), Qeq 12.0 (2.0 * (v - 4.0)) -> Qeq v 10.0.
Proof. intros. lra. Qed.
3

Thanks a lot for your answer.

I’m trying to sort things out:

Require Import QArith.
Local Open Scope Q_scope.

Print "=".
Print Qeq.

Results in:

Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x.
Qeq = 
fun p q : Q => (Qnum p * QDen q)%Z = (Qnum q * QDen p)%Z
     : Q -> Q -> Prop

So “=” is basically maps to “eq_refl”.

To follow this logic, when using nat to formulate my original statement, I need to use “Nat.eq” nat -> nat -> Prop and not “Neq” (which does not exists) or eq (which maps to eq_refl).

Require Import Arith.
Lemma example2 : forall (v : nat), Nat.eq 12 (2 * (v - 4)) -> Nat.eq v 10.

in this case the tactics you provided - even if the proposition is very similar - do not work.

Trying to convert my proposition to “Z” or “R” I completely failed. There is no “Zeq” or “Z.eq”. And I think I have a kind of an impression why there is no “Req” or similar. (Is there any way to express and proof the proposition with elements from R?)

The different namings are very confusing. Also the fact, that the same tactics do not work for Q and N.

4

There is a “generic” notion of equality called “eq”, which recognizes when two objects are exactly the same (there is never a way to distinguish them). If two objects are the same, then any function applied to these objects return the same result.

Your sentence

is wrong.

“=” maps to eq , not eq_refl. “eq” means equals, and you can use it to express that sentences that are false, like 3 = 4 . eq_refl is a theorem, which says that any object is equal to itself. So you can use “eq” to build logical sentences that are either true or false, but you can only use eq_refl to build proofs. When you build a proof, this proof actually proves a sentence, and this sentence is true.

Working with rational numbers is confusing, but you need to first understand the concepts of equality and logical sentences. So I suggest you start with a tutorial that will only mention natural numbers, and then you can climb the ladder of more and more complicated number systems. Rational numbers are confusing because their notion of equality is different from other data-types. Real numbers live in yet another world, when numbers are concerned.

5

If you really want to see what a notation symbol means, use Locate.

Locate "=".
Locate "==".

Incidentally, == is the infix notation for Qeq.

The reason for == is because in Coq’s Q it is possible for two different fractions to be unequal while still representing the same rational number. For example 2/3 is not the same fraction as 4/6 but 2/3 is the same rational number as 4/6.

From Coq Require Import QArith.
Local Open Scope Q_scope.

Goal ~ 2/3 = 4/6.
Proof.
  discriminate.
Qed.

Goal 2/3 == 4/6.
Proof.
  reflexivity.
Qed.
1 Like