- 10/27
- 時間: 14:30 - 17:30
- 場所: 名古屋大学 理学部A館 428
- 参加登録: [PARTAKE: 第24回 ProofCafe](http://partake.in/events/8043bda9-a1dc-466e-aa33-3ab6bc5eac5a)
- [ソフトウェアの基礎](http://proofcafe.org/sf/)の[命題と論拠](http://proofcafe.org/sf/Prop_J.html)の「???」から
- ドキュメントはCoqソースコードから自動生成されています。ソースコード全体はこちら: [http://proofcafe.org/sf/sfja.tar.gz]()

## 述語evが各自然数に対してsingletonになることの証明
~~~ { .v }
(* dependent induction, dependent destructionを使うために必要な
   Program.Equalityをimport. *)
Require Import Program.Equality.

(* Program.Equalityによってproof_irrelevanceが仮定されるので、
   evをimpredicative universeで定義してしまうと
   (すなわちnat -> Propにしてしまうと)、下のev_singletonは自明になってしまう。
   そのため、predicative universeでevを定義する *)
Inductive ev : nat -> Set :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).

Theorem ev_singletons : forall (n : nat) (p q : ev n), p = q.
Proof.
  intros.
  dependent induction p.
  dependent induction q.
  reflexivity.
  dependent destruction q.
  rewrite (IHp q).
  reflexivity.
Qed.
~~~