CODEWITHSUNDEEP
coqcoq-tacticinequalityrational-numberssreflect
Mohammad Shaheer
Mohammad Shaheer

Reputation: 1

Proving non-linear equations and inequalities involving rational numbers in Coq

I'm trying to formalize a stable-coin protocol using the Coq Interactive Theorem Prover. The proofs I have involve a lot of manipulation of linear and non-linear equations involving rational numbers. For now, I'm using the standard Coq library of rational numbers but it involves a lot of proof writing. I tried using tactics like 'nra' and 'lra' for finding proofs automatically but it gives me an error saying 'Tactic failure: Cannot find witness'. As an example, I was trying to prove this simple lemma using the proof given below.

Lemma test (qs : Q) (n : Q) (nu : Q) (ex : Q) :
  qs > 0 /\ n > 0 /\ nu > 0 /\ ex > 0 -> 
  qs <= ex -> qs / ex <= 1.
Proof.
    intros. lra.
Qed.

but it gave me an error saying 'Tactic failure: Cannot find witness'. I tried destructing the rational numbers but couldn't complete the proof.

My questions are:

  1. How to solve the above proof in the simplest way possible?
  2. Are there any other libraries that would help me write simple proofs for inequalities and equations rational numbers and also automatically find proofs for simple lemmas as given above?
  3. Are there examples of papers/code that deal with algebraic manipulations involving rational/real numbers?

Any sort of help would be much appreciated.

Hope you all have an amazing day!

Upvotes: 0

Views: 61

Answers (1)

larsr
larsr

Reputation: 5811

I know you are looking for an automated tactic, which I don't know about, but there are lemmas in the library, and it's important to know how to look for them with the Search command. You can query for patterns that occur in them, parts of their names etc. Very handy. I searched for theorems related with Search (_ %Q <= _ -> _). and Search (1 %Q * _). (the %Q marks it as a Q type), and found two useful theorems. Removing the unused variables in your example gives this proof:

Require Import QArith.

Lemma foo (a b:Q) (H: 0 < b <= a): 1 <= a/b. 
    intros; apply Qle_shift_div_l; rewrite ?Qmult_1_l; apply H. 
Qed.

Upvotes: 1

Related Questions