Lra

[proux01]

This is a Work In Progress to get lra (Linear Real Arithmetic) with MathComp. The parser needs to be completed but it already handles the following examples:

From mathcomp Require Import all_ssreflect ssralg ssrnum rat.
From mathcomp Require Import lra.

Local Open Scope ring_scope.

Lemma test (F : realDomainType) (x y : F) :
  x + 2%:R * y ≤ 3%:R → 2%:R * x + y ≤ 3%:R → x + y ≤ 2%:R.
Proof.
lra.
Qed.

(* Print test. *)
(* Print Assumptions test.  (* Closed under the global context *) *)

Lemma test_rat (x y : rat) :
  x + 2%:R * y ≤ 3%:R → 2%:R * x + y ≤ 3%:R → x + y ≤ 2%:R.
Proof.
lra.
Qed.

Lemma test_rat_constant (F : realFieldType) (x : F) :
  0 ≤ x → 1 / 3 * x ≤ 2^-1 * x.
Proof.
lra.
Qed.

We also have nra and psatz.

The minimal assumption is a realDomainType because we need both a total order and a ring structure. This enables integer constants. In presence of a realFieldType, rational constants are understood.

This requires coq/coq#15921 to export micromega witness generation as Ltac1 tactics and use an elpi parser.

[proux01]

@pi8027 I think algebra-tactics is the best place for that but let me know if you disagree.

[pi8027]

Wow, this is quite surprising since I didn't think the reflexive checker of lra as is may work for any realFieldType.

@pi8027 I think algebra-tactics is the best place for that but let me know if you disagree.

