忽略 Agda 中的点模式会出现什么问题？

Question

我是 agda 的菜鸟，正在阅读 http://www.cse.chalmers.se/~ulfn/papers/afp08/tutorial.pdf。我的浅薄知识以某种方式发现点阵图案不是很有必要。例如，

data Image_∋_ {A B : Set}(f : A → B) : B → Set where
  im : (x : A) → Image f ∋ f x


inv : {A B : Set}(f : A → B)(y : B) → Image f ∋ y → A
inv f .(f x) (im x) = x

我发现inv可以定义为

inv : {A B : Set}(f : A → B)(y : B) → Image f ∋ y → A
inv _ _ (im x) = x

因为从类型上，我们已经知道y对于某些x来说是f的图像，所以它不可能出错。

另一个例子是

data _==_ {A : Set}(x : A) : A → Set where
  refl : x == x

data _≠_ : ℕ → ℕ → Set where
  z≠s : {n : ℕ} → zero ≠ suc n
  s≠z : {n : ℕ} → suc n ≠ zero
  s≠s : {n m : ℕ} → n ≠ m → suc n ≠ suc m


data Equal? (n m : ℕ) : Set where
  eq : n == m → Equal? n m
  neq : n ≠ m → Equal? n m


equal? : (n m : ℕ) → Equal? n m
equal? zero zero    = eq refl
equal? zero (suc _) = neq z≠s
equal? (suc _) zero = neq s≠z
equal? (suc n') (suc m') with equal? n' m'
... | eq refl   = eq refl
... | neq n'≠m' = neq (s≠s n'≠m')

考虑equal?函数，论文倒数第二行写成(suc n') (suc .n') | eq refl = eq refl。同样，with 构造中的 eq refl 已经提供了证明，因为这两个值是相同的，所以我为什么要费心用点模式写出来？

我比较熟悉coq，不知道coq有类似的东西。我在这里遗漏了什么吗？

Answer 1

在 Coq 中，您可以明确地编写模式匹配，而 Agda 基于方程的方法会强制类型检查器重建一个应该与您编写的内容相对应的案例树。

点模式帮助类型检查器看到给定的模式不是匹配的产物，而是强制由对其他参数之一的匹配（例如：匹配在 Vec Bool n 上将强制 n 的值，或者如您所观察到的，在等式证明上的匹配将强制某些变量相同。

它们并不总是必需的，事实上，正如您在 the CHANGELOG for version 2.5.3:

中看到的那样，有些已经慢慢成为可选的

Dot patterns.

The dot in front of an inaccessible pattern can now be skipped if the pattern consists entirely of constructors or literals. For example:

忽略 Agda 中的点模式会出现什么问题？

What could go wrong by ignoring dot pattern in Agda?

agda