如何使用 "with" 从函数中恢复中间计算结果？
How to recover intermediate computation results from a function using "with"?
我写了一个关于自然数的函数，它使用带有抽象的运算符 _<?_。
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
fun : ℕ → ℕ → Maybe ℕ
fun x y with x <? y
... | yes _ = nothing
... | no _ = just y
我想证明如果用fun计算的结果是nothing那么原来的两个值（x和y）满足x < y.
到目前为止，我所有的尝试都未能证明 属性:
prop : ∀ (x y)
→ fun x y ≡ nothing
→ x < y
prop x y with fun x y
... | just _ = λ()
... | nothing = λ{refl → ?} -- from-yes (x <? y)}
-- This fails because the pattern matching is incomplete,
-- but it shouldn't. There are no other cases
prop' : ∀ (x y)
→ fun x y ≡ nothing
→ x < y
prop' x y with fun x y | x <? y
... | nothing | yes x<y = λ{refl → x<y}
... | just _ | no _ = λ()
--... | _ | _ = ?
总的来说，我发现使用 with-abstraction 很痛苦。这可能是因为 with 和 | 在后台隐藏了一些魔法。我想了解 with 和 | 的真正作用，但 "Technical details" 目前无法理解。您知道去哪里寻找以了解如何解释它们吗？
具体解决方案
您需要在函数中进行大小写拆分的同一元素上进行大小写拆分：
prop : ∀ x y → fun x y ≡ nothing → x < y
prop x y _ with x <? y
... | yes p = p
在旧版本的 Agda 中，您必须编写以下内容：
prop-old : ∀ x y → fun x y ≡ nothing → x < y
prop-old x y _ with x <? y
prop-old _ _ refl | yes p = p
prop-old _ _ () | no _
但是现在你可以完全忽略导致直接矛盾的情况，在这种情况下，nothing 和 just smth 永远不会相等。
详细说明
要了解 with 的工作原理，您首先需要了解 Agda 中如何使用定义相等来减少目标。定义相等性根据其输入的结构将函数调用与其关联的表达式绑定在一起。在 Agda 中，通过在函数的不同情况的定义中使用等号很容易看出这一点（尽管由于 Agda 构建了一个案例树，一些定义的等式在某些情况下可能不成立，但让我们暂时忘记这一点） .
让我们考虑以下自然数加法的定义：
_+_ : ℕ → ℕ → ℕ
zero + b = b
(suc a) + b = suc (a + b)
此定义提供了两个定义等式，将 zero + b 与 b 和 (suc a) + b 与 suc (a + b) 绑定。定义等式（相对于命题等式）的好处是，只要有可能，Agda 就会自动使用它们来减少目标。这意味着，例如，如果在进一步的目标中你有任何 p 的元素 zero + p 那么 Agda 会自动将它减少到 p.
为了允许 Agda 进行这种归约，这在大多数情况下都是基本的，Agda 需要知道这两个等式中的哪一个可以被利用，这意味着必须对这个加法的第一个参数进行 case-split在任何进一步证明加减是可能的。 （除了基于使用此类案例拆分的其他证明的复合证明）。
当使用 with 时，您基本上会根据附加元素的结构添加附加定义等式。这才有意义，理解你需要在对这样的函数进行证明时对所述元素进行大小写拆分，以便 Agda 再次能够利用这些定义等式。
让我们以你的例子为例，并将这个推理应用于它，首先没有最近省略不可能的情况的能力。您需要证明以下陈述：
prop-old : ∀ x y → fun x y ≡ nothing → x < y
在context中引入参数，你这样写：
prop-old x y p = ?
写完该行后，您需要用上下文中的元素提供 x < y 的证明。 x 和 y 是很自然的，所以你期望 p 拥有足够的信息来证明这个结果。但是，在这种情况下，p 只是 fun x y ≡ nothing 类型，无法为您提供足够的信息。但是，此类型包含对函数 fun 的调用，所以还有希望！查看 fun 的定义，我们可以看到它产生两个定义等式，这取决于 x <? y 的结构。这意味着再次使用 with 将此参数添加到证明中将允许 Agda 使用这些等式。这导致以下代码：
prop-old : ∀ x y → fun x y ≡ nothing → x < y
prop-old x y p with x <? y
prop-old _ _ p | yes q = ?
prop-old _ _ p | no q = ?
那时，Agda 不仅在 x <? y 上进行了大小写拆分，而且还降低了目标，因为在这两种情况下，它都能够使用 fun 的特定定义等式.让我们仔细看看这两种情况：
在 yes q 的情况下，p 现在是 nothing ≡ nothing 类型，而 q 是 x < y 类型，这正是您要证明的，这意味着目标简单地解决了：
prop-old _ _ p | yes q = q
在 no q 案例中，发生了一些更有趣的事情，这有点难以理解。归约后，p 现在是 just y ≡ nothing 类型，因为 Agda 可以使用 fun 的第二个定义等式。由于 _≡_ 是一种数据类型，因此可以在 p 上进行大小写拆分，这基本上会询问 Agda：“看看这个数据类型，并为类型 [=49 的元素提供所有可能的构造函数=]”。起初，Agda 只找到一个可能的构造函数，refl，但是这个构造函数只构建一个等式两边都相同的类型的元素，根据定义，这里不是这种情况，因为 just和 nothing 是来自同一数据类型 Maybe 的两个不同的构造函数。 Agda 然后得出结论，没有可能的构造函数可以构建这种类型的元素，因此这种情况实际上是不可能的，这导致 Agda 将 p 替换为空模式 () 并驳回这种情况.因此，这一行很简单：
prop-old _ _ () | no _
在较新版本的 Agda 中，正如我之前解释的，其中一些步骤由 Agda 直接完成，这允许我们直接忽略不可能的情况，因为可以在幕后推断出模式的空虚，这导致更漂亮：
prop : ∀ x y → fun x y ≡ nothing → x < y
prop x y _ with x <? y
... | yes p = p
但它是相同的过程，只是更自动地完成了一点。希望这些元素对您理解 Agda 的过程有所帮助。
我写了一个关于自然数的函数，它使用带有抽象的运算符 _<?_。
open import Data.Maybe
open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary
fun : ℕ → ℕ → Maybe ℕ
fun x y with x <? y
... | yes _ = nothing
... | no _ = just y
我想证明如果用fun计算的结果是nothing那么原来的两个值（x和y）满足x < y.
到目前为止，我所有的尝试都未能证明 属性:
prop : ∀ (x y)
→ fun x y ≡ nothing
→ x < y
prop x y with fun x y
... | just _ = λ()
... | nothing = λ{refl → ?} -- from-yes (x <? y)}
-- This fails because the pattern matching is incomplete,
-- but it shouldn't. There are no other cases
prop' : ∀ (x y)
→ fun x y ≡ nothing
→ x < y
prop' x y with fun x y | x <? y
... | nothing | yes x<y = λ{refl → x<y}
... | just _ | no _ = λ()
--... | _ | _ = ?
总的来说，我发现使用 with-abstraction 很痛苦。这可能是因为 with 和 | 在后台隐藏了一些魔法。我想了解 with 和 | 的真正作用，但 "Technical details" 目前无法理解。您知道去哪里寻找以了解如何解释它们吗？
具体解决方案
您需要在函数中进行大小写拆分的同一元素上进行大小写拆分：
prop : ∀ x y → fun x y ≡ nothing → x < y
prop x y _ with x <? y
... | yes p = p
在旧版本的 Agda 中，您必须编写以下内容：
prop-old : ∀ x y → fun x y ≡ nothing → x < y
prop-old x y _ with x <? y
prop-old _ _ refl | yes p = p
prop-old _ _ () | no _
但是现在你可以完全忽略导致直接矛盾的情况，在这种情况下，nothing 和 just smth 永远不会相等。
详细说明
要了解 with 的工作原理，您首先需要了解 Agda 中如何使用定义相等来减少目标。定义相等性根据其输入的结构将函数调用与其关联的表达式绑定在一起。在 Agda 中，通过在函数的不同情况的定义中使用等号很容易看出这一点（尽管由于 Agda 构建了一个案例树，一些定义的等式在某些情况下可能不成立，但让我们暂时忘记这一点） .
让我们考虑以下自然数加法的定义：
_+_ : ℕ → ℕ → ℕ
zero + b = b
(suc a) + b = suc (a + b)
此定义提供了两个定义等式，将 zero + b 与 b 和 (suc a) + b 与 suc (a + b) 绑定。定义等式（相对于命题等式）的好处是，只要有可能，Agda 就会自动使用它们来减少目标。这意味着，例如，如果在进一步的目标中你有任何 p 的元素 zero + p 那么 Agda 会自动将它减少到 p.
为了允许 Agda 进行这种归约，这在大多数情况下都是基本的，Agda 需要知道这两个等式中的哪一个可以被利用，这意味着必须对这个加法的第一个参数进行 case-split在任何进一步证明加减是可能的。 （除了基于使用此类案例拆分的其他证明的复合证明）。
当使用 with 时，您基本上会根据附加元素的结构添加附加定义等式。这才有意义，理解你需要在对这样的函数进行证明时对所述元素进行大小写拆分，以便 Agda 再次能够利用这些定义等式。
让我们以你的例子为例，并将这个推理应用于它，首先没有最近省略不可能的情况的能力。您需要证明以下陈述：
prop-old : ∀ x y → fun x y ≡ nothing → x < y
在context中引入参数，你这样写：
prop-old x y p = ?
写完该行后，您需要用上下文中的元素提供 x < y 的证明。 x 和 y 是很自然的，所以你期望 p 拥有足够的信息来证明这个结果。但是，在这种情况下，p 只是 fun x y ≡ nothing 类型，无法为您提供足够的信息。但是，此类型包含对函数 fun 的调用，所以还有希望！查看 fun 的定义，我们可以看到它产生两个定义等式，这取决于 x <? y 的结构。这意味着再次使用 with 将此参数添加到证明中将允许 Agda 使用这些等式。这导致以下代码：
prop-old : ∀ x y → fun x y ≡ nothing → x < y
prop-old x y p with x <? y
prop-old _ _ p | yes q = ?
prop-old _ _ p | no q = ?
那时，Agda 不仅在 x <? y 上进行了大小写拆分，而且还降低了目标，因为在这两种情况下，它都能够使用 fun 的特定定义等式.让我们仔细看看这两种情况：
在 yes q 的情况下，p 现在是 nothing ≡ nothing 类型，而 q 是 x < y 类型，这正是您要证明的，这意味着目标简单地解决了：
prop-old _ _ p | yes q = q
在 no q 案例中，发生了一些更有趣的事情，这有点难以理解。归约后，p 现在是 just y ≡ nothing 类型，因为 Agda 可以使用 fun 的第二个定义等式。由于 _≡_ 是一种数据类型，因此可以在 p 上进行大小写拆分，这基本上会询问 Agda：“看看这个数据类型，并为类型 [=49 的元素提供所有可能的构造函数=]”。起初，Agda 只找到一个可能的构造函数，refl，但是这个构造函数只构建一个等式两边都相同的类型的元素，根据定义，这里不是这种情况，因为 just和 nothing 是来自同一数据类型 Maybe 的两个不同的构造函数。 Agda 然后得出结论，没有可能的构造函数可以构建这种类型的元素，因此这种情况实际上是不可能的，这导致 Agda 将 p 替换为空模式 () 并驳回这种情况.因此，这一行很简单：
prop-old _ _ () | no _
在较新版本的 Agda 中，正如我之前解释的，其中一些步骤由 Agda 直接完成，这允许我们直接忽略不可能的情况，因为可以在幕后推断出模式的空虚，这导致更漂亮：
prop : ∀ x y → fun x y ≡ nothing → x < y
prop x y _ with x <? y
... | yes p = p
但它是相同的过程，只是更自动地完成了一点。希望这些元素对您理解 Agda 的过程有所帮助。