pattern-matching - `with` 句内のコンテキストの評価が不十分です

Answer 1

ネストされたwith句は問題ありません。問題は、 の定義では、 の結果だけでなく、引数とそれ自体もclose-var一致することです。そしてもちろん、Agda は、どの関数方程式を使用するかを確認せずに何かを減らすことはできません。compare (toℕ y) (toℕ z)yz

2 番目の穴では、close-varでパターン マッチする必要inject₁ zがありますが、そうではありません (できません)。それも抽象化してから、1 つの方程式を安全に選択できることを 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が、この補題が既に存在する可能性があります)。