在勒柯克

Question

与半环的工作这是一个简单的勒柯克语法新手的问题:)

我想对semi_rings定义简单的多项式函数：

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. 

当我使用它的实数，例如，我必须做这样的事情：

Require Import Reals.Rdefinitions. 

evalPolynomial R R0 Rplus Rmult a v 

我怀疑应该有一个简单的语法，在那里我可以只通过单一的数据结构（如comm_ring_1在伊莎贝尔），这将EN封装所有类型的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如何自动传递这些参数。