在勒柯克

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如何自動傳遞這些參數。