Ruby の Range#empty? は実装可能か?、という話で、 極小の判定が必要になるという話を書いた。 しかしそこで極大の判定は必要にならなかった。 このように非対称なのは、Range に exclude_end? はあるが exclude_begin? はない、という非対称性による。
もし exclude_begin? が入って、始点を含まない範囲を表現可能になると、極大の判定も必要になるだろう。 (実際 <URL:https://bugs.ruby-lang.org/issues/12133> で提案されたことがある)
なお、Raku (Perl6) にはそういう機能（と演算子）がある。 <URL:https://docs.raku.org/type/Range> から例を引用する。
1 .. 5; # 1 <= $x <= 5 1^.. 5; # 1 < $x <= 5 1 ..^5; # 1 <= $x < 5 1^..^5; # 1 < $x < 5
Ruby (や Perl) の x...y は x..^y に対応するわけだ。
一部界隈では、始点と終点の両方を含まない 1^..^5 みたいなのを neko operator と呼ぶようだが、さすがに公式ドキュメントにそうは書いていないようだ。
ここで Raku の記法を使わせてもらうと(そして Ruby の beginless, endless も使えるとして)、極大要素 max が存在すると、 要素を持たない range として max^.. を考えられる。 max^.. は max よりも大きな要素からなる範囲だが、max は極大なのでそれよりも大きな要素は存在せず、結局、空になる。
exclude_begin? と exclude_end? の両方があると、問題になるのは極大だけではない。 整数の範囲で考えると、1^..^2 は、 1 < x < 2 なので、要素を持たない。 ただ、Ruby ではオブジェクト全体が半順序をなしているという考えのもとでは、整数だけという制約をいれることはできない。 そして、標準で浮動小数点数や有理数があるので、1^..^2 は要素を持つ。1.5 とか。 有理数があると、x^..^y には (x < y であれば) (x+y)/2 が含まれているので、要素を持たないことはなさそうである。 (有理数の大小関係は稠密順序だが、整数はそうでないという話だなこれは。wikipedia:稠密関係)
では、なにかそういう、間に値がないようなものはないだろうかと考えて、 [] と [min] というのを考えついた。 空の配列と、なんらかの極小値ひとつを要素として持つ配列は、 辞書式順序で考えて、その間には値がないのではないだろうか。
たぶんそうだろう、と思ったのだが、Coq で確かめようと思った。
ただ、しばらく考えていると、そもそも半順序関係な値の配列を辞書式順序で比較すると、それは半順序になるのだろうか、という疑問も沸いてきた。 いや、半順序になっている気はするのだが、一抹の不安が。 そこから調べていこう。
例によって mathcomp を使う
From mathcomp Require Import all_ssreflect all_algebra. Open Scope order_scope. Section POrderArray.
今回は、前回同様、半順序関係のある型 value と、その value の列である seq value を使う。 seq value に pseq という別名をつけよう。
Variable value : porderType ring_display. Definition pseq := seq value.
value は半順序関係なので、等値関係も中に入っている。 なので、pseq の等値関係を簡単に作れる。
Definition pseq_eqType := seq_eqType value.
pseq に対する辞書式順序の比較を実装する。le と lt を定義する。 le は less than or equal であり、lt は less than である。 まぁ普通の実装だと思う。
Fixpoint le (a b : pseq) : bool := match a, b with | [::], [::] => true | [::], (y :: b') => true | (x :: a'), [::] => false | (x :: a'), (y :: b') => (x < y) || ((x == y) && le a' b') end. Definition lt (a b : pseq) : bool := (b != a) && le a b.
ここで、le のなかで列の要素 x, y の比較をしているが、半順序なので、比較不能な場合がある。 その場合は x < y と x == y が偽になって、le の結果が false になる。 これは比較不能なときだけでなく、x > y のときと結果が同じになる。 それでいいのだろうか、<=> なら -1, 0, 1, nil と4種類の結果をちゃんと区別するのに、とも思うが、 le a b && le b a && (a != b) とすれば、比較不能であることはわかるのでいけなくはないか。 効率は気にしない文脈だしな。
半順序は、le について反射律、反対称律、推移律が成り立てばいいので、それぞれ証明する。
(* forall x, le x x *)
Lemma le_refl : reflexive le.
Proof.
elim; first by [].
move=> v s IH /=.
rewrite Order.POrderTheory.ltxx /=.
by rewrite eq_refl.
Qed.
(* forall x y, le x y && le y x -> x = y *)
Lemma le_anti : antisymmetric le.
Proof.
elim; first by case.
move=> x1 xs IH [] /=; first by [].
move=> y1 ys.
move/andP => [].
move/orP => [].
move=> lt_x1_y1.
rewrite (Order.POrderTheory.lt_gtF lt_x1_y1) /=.
move/andP => [].
by rewrite (Order.POrderTheory.gt_eqF lt_x1_y1).
move/andP => [] /eqP <-.
move=> le_xs_ys.
move/orP => [].
by rewrite Order.POrderTheory.ltxx.
rewrite eq_refl /=.
move=> le_ys_xs.
rewrite (IH ys); first by [].
apply/andP.
by split.
Qed.
(* forall y x z, le x y -> le y z -> le x z *)
Lemma le_trans : transitive le.
Proof.
elim; first by case.
move=> y1 ys IH.
case; first by case.
move=> x1 xs.
case; first by [].
move=> z1 zs /=.
move/orP => [].
move=> lt_x1_y1.
move/orP => [].
move=> lt_y1_z1.
apply/orP; left.
by exact (Order.POrderTheory.lt_trans lt_x1_y1 lt_y1_z1).
move/andP => [].
move/eqP => <-.
by rewrite lt_x1_y1.
move/andP => [] /eqP => <- le_xs_ys.
move/orP => [].
by move=> ->.
move/andP => [] /eqP -> le_ys_zs.
rewrite Order.POrderTheory.ltxx eq_refl /=.
by apply IH.
Qed.
le について反射律、反対称律、推移律が成り立つと、mathcomp で pseq と le, lt (と反射律、反対称律、推移律)をまとめて、これが半順序関係のインスタンスである、とできる。
Definition pseq_porderType : lePOrderMixin pseq_eqType.
apply (@Order.LePOrderMixin.Build pseq_eqType le lt).
by [].
by exact le_refl.
by exact le_anti.
by exact le_trans.
Defined.
これで、配列の辞書式順序が半順序になっていることを確認できた。 というわけで不安は杞憂であった。
もうひとつ、[] と [min] の間に値がないことを確認しよう。
まず、補題をひとつ証明する。 空列以下だったらそれは空列という補題である。
Lemma le_s_emp s : (le s [::]) = (s == [::]). Proof. by case: s. Qed.
min という値があってそれが極小ならば、 [::] よりも大きく、かつ、[:: min] よりも小さい値は存在しないという証明を行う。
Lemma not_dense min :
~(exists x, x < min) ->
~(exists y, lt [::] y && lt y [:: min]).
Proof.
move=> Hmin.
case=> y.
move/andP => [].
rewrite /lt.
case: y; first by [].
move=> y1 ys /= _ /andP [] Hy /orP [].
move=> lt_y1_min.
apply Hmin.
by exists y1.
rewrite le_s_emp.
move/andP => [] /eqP eq_y1_min /eqP eq_ys_emp.
move: Hy.
by rewrite eq_y1_min eq_ys_emp eq_refl.
Qed.
証明できた、というわけで、やはり [] と [min] の間には値がない。
End POrderArray.
ということで、[] と [min] の間には値がないので、[]^..^[min] という範囲は空であり、 空かどうかを判定するには、ふたつの値の間に値が存在するかどうかを確認する仕掛けが必要になる。
2023-11-06 Parameter じゃなくて Variable を使うようにした
[latest]