L-product-0 定理

Question

我想证明以下几点：

-product-0 : ∀{l :  ℕ} → list-any (_=ℕ_ 0) l ≡ tt → -product l ≡ 0
-product-0 = {!!}

'list-any' 定义为：

list-any : ∀{ℓ}{A : Set ℓ}(pred : A → )(l :  A) → 
list-any pred [] = ff
list-any pred (x :: xs) = pred x || list-any pred xs

而_=ℕ_定义为：

_=ℕ_ : ℕ → ℕ → 
0 =ℕ 0 = tt
suc x =ℕ suc y = x =ℕ y
_ =ℕ _ = ff

我正在尝试理解这部分内容：list-any (_=ℕ_ 0) l ≡ tt

是(_=ℕ_ 0) ≡ (pred : A → )和l ≡ (l : A)吗？

如果是这样，我想帮助理解谓词。 (=ℕ 0) 是什么意思？我假设 =ℕ 应用如下：

L return 中的每个元素（元素 =ℕ 0）。

这是正确的吗？我试图通过使用列表 l1:

来证明定理

-product-0 : ∀{l :  ℕ} → list-any (_=ℕ_ 0) l ≡ tt → -product l ≡ 0
-product-0 l1 = {!!}

但出现以下错误：

I'm not sure if there should be a case for the constructor refl,
because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
  list-any (_=ℕ_ 0) l ≟ tt
when checking that the expression ? has type -product .l ≡ 0

感谢您提供的任何帮助！

编辑（回复 1）：

我把箱子拆开，得到：

-product-0 : ∀{l :  ℕ} → list-any (_=ℕ_ 0) l ≡ tt → -product l ≡ 0
-product-0 x = {!!}

这是我想要的吗？我拆分的时候填了x。

还可以看出：

Goal: -product .l ≡ 0

其中：

x  : list-any (_=ℕ_ 0) .l ≡ tt
.l :  ℕ

此时程序要我解决什么问题？我怎样才能证明

-product-0 x 在逻辑上等同于 -product .l ≡ 0?

Answer 1

I'm trying to understand this part: list-any (=ℕ 0) l ≡ tt

Is (=ℕ 0) ≡ (pred : A → ) and l ≡ (l : A)?

您是正确的，_=ℕ_ 0 被替换为 pred。 _=ℕ_ 0 表示将函数 _=ℕ_ 应用于 0 的结果。由于 _=ℕ_ 是一个二元函数，将它应用于一个参数会产生一个函数 ℕ -> ，这正是 list-any 所期望的。

至于另一个问题，您试图在 l 上进行模式匹配，但它是隐式的：在您的示例中 l1 实际上表示 list-any (_=ℕ_ 0) l ≡ tt 参数，因为那是第一个显式参数。您必须使用方括号引入隐式参数：

-product-0 : ∀{l :  ℕ} → list-any (_=ℕ_ 0) l ≡ tt → -product l ≡ 0
-product-0 {l1} = {!!}

编辑：

我假设您使用的是 Emacs agda 模式。当您查看上下文时，隐式参数以点为前缀，如 .l : ℕ。如果你在一个新的 Agda 上，如果你想在 .l 上拆分，在洞里写 { .l }，然后按 C-c-c。另一种解决方法是在函数定义中用括号引入参数，就像我上面写的那样，然后在洞里写 { l1 } ，然后按 C-c-c。

或者，您可以使列表参数显式化并省去括号：

-product-0 : (l :  ℕ) → list-any (_=ℕ_ 0) l ≡ tt → -product l ≡ 0
-product-0 l = ?

请记住，在函数定义中，不带括号的参数是显式参数，您可以根据它们在类型中出现的顺序在它们之前或之间插入隐式参数。您还可以通过类型中的名称来引用隐式参数。例如：

foo : Nat -> {l : list Nat} -> Nat -> Nat
foo n m = ?  -- now "n" refers to the first Nat and "m" refers to the last argument

foo : Nat -> {l : list Nat} -> Nat -> Nat
foo n {l} m = ? -- now "l" refers to the list.

foo : Nat -> {l : list Nat} -> Nat -> Nat
foo n {l = list} m = ? -- refer to "l" by the name "list" here.

L-product-0 定理

L-product-0 Theorem

agda