在Coq中处理半环

Question

这是一个简单的Coq语法新手问题。：）

我试图在半环上定义一个简单的多项式函数：

Require Import Vector.
Import VectorNotations.
Require Import Ring_theory.
Section Polynomial_def.
       Variable Asring : Type.
       Variable (asr_0 asr_1 : Asring) (asr_add asr_mul: Asring->Asring->Asring).
       Variable SRth : semi_ring_theory asr_0 asr_1 asr_add asr_mul eq.
       Fixpoint evalPolynomial {n} (a: t Asring n) (x:Asring) : Asring  :=
        match a with
            nil => asr_0
          | cons a0 p a' => asr_add a0 (asr_mul x (evalPolynomial a' x))
        end.        
    End Polynomial_def.

例如，当我在Reals上使用它时，我必须做这样的事情：

 Require Import Reals.Rdefinitions.
 evalPolynomial R R0 Rplus Rmult a v 

我怀疑应该有一个更简单的语法，我可以只传递单个数据结构（如Isabelle中的comm_ring_1），它将封装给定类型的所有字段，如R、R0、Rplus、Rmult。

Answer 1

是的，您可以将所有参数打包到一个结构中，然后将其作为参数传递，类似

Structure semiring := Semiring {
  Asring : Type;
  asr_0 : Asring;
  asr_1 : Asring;
  asr_add : Asring -> Asring -> Asring
  (* Other fields... *)
}.

然后，你可以用这个结构来重新表述你的发展：

Section Polynomial_def.
Variable sr := semiring.
Fixpoint evalPolynomial {n} (a: t (Asring sr) n) (x:Asring sr) : Asring sr :=
(* ... *)

稍后，当尝试使用它时，您只需要构建这样一个结构，并将其作为普通参数传递。您还可以使用Coq类型的类或规范结构来告诉Coq如何自动传递此类参数。