[Coq] Coq Advent Calender : reflexivity (25 of 25)

　Coq でよく使われる tactic の紹介も今回で最後。最終回は reflexivity を紹介します。

　reflexivity はゴールが等式で、左辺と右辺の値が等しい時に使います。内容的には apply refl_equal. と同じです。refl_equal はこんな公理。

Inductive eq (A : Type) (x : A) : A -> Prop :=  refl_equal : x = x

　左辺と右辺が全く同じ形をしていないと等式は成り立ちません（が、reflexivity は内部的に simpl を実行しているので simpl で簡単化して等しくなる物は成立します）。

　ところで、同じ形というのはどこまで同じならば = が成り立つかというのは良く解らないので色々試してみました。

Coq < Definition f : nat -> nat := fun x => x.
Coq < Definition h : nat -> nat := fun y => y .
Coq < Goal f = h.
1 subgoal
  
  ============================
   f = h

Unnamed_thm < simpl.
1 subgoal
  
  ============================
   f = h

Unnamed_thm < unfold f.
1 subgoal
  
  ============================
   (fun x : nat => x) = h

Unnamed_thm < unfold h.
1 subgoal
  
  ============================
   (fun x : nat => x) = (fun y : nat => y)

Unnamed_thm < reflexivity.
Proof completed.

Unnamed_thm < Qed.

　これを見ると、(fun x : nat => x) = (fun y : nat => y) は成立するようです。同様に、

Coq < Goal forall P:nat->Prop, (forall n, P n) = (forall m, P m).
Unnamed_thm0 < intros P.
Unnamed_thm0 < reflexivity.
Proof completed.

　これを見ると、(forall n : nat, P n) = (forall m : nat, P m) も成立。

　上記の f, h の場合はreflexivityで等しい事が示せましたが、一般には関数が等しい事を reflexivity で証明する事は出来ません。　
　f, g : nat -> nat について、f = g ⇔ ∀n:nat, f n = g n. を以て等しいとする場合は、こんな感じで証明します。

Coq < Definition f : nat -> nat := fun x => x.

Coq < Fixpoint g(x:nat):nat :=
Coq < match x with
Coq < | O => O
Coq < | S n' => S (g n')
Coq < end.

Coq < Require Import Logic.FunctionalExtensionality.

Coq < Lemma Sample_of_reflexivity : f = g.
1 subgoal
  
  ============================
   f = g

Sample_of_reflexivity < extensionality n.
1 subgoal
  
  n : nat
  ============================
   f n = g n

Sample_of_reflexivity < unfold f.
1 subgoal
  
  n : nat
  ============================
   n = g n

Sample_of_reflexivity < induction n.
2 subgoals
  
  ============================
   0 = g 0

subgoal 2 is:
 S n = g (S n)

Sample_of_reflexivity < reflexivity.
1 subgoal
  
  n : nat
  IHn : n = g n
  ============================
   S n = g (S n)

Sample_of_reflexivity < simpl.
1 subgoal
  
  n : nat
  IHn : n = g n
  ============================
   S n = S (g n)

Sample_of_reflexivity < rewrite <- IHn.
1 subgoal
  
  n : nat
  IHn : n = g n
  ============================
   S n = S n

Sample_of_reflexivity < reflexivity.
Proof completed.

Sample_of_reflexivity < Qed.

　他にも、= を同値関係を以て定義する場合は Setoid というものを使って考える（Coqの型理論には集合論の商集合が無いので、代わりに = を同値関係で置き換えた物を使う）とか有るらしいのですが、そっちはちょっと調べきれませんでした。

ーーーーー

★後書き★

　Coq Advent Calender を始めるにあたっては、Coq Partyでのmaeda_さんの発表に有った「tactic使用例が有ると嬉しい」と「coqでの人気tactic」という話題からネタを頂きました。
　25個もあると自分では使った事の無いtacticとかもあって結構使い方を調べたり、あるいは適当な証明課題を探したりなど、それなりに大変で、何度か挫けそうになりましたがなんとか最後まで書けて良かったです。
　Coq を学ぶ人の参考になると良いなぁ。