測試多項式定義（從自然數到整數）

對於我的第一次正式化。我想在精益中定義多項式。第一次嘗試如下：測試多項式定義（從自然數到整數）

def polynomial (f : ℕ → ℤ ) (p: (∃m:ℕ , ∀ n : ℕ, implies (n≥m) (f n = (0:ℤ) ))):= f

現在想用測試我的定義：

def test : ℕ → ℤ 
| 0 := (2:ℤ) 
| 1 := (3:ℤ) 
| 2 := (4:ℤ) 
| _ := (0:ℤ)

但我有麻煩構建證明期限：

def prf : (∃m:ℕ , ∀ n : ℕ, implies (n≥m) (test n = (0:ℤ) )):= 
exists.intro (3:ℕ) (
assume n : ℕ, 
nat.rec_on (n:ℕ) 
() 
() 
)

而且反饋在定義本身是受歡迎的。

來源

2017-10-19 Jens Wagemaker

一個'係數list'可能是一個更簡單的定義與 –

合作@ SebastianUllrich我認爲，但是如果你想定義一個加法和乘法，如果你有兩個不同程度的多項式會不會更難？ –

@JensWagemaker列表會簡單一些，但是我們仍然需要一個假設：如果列表不是'empty'，那麼head元素不應該是'0'。否則，我們會有'0 * x + 1'和'1'是不同的多項式。列表工作，假設列表的頭部是較低的係數，即'[a，b，c]'表示多項式'c * x^2 + b * x + a'。對於'prf'：在這種情況下，你不想使用遞歸，而是使用'match'。 0,1和2的情況應該與證明'dec_trivial'一起工作。 – Johannes

def polynomial的公式不起作用。你標籤你的函數是一個多項式，但是這不能用於邏輯本身。尤其是，它不允許我們爲多項式設置類型實例。

我們要的是一個亞型，而不是：

def polynomial (A : Type) [ring A] : Type := 
{p : ℕ -> A // ∃ m : ℕ, ∀ n ≥ m, p n = 0}

與這一點，我們可以設置一個實例

instance {A : Type} [ring A] : polynomial A := ...

來源

2017-10-21 14:29:31 Johannes

'//'的含義是什麼？另外我找不到{...}的含義，你是否在這裏聲明一個結構？是否有可能做更詳細的相同的定義？ –

'{x：A // p x}'是'A'中所有元素'x'的子類型，其中'p x'成立。 '//'是'{_：_ // _}'語法的一部分。 – Johannes

測試多項式定義（從自然數到整數）

回答

相關問題