Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Port to Hierarchy Builder #71

Merged
merged 5 commits into from
Sep 22, 2023
Merged

Port to Hierarchy Builder #71

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
a13f8a0
Add .nra.cache to gitignore
proux01 Jul 11, 2023
48ea93f
Remove zmodule.v
pi8027 Sep 22, 2023
56b68aa
Port to MathComp 2
proux01 Nov 14, 2022
669119b
Avoid mentioning auto-generated names
pi8027 Sep 21, 2023
611f106
Add a few examples
proux01 Jul 18, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions .github/workflows/docker-action.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,11 +17,13 @@ jobs:
strategy:
matrix:
image:
- 'mathcomp/mathcomp:1.15.0-coq-8.16'
- 'mathcomp/mathcomp:1.16.0-coq-8.16'
- 'mathcomp/mathcomp:1.16.0-coq-8.17'
- 'mathcomp/mathcomp:1.17.0-coq-8.16'
- 'mathcomp/mathcomp:1.17.0-coq-8.17'
- 'mathcomp/mathcomp:2.0.0-coq-8.16'
- 'mathcomp/mathcomp:2.0.0-coq-8.17'
- 'mathcomp/mathcomp:2.0.0-coq-8.18'
- 'mathcomp/mathcomp-dev:coq-8.16'
- 'mathcomp/mathcomp-dev:coq-8.17'
- 'mathcomp/mathcomp-dev:coq-8.18'
- 'mathcomp/mathcomp-dev:coq-dev'
fail-fast: false
steps:
- uses: actions/checkout@v3
Expand Down
1 change: 1 addition & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ Make*.coq.conf
*#
.lia.cache
.nia.cache
.nra.cache
examples/.csdp.cache
examples/.nra.cache
examples/trace
Expand Down
1 change: 0 additions & 1 deletion Make.test-suite
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ examples/field_examples_no_check.v
examples/ring_examples_check.v
examples/ring_examples_no_check.v
examples/from_sander.v
examples/zmodule.v
examples/lra_examples.v

-R examples mathcomp.algebra_tactics.examples
Expand Down
4 changes: 2 additions & 2 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,9 +30,9 @@ ring/field expressions before applying the proof procedures.
- License: [CeCILL-B Free Software License Agreement](CeCILL-B)
- Compatible Coq versions: 8.16 or later
- Additional dependencies:
- [MathComp](https://math-comp.github.io) ssreflect 1.15 or later
- [MathComp](https://math-comp.github.io) ssreflect 2.0 or later
- [MathComp](https://math-comp.github.io) algebra
- [Mczify](https://github.com/math-comp/mczify) 1.1.0 or later
- [Mczify](https://github.com/math-comp/mczify) 1.4.0 or later
- [Coq-Elpi](https://github.com/LPCIC/coq-elpi) 1.15.0 or later (known not to work with 1.17.0)
- Coq namespace: `mathcomp.algebra_tactics`
- Related publication(s):
Expand Down
4 changes: 2 additions & 2 deletions coq-mathcomp-algebra-tactics.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -26,9 +26,9 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
depends: [
"coq" {>= "8.16"}
"coq-mathcomp-ssreflect" {>= "1.15"}
"coq-mathcomp-ssreflect" {>= "2.0"}
"coq-mathcomp-algebra"
"coq-mathcomp-zify" {>= "1.1.0"}
"coq-mathcomp-zify" {>= "1.4.0"}
"coq-elpi" {>= "1.15.0" & != "1.17.0"}
]

Expand Down
20 changes: 20 additions & 0 deletions examples/lra_examples.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,6 +46,26 @@
lra.
Qed.

Example test_div_mul x : 1 / (2 * x) <= 1 / 2 / x + 1.
Proof.
lra.
Qed.

Example test_div_inv x : 1 / x^-1 <= x + 1.
Proof.
lra.
Qed.

Example test_div_opp x : (- x)^-1 <= - x^-1 + 1.
Proof.
lra.
Qed.

Example test_div_exp x : (x ^+ 2) ^-1 <= x ^-1 ^+ 2 + 1.
Proof.
lra.
Qed.

Lemma test_lt x y :
x + 2%:R * y < 3%:R -> 2%:R * x + y <= 3%:R -> x + y < 2%:R.
Proof.
Expand Down Expand Up @@ -172,7 +192,7 @@
lra.
Qed.

Lemma vcgen_25 (n m jt j it i : F) :

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.17) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.17) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.17) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.17) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.17) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.17) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.17) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.17) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.16) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.16) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.16) 

To avoid stack overflow, large numbers in nat are interpreted as

Check warning on line 195 in examples/lra_examples.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.16) 

To avoid stack overflow, large numbers in nat are interpreted as
1 * it + -(2%:R) * i + -(1%:R) = 0 ->
1 * jt + -(2%:R) * j + -(1%:R) = 0 ->
1 * n + -(10%:R) = 0 ->
Expand Down
Loading
Loading