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

对于我的第一次正式化。我想在精益中定义多项式。第一次尝试如下：测试多项式定义（从自然数到整数）

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

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

回答

相关问题