Schedule/ProofCafe_24

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

述語evが各自然数に対してsingletonになることの証明

(* 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.