Coq の Variable と Parameter の違い

Coq の Variable(s), Parameter(s), Hypothesis(es), Axiom, Conjecture の違いがいつもわからなくなるのでメモ。

まず Parameter = Parameters = Axiom = Conjecture で、Variable = Variables = Hypothesis = Hypotheses です。

この2つは Section を使わない場合や Section の中にいる場合は同じなのですが、Section の中で使ってその Section を閉じた場合に違いがでます。

(* Coq8.4pl5 *)

Section Sect.
  Parameter (A : Type).
  Variable (B : Type).

  Definition A' := A.
  Definition B' := B.

  Print A.  (* => *** [ A : Type ] *)
  Print B.  (* => *** [B : Type] *)

  Print A'. (* => A' = A : Type *)
  Print B'. (* => B' = B : Type *)
End Sect.

Print A.    (* => *** [ A : Type ] *)
Print A'.   (* => A' = A : Type *)
Print B'.   (* => B' = fun B : Type => B : Type -> Type
                  Argument scope is [type_scope] *)
Print B.    (* => Error: B not a defined object. *)

Section の中ではどちらも同じですが、Section を閉じたあとは、Variable で定義した B は消え、B' は Type -> Type の関数になっています。

また慣習として、ソートが Prop のときは Axiom, Hypothesis を、それ以外のときは Parameter, Variable を使うようです。

参照: https://coq.inria.fr/refman/Reference-Manual003.html#sec41