存在量化子

仮定の存在量化子を消去する

仮定 H が \( \exists x, P(x) \) であるときに, destruct H をすると, H の代わりに新しく \( x \) という仮定と, \( P(x) \) という仮定が追加される.

1 subgoal
  
  n : nat
  H : exists m : nat, n = m
  ============================
  ...

ex <   destruct H.
1 subgoal
  
  n, x : nat
  H : n = x
  ============================
  ...

仮定に x と新しい H が追加された.

Goal の存在量化子を消去する

Goal が \( \exists x, P(x) \) という形をしている場合, そして具体的に \(P(x)\) を満たす \(x\) の値が分かっている場合は, exists コマンドでその値を代入することが出来る.

1 subgoal
  
  n : nat
  ============================
  exists m : nat, m - 1 = n

ex <   exists (n + 1).
1 subgoal
  
  n : nat
  ============================
  n + 1 - 1 = n

m に (n+1) が代入された. 証明はこの代入された後の式について続いて行われるので注意.