dependent-type - 测试多项式定义（从自然数到整数）

Question

对于我的第一次形式化。我想在精益中定义多项式。第一次尝试如下所示：

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:ℕ) 
 ()
 ()
 )

也欢迎对定义本身进行反馈。

score 1 · Accepted Answer

的公式def polynomial不起作用。您将函数标记为多项式，但这不能从逻辑本身使用。特别是，它不允许我们为多项式设置类型类实例。

我们想要的是一个子类型：

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

有了这个我们可以设置一个实例

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

1 回答 1