Fix

math-comp · Sep 22, 2023 · 1c20aef · 1c20aef
1 parent 3074c8d
commit 1c20aef
Show file tree

Hide file tree

Showing 4 changed files with 50 additions and 64 deletions.
diff --git a/theories/common.v b/theories/common.v
@@ -1,3 +1,4 @@
+From elpi Require Import elpi.
 From Coq Require Import QArith.
 From Coq.micromega Require Import OrderedRing RingMicromega.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
@@ -1367,4 +1368,25 @@ Qed.
 
 End RealField.
 
-Import Instances.
+Elpi Db canonicals.db lp:{{
+
+pred canonical-nat-nmodule o:constant.
+pred canonical-nat-semiring o:constant.
+pred canonical-nat-comsemiring o:constant.
+pred canonical-N-nmodule o:constant.
+pred canonical-N-semiring o:constant.
+pred canonical-N-comsemiring o:constant.
+pred canonical-int-nmodule o:constant.
+pred canonical-int-zmodule o:constant.
+pred canonical-int-semiring o:constant.
+pred canonical-int-ring o:constant.
+pred canonical-int-comring o:constant.
+pred canonical-int-unitring o:constant.
+pred canonical-Z-nmodule o:constant.
+pred canonical-Z-zmodule o:constant.
+pred canonical-Z-semiring o:constant.
+pred canonical-Z-ring o:constant.
+pred canonical-Z-comring o:constant.
+pred canonical-Z-unitring o:constant.
+
+}}.
diff --git a/theories/lra.v b/theories/lra.v
@@ -391,29 +391,6 @@ Strategy expand [Reval_pop2 Reval_bop2 Reval_op2].
 Strategy expand [Reval_formula Rnorm_formula Fnorm_formula].
 Strategy expand [Reval_PFormula Feval_PFormula].
 
-Elpi Db canonicals.db lp:{{
-
-pred canonical-nat-nmodule o:constant.
-pred canonical-nat-semiring o:constant.
-pred canonical-nat-comsemiring o:constant.
-pred canonical-N-nmodule o:constant.
-pred canonical-N-semiring o:constant.
-pred canonical-N-comsemiring o:constant.
-pred canonical-int-nmodule o:constant.
-pred canonical-int-zmodule o:constant.
-pred canonical-int-semiring o:constant.
-pred canonical-int-ring o:constant.
-pred canonical-int-comring o:constant.
-pred canonical-int-unitring o:constant.
-pred canonical-Z-nmodule o:constant.
-pred canonical-Z-zmodule o:constant.
-pred canonical-Z-semiring o:constant.
-pred canonical-Z-ring o:constant.
-pred canonical-Z-comring o:constant.
-pred canonical-Z-unitring o:constant.
-
-}}.
-
 Elpi Tactic lra.
 Elpi Accumulate Db canonicals.db.
 Elpi Accumulate File common lra.
@@ -425,4 +402,4 @@ Tactic Notation "psatz" integer(n) :=
   elpi lra "psatz_witness" "tacF" "tacR" ltac_int:(n).
 Tactic Notation "psatz" := elpi lra "psatz_witness" "tacF" "tacR" (-1).
 
-Elpi Query lp:{ canonical-init library "canonicals.db" }.
+Elpi Query lp:{{ canonical-init library "canonicals.db" }}.
diff --git a/theories/ring.elpi b/theories/ring.elpi
@@ -7,26 +7,36 @@
 pred mk-ring-morphism i:term, o:rmorphism, o:term, o:term, o:list prop.
 mk-ring-morphism Ty rmorphism-nat {{ semiring_correct }} {{ target_nat }} Env :-
   coq.unify-eq Ty {{ nat }} ok, !,
+  canonical-nat-nmodule NatNmodule,
+  canonical-nat-semiring NatSemiRing,
   semiring-env SREnv,
-  Env = [target-nmodule (global (const { canonical-nat-nmodule })),
-         target-semiring (global (const { canonical-nat-semiring })) | SREnv].
+  Env = [target-nmodule (global (const NatNmodule)),
+         target-semiring (global (const NatSemiRing)) | SREnv].
 mk-ring-morphism Ty rmorphism-N {{ semiring_correct }} {{ target_N }} Env :-
   coq.unify-eq Ty {{ N }} ok, !,
+  canonical-N-nmodule NNmodule,
+  canonical-N-semiring NSemiRing,
   semiring-env SREnv,
-  Env = [target-nmodule (global (const { canonical-N-nmodule })),
-         target-semiring (global (const { canonical-N-semiring })) | SREnv].
+  Env = [target-nmodule (global (const NNmodule)),
+         target-semiring (global (const NSemiRing)) | SREnv].
 mk-ring-morphism Ty rmorphism-int {{ ring_correct }} {{ target_int }} Env :-
   coq.unify-eq Ty {{ int }} ok, !,
+  canonical-int-nmodule IntNmodule,
+  canonical-int-semiring IntSemiRing,
+  canonical-int-zmodule IntZmodule,
   ring-env REnv,
