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 https://github.com/coq/coq/pull/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]

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]

Really sorry for the late response. Since I would like to use this feature in the MC school next month, I will do a minimal check and merge. (But, the compatibility with MC 2.0 would require more work.)

[proux01]

Arg indeed, algebra-tactics is not in Nix and wasn't tested in the CI. Looks like there is no port to HB yet. I'll try to have a look.

[pi8027]

Currently, some subtyping functions are hard-coded in the reification procedures. It would be nice if we could query them from HB without sacrificing performance. https://github.com/math-comp/algebra-tactics/blob/d4de5a2d05ab500017b272d9d37af7a05818d01e/theories/common.elpi#L143 There is a related remark in the ITP'22 paper:

Our twofold reflection scheme and its preprocessing step to support homomorphisms allow us to adapt an existing reflexive tactic to new operators without either reimplementing the whole tactic or reifying similar terms twice (Section 4.2). However, it does not let users extend an existing preprocessor with new rules as the ppsimpl tactic [7] does, although ppsimpl is not flexible enough to cover our use cases. Since Coq-Elpi provides the abilities to generate inductive data types, Coq constants, and Elpi rules, we could improve this situation by writing an Elpi program that produces a reflexive preprocessor and reification rules from their high-level descriptions. Furthermore, we could integrate such an enhancement to Hierarchy Builder [19] to utilize metadata about the hierarchy of structures in reification.

[gares]

The names of these coercions are "private", but we can surely give them a public name if needed. Querying HB database is also a possibility, but I don't think we have this specific predicate/database. For an alpha release of MC 2.0, using the "private" names of the coercions may be the only option.

[proux01]

So here is a hierarchy-builder port that seems to work: https://github.com/proux01/algebra-tactics/tree/hierarchy-builder (for master branch, haven't tried yet for this lra branch)

[pi8027]

@proux01 If you agree, I will do a minimal fix for some of the issues above and then merge (by tomorrow).

[pi8027]

So here is a hierarchy-builder port that seems to work: https://github.com/proux01/algebra-tactics/tree/hierarchy-builder (for master branch, haven't tried yet for this lra branch)

Could you open another PR for this? Thanks a lot.

[pi8027]

A related math question (not expecting an answer but FTR): Let's say R and S are ordered rings and n and m are natural numbers. Is it always possible to prove things like n%:R <= m%:R :> R -> n%:R <= m%:R :> S using ~lia~ lra, by embedding them into a larger ordered ring?

[proux01]

I guess you mean "using lra"?

[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.)