agda - 在 Agda 中将构造函数编写为函数的更好方法

Question

我有一个 list

data List (X : Set) : Set where
  <>   : List X
  _,_  : X -> List X -> List X

平等的定义

data _==_ {l}{X : Set l}(x : X) : X -> Set l where
  refl : x == x

和一致性

cong : forall {k l}{X : Set k}{Y : Set l}(f : X -> Y){x y} -> x == y -> f x == f y
cong f refl = refl

我试图证明

propFlatten2 : {X : Set } ( xs0 : List X ) (x : X)  (xs1 : List X) (xs2 : List X)
              -> ( xs0 ++ x , xs1 ) ++ xs2  ==  xs0 ++ (x , xs1 ++ xs2 )
propFlatten2 <> x xs1 xs2 = refl
propFlatten2 (x , xs0) x₁ xs1 xs2 =   cong (λ l -> x , l) {!!}

有没有更好的方法直接使用构造函数 _,_除了通过最后一行中的 lambda 之外？

Answer 1

Agda 对于运算符的部分应用没有任何特殊的语法。但是，您可以在通常的前缀版本中使用运算符:

x + y = _+_ x y

当您需要部分应用最左边的参数时，这很方便:

_+_ 1 = λ x → 1 + x

当您需要部分应用来自右侧的参数时，您的选择就更加有限。如评论中所述，您可以使用其中一种便利功能，例如 flip (在 Function 中找到):

flip f x y = f y x  -- Type omitted for brevity.

然后简单地 flip _+_ 的参数:

flip _+_ 1 = λ x → x + 1

有时您会发现运算符的唯一目的是使代码更好一些。我能想到的最好的例子可能是 Data.Product.,_ .当您编写依赖对 ( Data.Product.Σ ) 时，有时可以自动填充该对的第一部分。而不是写:

_ , x

你可以只写:

, x

很难说写一个像上面这样的专门操作符是否真的值得；如果您唯一的用例是一致地使用它，我会坚持使用 lambda，因为它非常清楚发生了什么。