Help us understand the problem. What is going on with this article?

Coq の Variable と Parameter の違い

More than 3 years have passed since last update.

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

Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
Comments
No comments
Sign up for free and join this conversation.
If you already have a Qiita account
Why do not you register as a user and use Qiita more conveniently?
You need to log in to use this function. Qiita can be used more conveniently after logging in.
You seem to be reading articles frequently this month. Qiita can be used more conveniently after logging in.
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
ユーザーは見つかりませんでした