天泣記

ProofIrrelevance というのは、同じ命題の証明を同一視する、という公理である

Require Import ProofIrrelevance.

About proof_irrelevance.
(*
proof_irrelevance : forall (P : Prop) (p1 p2 : P), p1 = p2

proof_irrelevance is not universe polymorphic
Arguments proof_irrelevance _%type_scope _ _
Expands to: Constant Coq.Logic.ProofIrrelevance.proof_irrelevance
*)

任意の命題 P について、P の証明 p1 と p2 はなんでも p1 = p2 となる、ということにする、というものである

証明がいくつもある命題、というのは、Prop に属する帰納型で、コンストラクタがふたつあるものを考えればよさそうである

ということは、bool の Prop 版でいいんじゃないかということで、定義してみよう

Inductive pbool : Prop := ptrue | pfalse.

問題なく定義できるので、これらの証明 ptrue と pfalse が等しいということを証明してみよう

Lemma ptrue_eq_pfalse : ptrue = pfalse.
apply proof_irrelevance.
Qed.

Print ptrue_eq_pfalse.
(*
ptrue_eq_pfalse = proof_irrelevance pbool ptrue pfalse
     : ptrue = pfalse
*)

これの証明は proof_irrelevance を呼び出しているだけである

さて、ptrue = pfalse が証明できたということは、もし ptrue <> pfalse も証明できちゃったとすると、矛盾となる (両方証明できちゃうと、False が証明可能になり、ひいてはすべての命題が証明可能になって、意味の無いシステムになってしまう)

true <> false は普通に証明できるので、ptrue <> pfalse も証明できてもおかしくないのではなかろうか

もちろん、きっとそれはうまく禁止されているのだろうが、どのように禁止されているのだろうか

まず、true <> false を証明してみる

Lemma true_neq_false : true <> false.
Proof.
  intros H.
  discriminate.
Defined.
Print true_neq_false.
(*
true_neq_false =
fun H : true = false =>
let H0 : False := eq_ind true (fun e : bool => if e then True else False) I false H
  in
False_ind False H0
     : true <> false
*)

証明項をみると、eq_ind とか False_ind を使っていて中身がよくわからないので展開してみよう

Eval cbv beta zeta delta [true_neq_false eq_ind False_ind] in true_neq_false.
(*
     = fun H : true = false =>
       match
         match H in (_ = y) return (if y then True else False) with
         | eq_refl => I
         end return False
       with
       end
     : true <> false
*)

なんか、外側の match は無駄な気がするので、それは外したものを自分で定義してみよう

Definition true_neq_false' : true <> false :=
  fun H : true = false =>
  match H in (_ = y) return (if y then True else False) with
  | eq_refl => I
  end.

この定義はとくに問題なく可能なので、やはり外側の match は無駄だった

で、これを真似して ptrue <> pfalse の証明に挑戦してみる

Fail Definition ptrue_neq_pfalse : ptrue <> pfalse :=
  fun H : ptrue = pfalse =>
  match H in (_ = y) return (if y then True else False) with
  | eq_refl => I
  end.
(*
The command has indeed failed with message:
Incorrect elimination of "y" in the inductive type "pbool":
the return type has sort "Type" while it should be "SProp" or "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.
*)

ふむ、やはり失敗するのだが、エラーメッセージをみると、 if y then True else False の部分が原因のようだ

この if 式 (match 式) の返値のソートは (つまり返値の型の型は) SProp か Prop でなければならないのに、 Type になっている、というのが理由である

if y then True else False の返値は True ないし False で、 True や False の型は Prop であり、 Prop の型は Type なので、たしかにそれはそうである

if 式は match 式なので、match 式同様 return 節もあり、自明な場合には表示が省略されてしまうのだが、省略しないようにして true_neq_false' を調べてみよう

Unset Printing Synth.
Print true_neq_false'.
(*
true_neq_false' =
fun H : true = false =>
match H in (_ = y) return (if y return Set then True else False) with
| eq_refl => I
end
     : true <> false
*)

ふむ、if y return Set then True else False と、返値の型は Set になっている

えー、Prop じゃないの、と思ったが、Prop と Set はサブタイプ関係で、Set のほうが大きいから嘘ではない、か

Prop にしても問題ないか試してみよう

Definition true_neq_false'' : true <> false :=
  fun H : true = false =>
  match H in (_ = y) return (if y return Prop then True else False) with
  | eq_refl => I
  end.

とくに問題ないようだ

あ、true_neq_false だとどうなってるかな

Print true_neq_false.
(*
true_neq_false =
fun H : true = false =>
let H0 : False :=
  eq_ind true (fun e : bool => if e return Prop then True else False) I false H in
False_ind False H0
     : true <> false
*)

こっちは return Prop になってる

ptrue <> pfalse で、明示的に return Prop と書いてもとくに結果は変わらない

Fail Definition ptrue_neq_pfalse : ptrue <> pfalse :=
  fun H : ptrue = pfalse =>
  match H in (_ = y) return (if y return Prop then True else False) with
  | eq_refl => I
  end.
(*
The command has indeed failed with message:
Incorrect elimination of "y" in the inductive type "pbool":
the return type has sort "Type" while it should be "SProp" or "Prop".
Elimination of an inductive object of sort Prop
is not allowed on a predicate in sort Type
because proofs can be eliminated only to build proofs.
*)

CIC だとどうなってたっけ、と調べてみる

Coq reference manual, The match ... with ... end construction

あぁ、match 可能なソートを定義していて、Prop が match 可能という [I:Prop|I->s] の前提には s が SProp か Prop と書いてあるな

で、理由は、Prop の部分は extraction で消えちゃうからプログラムに残る分岐に使うことはできない、というのと、 proof-irrelevance と矛盾するから、とちゃんと書いてあった

天泣記

2021-12-02 (Thu)

2021-12-03 (Fri)

2021-12-28 (Tue)