[Coq] Coq Advent Calender : exists (11 of 25)

　Coq でよく使われる tactic の11番目は exists です。
　証明のゴールが exists x, P x とか { n:nat | isPrime n } とか、ある性質を満たす要素が存在することを求めている時に、「具体的に」その要素を与えてゴールを変形します。

　下記は exists を使う簡単な例です。mの具体的な値としてS n = n+1 を与えています。具体的なmを何か与えないとomegaでの自動証明は通りません。

Coq < Require Import Omega.

Coq < Lemma Sample_of_exists : forall n, exists m, n < m.
1 subgoal
  
  ============================
   forall n : nat, exists m : nat, n < m

Sample_of_exists < intros.
1 subgoal
  
  n : nat
  ============================
   exists m : nat, n < m

Sample_of_exists < exists (S n).
1 subgoal
  
  n : nat
  ============================
   n < S n

Sample_of_exists < omega.
Proof completed.

Sample_of_exists < Qed.
intros.
exists (S n).
omega.

Sample_of_exists is defined
Coq <