天泣記

2021-12-02 (Thu)

#1 coq issue

GitHub coq/coq/issues/15286: Unknown constructor name in a match-expression is accepted

これは勘違いだと教えてもらった

2021-12-03 (Fri)

#1 ProofIrrelevance はなんで矛盾にならないのか

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-28 (Tue)

#1 Coq の (とくに SSReflect での) Search

Coq には Search というコマンドがあって、定理などを検索できるという話なののだが、 使っても思うように見つからない経験があって、 結局、ライブラリのソース (ssrnat.v とか) を less で眺めるのが日常である

でも、なんとなく気が向いて、真面目に Search の使い方を調べてみた

たとえば addnA は (自然数 nat についての) x + (y + z) = (x + y) + z という定理なので、 よく Search の例としてあげられる使い方としては、(_ + (_ + _)) を探せば見つかると期待される

が、試してみると、出てこない

From mathcomp Require Import all_ssreflect.

Search (_ + (_ + _)).
(*
addnACl: forall m n p : nat, m + n + p = n + (p + m)
halfD: forall m n : nat, (m + n)./2 = odd m && odd n + (m./2 + n./2)
*)

Search ((_ + _) + _).
(*
ddnACl: forall m n p : nat, m + n + p = n + (p + m)
addnCAC: forall m n p : nat, m + n + p = p + n + m
leq_divDl: forall p m n : nat, (m + n) %/ p <= m %/ p + n %/ p + 1
sqrnD: forall m n : nat, (m + n) ^ 2 = m ^ 2 + n ^ 2 + 2 * (m * n)
...
*)

なんか、もっと複雑なものが出てくるが、addnA は出てこない

ちょっと考えると、たぶん、addnA の型が associative というのを使っているのが原因な気がする。

Check addnA.
(*
addnA
     : associative addn
*)

これが x + (y + z) = x + y + z であることは、[eta ...] というので括って Check してみるとわかる。

Check [eta addnA].
(*
[eta addnA]
     : forall x y z : nat, x + (y + z) = x + y + z
*)

というわけで、addnA の型には、表面的には (_ + (_ + _)) という項は含まれておらず、見つからない、ということなのだと思う (もちろん、associative を展開するなど計算を進めれば、(_ + (_ + _)) という形の部分項は出てくる)

正直、計算してくれとも思うが、 型の中に複雑な計算がある可能性を考えると、無条件に計算するのは難しいのだろう (なんか指定すると型を計算して Search 可能にしてくれるような機能があるといいんだけど)

ということで、現状の Coq で、どうやればうまく検索できるか、 マニュアルを眺めて、 いくつかやりかたがあることが判明した

以下のいずれでも addnA は見つけられる

まぁ、SSReflect をしばらく使っていれば、addnA は覚えちゃうと思うので、addnA はいいのだが、 より現実的な問題は分配規則とかである

たとえば、(x - y) * z = x * z - y * z という書き換え規則は mulnBl なのだが、 個人的にはこれの名前は覚えていないので、Search で見つけたい、が、 上記と同じく Search ((_ - _) * _). では見つからない

理由は addnA と同じで、型が left_distributive muln subn と定義されていて、表面的には ((_ - _) * _) という部分項は現れていないからである

Check mulnBl.
(*
mulnBl
     : left_distributive muln subn
*)

これをどうすれば検索できるかというと、Search "-" "*". とすればよい (Search subn muln. でもよい)

Search "-" "*".
(*
mulnBr: right_distributive muln subn
mulnBl: left_distributive muln subn
divnBMl: forall q m d : nat, (m - q * d) %/ d = m %/ d - q
...
*)

"-" と "*" の組み合わせを探したければ Search "-" "*". とすればよい、というのはたぶん覚えられると思うので、これでいいかな


[latest]


田中哲