From 1c20aefd79c29411715c137be58c9a873ce4b386 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Fri, 22 Sep 2023 14:06:17 +0200 Subject: [PATCH] Fix --- theories/common.v | 24 +++++++++++++++++++++++- theories/lra.v | 25 +------------------------ theories/ring.elpi | 36 ++++++++++++++++++++++++------------ theories/ring.v | 29 ++--------------------------- 4 files changed, 50 insertions(+), 64 deletions(-) diff --git a/theories/common.v b/theories/common.v index 9d6cfe0..e88a37c 100644 --- 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 index 70e206c..ea1fade 100644 --- 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" }. \ No newline at end of file +Elpi Query lp:{{ canonical-init library "canonicals.db" }}. diff --git a/theories/ring.elpi b/theories/ring.elpi index 383f343..39c8d6b 100644 --- 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 index 5ced579..afedb5c 100644 --- 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" }}.