I agree, but I have to spend some time understanding how it works. (Also, I'm quite busy these days...)

[proux01]

No hurry, I could do a short demo at the next MathComp (Analysis) meeting.

Here is the big picture:

• an elpi tactic reify the goals from any realField to Q (from the stdlib QArith),
• lqa is called on this giving: a varmap, a reified formula, a witness and a reflexive proof (lra checker on Q returns true),
• instead of the lemma for Q, we apply a new lemma for realField on all that.

So the reflexive checker is actually run on Q, nothing is computed in any realField.

[pi8027]

I took a quick look. This is a note for myself rather than an actual review comment.

[pi8027]

And this part explains how it works. I'm thinking about exposing some more internals of lra on the Coq side (e.g., to take a reified term instead) so that we can avoid traversing the input term twice.

[pi8027]

BTW, isn't it possible to do the last two tactic calls (change and exact) inside the match?

[proux01]

It is, the only goal of the pose is to get a resulting proof term that is smaller and looks nicer with let-ins rather than having terms like ff and varmap duplicated.

[proux01]

Following your suggestion, this is now based on coq/coq#15921 exporting micromega witness generators. We needed it anyway as the micromega builtin parser was ignoring boolean operators (&&, ||, ~~ and ==>).

[pi8027]

I guess lra cannot solve this. Some sort of preprocessing (like zify, or maybe Trakt?) is required.

[ecranceMERCE]

Hello. Trakt could indeed probably turn the current goal into this one:

forall (x y z : Z), Z.abs (x - z) <= Z.abs (x - y) + Z.abs (y - z)

To that end, it would need an embedding declaration from F to Z, as well as declaring the following mappings:

• from GRing.add on F to Z.add;
• same for opp;
• from Num.Def.normr to Z.abs;
• from Order.le to Z.le.
  Finally, it would require allowing conversion on most of these terms, so that zmodType F, numDomainType F, etc, can be identified.

Unfortunately, for a technical reason, Order.le and Num.Def.normr cannot be declared ATM. But I can make the change. I am also not sure a local embedding can be declared (as F is a variable). I think this needs further investigation.

[proux01]

Indeed looks like a case where an external preprocessing thing may be useful.

[pi8027]

Talking about preprocessing, we could also support terms like (n + 10)%:~R, and moreover, arbitrary homomorphisms. I hope my paper about Algebra Tactics is useful to implement such features.

[gares]

FYI:

https://github.com/LPCIC/coq-elpi/blob/7c070159906235b77a49d3dfe20bf92eea987887/elpi-builtin.elpi#L365

and also closed_term.

Your code also tests it does not contain axioms, but that seems a bit far fetched. Anyway, your code is fine, these apis are there just in case it becomes a bottle neck

[proux01]

Thanks, the result will then go through the migromega plugin which is expecting axiom free terms: https://github.com/coq/coq/blob/bb5e7e5fa39f11ec222b0c1434148a02f6d3c587/plugins/micromega/coq_micromega.ml#L333
hence the test.

[proux01]

Talking about preprocessing, we could also support terms like (n + 10)%:~R, and moreover, arbitrary homomorphisms. I hope my paper about Algebra Tactics is useful to implement such features.

@pi8027 thanks, done
I now consider this ready. What about the following course of action?

1. you review (no hurry, I recommend doing this commit by commit to ease the process)
2. I take your review into account / iteration of 1. and 2.
3. once ready, I add a commit to support 8.13-8.15 (with the initial hack, this will be less efficient but should be reasonably easy)
4. you merge and release 1.1.0 compatible with Coq 8.13-8.15
5. revert last commit and release 1.1.1 compatible with Coq >= 8.16

[pi8027]

@proux01 Do you think it is possible to support Coq <= 8.15 and Coq >= 8.16 in the same branch? If so, I prefer to delay dropping the support for Coq <=8.15. If not, we can consider maintaining two branches.

[pi8027]

In any case, I'm fine with the first two items.

[proux01]

Do you think it is possible to support Coq <= 8.15 and Coq >= 8.16 in the same branch?

Maybe, let me try.

[proux01]

@proux01 Do you think it is possible to support Coq <= 8.15 and Coq >= 8.16 in the same branch?

@pi8027 Done (thanks to the wonderful coq.version function of coq-elpi!). The CI is as green as it can be (Docker images for coq-dev are unfortunately broken currently).

[gares]

W.r.t compat, you skinned the cat this way which is OK, but there is also another way which may be is a bit more lightweight (but less precise).

Elpi Accumulate understand #[only="regexp"] and #[skip="regex"], so you can easily accumulate one file or another on top of the same tactic depending on the coq version.

Eg

Elpi Tactic foo.
Elpi Accumulate "common_code.elpi".
#[only="8.15.*"] Elpi Accumulate "compat_815_code.elpi". 
#[skip="8.15.*"] Elpi Accumulate "future_code.elpi".
Elpi Typecheck.

It is an OCaml regex, so it is a bit more hackish than coq.version, but it lifts the compat code selection at "compile" time.
Just FYI.

[gares]

Is anything blocking this PR?

[proux01]

Not really, it's just a rather large PR whose review requires some time.

[gares]

bump

[proux01]

@pi8027 any chance we could ship this in a new release of algebra-tactics, along the forthcoming mathcomp 1.16 and 2.0 beta (hopefully before the end of the year)? That would be great

[pi8027]

Sorry, it takes a few more days.

[proux01]

Sorry, it takes a few more days.

No worries. Once merged, I'll try to rebase #71

[pi8027]

@proux01 Could you confirm that Micromega at this moment does not provide a witness generator (like wlra_Q) accepting an input of type BFormula (Formula Z) isProp? It seems to me that the translation part is a kind of wasteful computation.

[proux01]

@pi8027 I confirm that. IIRC avoiding the translation would require non trivial changes to micromega (but my memory might betray me, I wrote that code a few months ago now).

[pi8027]

Almost done, but I ended up removing:

• the compatibility layer for Coq <= 8.15 and
• the support for large nat constants (which I plan to put back more properly).

I will push my result soon.

[pi8027]

@proux01 I will do a few more fixes and then merge, but feel free to ask questions.

[proux01]

@pi8027 thanks!

the compatibility layer for Coq <= 8.15

Well, this made sense six months ago, maybe less so now.

After a quick look, the only thing I'm a bit worried about are the ! in rfstr.bool and rfstr.prop. Maybe we should add a test for it but if the goal looks something like x <= 2 && true = true, I fear it would look for a field instance in true = true, fail and not backtrack to x <= 2 because of the !?

[pi8027]

After a quick look, the only thing I'm a bit worried about are the ! in rfstr.bool and rfstr.prop. Maybe we should add a test for it but if the goal looks something like x <= 2 && true = true, I fear it would look for a field instance in true = true, fail and not backtrack to x <= 2 because of the !?

Thanks. Done in #72 and there is no such an issue. (Note that ; is disjunction.)