Schedule/ProofCafe_24

述語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.