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 *)SectionSect.Parameter(A:Type).Variable(B:Type).DefinitionA':=A.DefinitionB':=B.PrintA.(* => *** [ A : Type ] *)PrintB.(* => *** [B : Type] *)PrintA'.(* => A' = A : Type *)PrintB'.(* => B' = B : Type *)EndSect.PrintA.(* => *** [ A : Type ] *)PrintA'.(* => A' = A : Type *)PrintB'.(* => B' = fun B : Type => B : Type -> Type
 Argument scope is [type_scope] *)PrintB.(* => 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