-  Env = [target-nmodule (global (const { canonical-int-nmodule })),
-         target-semiring (global (const { canonical-int-semiring })),
-         target-zmodule (global (const { canonical-int-zmodule })) | REnv].
+  Env = [target-nmodule (global (const IntNmodule)),
+         target-semiring (global (const IntSemiRing)),
+         target-zmodule (global (const IntZmodule)) | REnv].
 mk-ring-morphism Ty rmorphism-Z {{ ring_correct }} {{ target_Z }} Env :-
   coq.unify-eq Ty {{ Z }} ok, !,
+  canonical-Z-nmodule ZNmodule,
+  canonical-Z-semiring ZSemiRing,
+  canonical-Z-zmodule ZZmodule,
   ring-env REnv,
-  Env = [target-nmodule (global (const { canonical-Z-nmodule })),
-         target-semiring (global (const { canonical-Z-semiring })),
-         target-zmodule (global (const { canonical-Z-zmodule })) | REnv].
+  Env = [target-nmodule (global (const ZNmodule)),
+         target-semiring (global (const ZSemiRing)),
+         target-zmodule (global (const ZZmodule)) | REnv].
 mk-ring-morphism Ty (rmorphism U V' SR R' UR' none (x\ x)) Lem CR Env :- !,
   std.assert-ok! (coq.unify-eq Ty {{ GRing.Nmodule.sort lp:U }})
                  "Cannot find a declared nmodType",
@@ -104,7 +114,8 @@ ring-env
    (pi In\ quote.build.Z-constant In {{ @PEc Z lp:In }} :- !),
    (quote.build.N-constant {{ N0 }} {{ @PEc Z Z0 }} :- !),
    (pi In\
-      quote.build.N-constant {{ Npos lp:In }} {{ @PEc Z (Zpos lp:In) }} :- !)].
+      quote.build.N-constant {{ Npos lp:In }} {{ @PEc Z (Zpos lp:In) }} :- !)]
+  :- !.
 
 pred field-env o:list prop.
 field-env
@@ -120,7 +131,8 @@ field-env
    (pi In\ quote.build.Z-constant In {{ @FEc Z lp:In }} :- !),
    (quote.build.N-constant {{ N0 }} {{ @FEc Z Z0 }} :- !),
    (pi In\
-      quote.build.N-constant {{ Npos lp:In }} {{ @FEc Z (Zpos lp:In) }} :- !)].
+      quote.build.N-constant {{ Npos lp:In }} {{ @FEc Z (Zpos lp:In) }} :- !)]
+  :- !.
 
 pred if-verbose i:prop.
 if-verbose P :- get-option "verbose" tt, !, P.

diff --git a/theories/ring.v b/theories/ring.v
@@ -1,4 +1,4 @@
-From elpi Require Export elpi.
+From elpi Require Import elpi.
 From Coq Require Import ZArith Ring Ring_polynom Field_theory.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.
@@ -437,29 +437,6 @@ Strategy expand [nat_of_large_nat N_of_large_nat Z_of_large_nat].
 Strategy expand [Reval Meval SemiRing.Rnorm SemiRing.Mnorm].
 Strategy expand [Ring.Rnorm Ring.Mnorm Field.Rnorm Field.Mnorm PEeval FEeval].
 
-Elpi Db canonicals.db lp:{{
-
-pred canonical-nat-nmodule o:constant.
-pred canonical-nat-semiring o:constant.
-pred canonical-nat-comsemiring o:constant.
-pred canonical-N-nmodule o:constant.
-pred canonical-N-semiring o:constant.
-pred canonical-N-comsemiring o:constant.
-pred canonical-int-nmodule o:constant.
-pred canonical-int-zmodule o:constant.
-pred canonical-int-semiring o:constant.
-pred canonical-int-ring o:constant.
-pred canonical-int-comring o:constant.
-pred canonical-int-unitring o:constant.
-pred canonical-Z-nmodule o:constant.
-pred canonical-Z-zmodule o:constant.
-pred canonical-Z-semiring o:constant.
-pred canonical-Z-ring o:constant.
-pred canonical-Z-comring o:constant.
-pred canonical-Z-unitring o:constant.
-
-}}.
-
 Elpi Tactic ring.
 Elpi Accumulate Db canonicals.db.
 Elpi Accumulate File common ring ring_tac.
@@ -471,8 +448,6 @@ Tactic Notation "#[" attributes(A) "]" "ring" := ltac_attributes:(A) elpi ring.
 Tactic Notation "#[" attributes(A) "]" "ring" ":" ne_constr_list(L) :=
   ltac_attributes:(A) elpi ring ltac_term_list:(L).
 
-Elpi Query lp:{ canonical-init library "canonicals.db" }.
-
 Elpi Tactic field.
 Elpi Accumulate Db canonicals.db.
 Elpi Accumulate File common ring field_tac.
@@ -485,4 +460,4 @@ Tactic Notation "#[" attributes(A) "]" "field" :=
 Tactic Notation "#[" attributes(A) "]" "field" ":" ne_constr_list(L) :=
   ltac_attributes:(A) elpi field ltac_term_list:(L).
 
-Elpi Query lp:{ canonical-init library "canonicals.db" }.
+Elpi Query lp:{{ canonical-init library "canonicals.db" }}.