agda - 忽略 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 是 f 对于某些 x 的图像，所以它不可能出错.

另一个例子是

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。同样，eq refl in with construct 已经提供了一个证明，因为这两个值是相同的，那么我为什么要费心用点模式写出来呢？

我比较熟悉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: