Gallina の構文と Vernacular コマンド

字句

空白文字、改行、タブは空白とみなされる。

コメントは (* で始まり *) で終わる。コメントの中に他のコメントあるいは文字列を入れることができる。コメントは空白とみなされる。

識別子には、英字 (A, B, …)、下線 (_) その他 Unicode で識別子として利用可能とされている文字が使える。識別子の二文字目以降には数字およびプライム (') も使える。

キーワード

特殊な意味を持つため識別子として使えないキーワードは以下の通り:

項

全称量化子
forall n, 0 <= n
forall n : nat, 0 <= n
forall i j k : nat, i <= j <= k
forall (m n : nat) (b : bool), m <= n /\ b = true
関数の型
nat -> bool
関数の型は特殊な全称量化子である: forall _ : nat, bool
関数リテラル
fun n => n + n
fun n : nat => n + n
fun i j k : nat => i + j + k
fun (m n : nat) (b : bool) => (m - n, negb b)
不動点 (再帰関数)
fix func n := match n with O => O | S n' => func n' end
不動点 (相互再帰関数)
fix even n :=
  match n with
  | 0 => true
  | S n' => negb (odd n')
  end
with odd n :=
  match n with
  | 0 => true
  | S n' => negb (even n')
  end
for even
マッチング
match 1 + 2 with O => true | S n => false end
match le_n 0 as H in _ <= n return 0 < S n with … end
If then else
if eq_nat_dec 1 2 then 3 else 4
If then else はマッチングの一種である: match eq_nat_dec 1 2 with left _ => 3 | right _ => 4 end
変数束縛
let z := 0 in z + z
let double z := 2 * z in double 3
変数束縛 (再帰関数)
let fix func n := match n with O => O | S n' => func n' end in func 3
この構文では相互再帰関数は書けない
変数束縛 (値の分解)
let (a, b, c) := (1, 2, 3) in a + b + c
変数束縛による値の分解はマッチングの一種である: match 1, 2, 3 with a, b, c => a + b + c end
変数束縛 (複雑な値の分解)
let '((a, b), (c, d)) := ((1, 2), (3, 4)) in a + b + c + d
式の解釈のスコープの指定
(nat * nat)%type
関数適用
plus 2 3
関数適用 (暗黙引数の明示)
ex (A := nat) (fun n => n = 0)
@ ex nat (fun n => n = 0)

Vernacular コマンド

宣言

グローバルな宣言
Parameter P : Prop.
Parameters i j k : nat.
Axiom all_le_O_n : forall n : nat, 0 <= n.
Conjecture all_le_O_n : forall n : nat, 0 <= n.
スコープを現在のセクション内に限定した宣言
Variable n : nat.
Variables s t u : Set.
Hypothesis H : n = 0.
Hypotheses (H1 : n <= 3) (H2 : forall b : bool, b = true \/ b = false).

宣言を行うキーワードは八つある。これらは言葉のニュアンスと宣言のスコープが違うだけで、他の点に違いはない。

定義

グローバルな定義
Definition zero := 0.
Definition zero : nat := 0.
Definition negate : bool -> bool := fun b => if b then false else true.
Definition negate (b : bool) : bool := if b then false else true.
Definition negate b := if b then false else true.
Example zero := 0.
スコープを現在のセクション内に限定した定義
Let zero := 0.

定義を行うキーワードは三つある。これらは言葉のニュアンスと宣言のスコープが違うだけで、他の点に違いはない。

帰納的な定義
Inductive nat : Set := O : nat | S : nat -> nat.
Inductive nat : Set := O | S (_ : nat).
Inductive list (A : Set) : Set := nil : list A | cons : A -> list A -> list A.
Inductive even : nat -> Prop :=
  | even_O  : even O
  | even_SS : forall n : nat, even n -> even (S (S n)).
Inductive tree : Set :=
  | node : nat -> forest -> tree
with forest : Set :=
  | leaf : nat -> forest
  | cons : tree -> forest -> forest.
不動点による定義
Fixpoint add m n := match m with O => n | S m' => S (add m' n) end.
Fixpoint add (m n : nat) {struct m} : nat := match m with O => n | S m' => S (add m' n) end.
Fixpoint tree_size (t : tree) :=
  match t with node a f => S (forest_size f) end
with forest_size (f : forest) :=
  match f with
  | leaf b => 1
  | cons t f' => (tree_size t + forest_size f')
  end.

不動点による定義では、{struct x} で再帰に伴い小さくなる引数を指定することができる。

余帰納的な定義
CoInductive stream : Set := seq : nat -> stream -> stream.
余不動点による定義
CoFixpoint from n := seq n (from (S n)).
レコードの定義
Record rational : Set := mkRat { n : nat; d : nat }.
Record nonzero := { n : nat; H : n <> 0 }.

レコードの定義では Record の代わりに Structure も使える。また Inductive/CoInductive を使うと(余)帰納的なレコードを定義できる。

レコードのフィールド名はレコードからそのフィールドを取り出す関数として使える: n (mkRat 1 2) = 1

証明

証明の開始
Theorem all_le_O_n : forall n : nat, 0 <= n.
Theorem even_odd_S : forall n, even n -> odd (S n) with odd_even_S : forall n, odd n -> even (S n). (証明に相互帰納法を使う場合)
Goal forall n : nat, 0 <= n. (定理名を指定しない場合)
証明
Proof … Qed.
Proof … Save.
証明による定義
Proof … Defined.
証明の中止 (証明ができたとみなす)
Proof … Admitted.

Theorem の代わりに Lemma, Remark, Fact, Corollary, Proposition, Definition も使える (ニュアンスが違うだけで意味は同じ)。

セクション

セクションの開始
Section Foo.
セクションの終了
End Foo.

情報の表示

© 2010 Magicant / 更新 2010-06-21 / 初出 2010-06-20