参数和类成员之间的区别

Question

我是 Coq 的新手，想知道以下内容之间有什么区别：

Class test (f g: nat -> nat) := {
  init:   f 0 = 0 /\ g 0 = 0;
  output: ...another proposition about f and g...;
}.

和

Class test := {
  f: nat -> nat;
  g: nat -> nat;
  init:   f 0 = 0 /\ g 0 = 0;
  output: ...another proposition about f and g...;
}.

有人能提供解释吗？

Answer 1

它们之间的区别称为捆绑。

Class test (f g: nat -> nat) := {
  init:   f 0 = 0 /\ g 0 = 0;
  output: ...another proposition about f and g...;
}.

是分拆的，并且

Class test := {
  f: nat -> nat;
  g: nat -> nat;
  init:   f 0 = 0 /\ g 0 = 0;
  output: ...another proposition about f and g...;
}.

是捆绑的。

捆绑的优点是您不需要总是提供f和g。分拆的优点是您可以让同一类的不同实例共享相同的f和g。如果将它们捆绑在一起，Coq 将不会轻易相信不同的实例共享参数。

您可以在类型理论中的数学类型类中阅读更多相关内容。

Answer 2

为了补充 Ana\xe2\x80\x99s 的优秀答案，这里有一个实际的区别：

\n

\n
• 非捆绑版本（称为utest）允许您编写utest f g关于特定函数对f和的逻辑语句g，
\n
• 而捆绑版本（称为btest）允许您声明存在一对满足属性的函数；f您稍后可以通过投影名称和来引用这些函数g。
\n

\n

所以，粗略地说：

\n

\n
• btest是 \xe2\x80\x9ce 等价于 \xe2\x80\x9d 到\xe2\x88\x83 f g, utest f g;
\n
• utest f' g'是 \xe2\x80\x9ce 等价于 \xe2\x80\x9d 到btest \xe2\x88\xa7 \xe2\x80\x9cthe f (resp. g) in the aforementioned proof of btest is equal to f' (resp. g')\xe2\x80\x9d.
\n

\n

更正式地说，下面是一个最小示例的等价\n（在此代码中，符号{ x : A | B }是依赖对(x, y)类型，\n即wherex : A和 的类型y : B\n且类型B取决于值x）：

\n

(* unbundled: *)\nClass utest (x : nat) : Prop := {\n  uprop : x = 0;\n}.\n\n(* bundled: *)\nClass btest : Type := {\n  bx : nat;\n  bprop : bx = 0;\n}.\n\n(* [btest] is equivalent to: *)\n\nGoal { x : nat | utest x } -> btest.\nProof.\n  intros [x u]. econstructor. exact (@uprop x u).\nQed.\n\nGoal btest -> { x : nat | utest x }.\nProof.\n  intros b. exists (@bx b). constructor. exact (@bprop b).\nQed.\n\n(* [utest x] is equivalent to: *)\n\nGoal forall x, { b : btest | @bx b = x } -> utest x.\nProof.\n  intros x [b <-]. constructor. exact (@bprop b).\nQed.\n\nGoal forall x, utest x -> { b : btest | @bx b = x }.\nProof.\n  intros x u. exists {| bx := x ; bprop := @uprop x u |}. reflexivity.\nQed.\n\n(* NOTE: Here I\xe2\x80\x99ve explicited all implicit arguments; in fact, you\n   can let Coq infer them, and write just [bx], [bprop], [uprop]\n   instead of [@bx b], [@bprop b], [@uprop x u]. *)\n

\n

在这个例子中，我们还可以观察到计算相关性方面的差异：utest可以存在于 中Prop，因为它唯一的成员uprop是一个命题。另一方面，我不能真正放入btest，Prop因为这意味着和 都会存在，但在计算bx上是相关的。换句话说，Coq 会向您发出以下警告：bpropPropbf

\n

Class btest : Prop := {\n  bx : nat;\n  bprop : bx = 0;\n}.\n(* WARNING:\n     bx cannot be defined because it is informative and btest is not.\n     bprop cannot be defined because the projection bx was not defined.\n*)\n

\n