pattern-matching - `with`子句中的上下文评估不足

Answer 1

嵌套with子句是可以的。问题在于，在 的定义中close-var，您不仅匹配 的结果，还匹配compare (toℕ y) (toℕ z)参数y及其z本身。当然，Agda 不能在不确定使用哪个函数方程的情况下减少一些东西。

在第二个洞中，close-var应该在 上进行模式匹配inject₁ z，但你不（也不能）。您还必须对其进行抽象，然后进行足够的模式匹配以使 Agda 相信它可以安全地选择一个方程。

close∘open≡id x y z | tri> _ _ _
  with inject₁ z | compare (toℕ y) (toℕ (inject₁ z))
... | tri> _ _ _ | Fin.zero  | tri< () _ _
... | tri> _ _ _ | Fin.suc r | tri< _  _ _ = {!!}  -- goal is r ≡ z

---

至于第一个洞 - 如果上面的代码没有帮助，只需证明一个简单的引理：

≡→≤ : {x y : ℕ} → x ≡ y → x ≤ y
≡→≤ refl = ≤-refl

然后，您可以通过以下方式得出矛盾：

y≮suc-z (s≤s (≡→≤ y≡z))

（我没有查看StrictTotalOrder记录，但很可能这个引理已经存在）。