以前から気になっていたというか腑に落ちていなかったこととして、 グレゴリオ歴の年月日からユリウス通日への変換がある。
Wikipedia:ユリウス通日によれば、 1月と2月は前年の13月と14月として、 y年m月d日午前0時の修正ユリウス日は以下で表される、とある
mjd = floor(365.25*y) + floor(y/400) - floor(y/100) + floor(30.59 * (m-2)) + d - 678912
(ユリウス日は正午が整数となってわかりにくいので、深夜0時が整数となる修正ユリウス日を扱うことにする。)
ここで、この式がなにをやっているのかだいたいはわかるのだが、30.59 の 0.59 ってどこから出てきたのだ?
365.25 の 0.25 は 4年に一回の閏年に関連しているのだろう。 y/400 と y/100 も、閏年の規則の 100年に一回と 400年に一回と対応しているのだろう。 678912 はなんらかのオフセットだろうから気にならない。
でも、0.59 はどうして 0.59 なのか?
これど関連して、(結論からいえば非常に強く関連しているのだが) 月の日数は一定じゃないのにこんな式でちゃんと求まるのか?
という疑問が長年あったのだが、思い立って Rocq で確認してみた。
結論からいうと、0.59 というのがうまく月の日数が一定でないのを扱っている。
Rocq でこれを扱うとして、まずちょっと問題になるのが、 大きな整数を扱う必要があることである。 Rocq の nat はペアノの自然数の素朴な実装なので、自然数 n を表現するのに n に比例したメモリを使う。 コンストラクタ O にコンストラクタ S を n 回適用した項を使うので。 まぁ、現実的な話としては数千くらいになるのは避けたい。
ということで、まず 678912 は無視することにする。 これは起点をしめしているだけで、私の疑問とは関係ない。 (あと、-678912 とすると負数を扱わなければならないので nat では表現できなくて困るというのもある)
本当は、年は自然数じゃなくて整数にしたほうがいいのだが、 MathComp で大きい整数をコンパクトに (2進で) 扱う方法はみあたらなかったので nat でやることにする。
ただ、少し大きな値は 2進で表現した項を使う。 Rocq には BinNums というライブラリがあって、そういう表現も可能であり、 ssrnat には、それで表現した数を記述するための %num という記法が用意されている。
が、それが動かない。 いろいろ調べたところ、以下のように最初に書いて動かした。 (そしてバグレポートしした。)
(* workaround for %num. https://github.com/math-comp/math-comp/issues/1512 *) From Stdlib Require Import BinNatDef. Delimit Scope N_scope with num. From mathcomp Require Import all_ssreflect.
まず、閏年かどうかを判定する関数を定義する。 ここで d %| m は、m が d で割りきれることを示す (bool を返す) 述語である。 グレゴリオ歴における閏年の定義そのものであるが、 今回は 1月2月のかわりに 13月14月を扱い、 13月14月は翌年の 1月2月なので、最初に年を補正する必要がある。 MathComp には、bool -> nat の coercion が定義されていて、false が 0, true が 1 になるので、この補正は y + (12 < m) と書ける。
Definition is_leap_year y m := let y' := y + (12 < m) in (4 %| y') && ~~(100%num %| y') || (400%num %| y').
月の長さを求める関数を定義する。 まぁ、グレゴリオ歴のままのふつうである。
Definition monlen (y m : nat) : nat := match m with | 13 => 31 | 14 => if is_leap_year y m then 29 else 28 | 3 => 31 | 4 => 30 | 5 => 31 | 6 => 30 | 7 => 31 | 8 => 31 | 9 => 30 | 10 => 31 | 11 => 30 | 12 => 31 | _ => 0 end.
正しい年月日かどうかを判定する述語を定義する。 (nat つまり 0以上の整数を表現する型を使っているので、正しくない値も表現できてしまうため)
Definition valid_ymd (ymd : nat * nat * nat) : bool := let: (y, m, d) := ymd in (3 <= m <= 14) && (1 <= d <= monlen y m).
Wikipedia日本語版にあった mjd を求める式を (最後の 678912 を除いて) 関数として定義する。
Definition jd_of_ymd (ymd : nat * nat * nat) : nat := let: (y, m, d) := ymd in 365%num * y + (y %/ 4 + y %/ 400%num - y %/ 100%num) + 30 * (m - 2) + (59 * (m - 2) %/ 100%num) + d.
年月日から、翌日の年月日を求める関数を定義する。 日をインクリメントしてオーバーフローしたら月をインクリメントしてそれもオーバーフローしたら年をインクリメントする。 これは素朴に正しいと思う。
Definition succ_ymd_y (y m d : nat) : nat := if d < monlen y m then y else if m < 14 then y else y.+1. Definition succ_ymd_m (y m d : nat) : nat := if d < monlen y m then m else if m < 14 then m.+1 else 3. Definition succ_ymd_d (y m d : nat) : nat := if d < monlen y m then d.+1 else 1. Definition succ_ymd (ymd : nat * nat * nat) := let: (y, m, d) := ymd in (succ_ymd_y y m d, succ_ymd_m y m d, succ_ymd_d y m d).
とりあえず、月の長さは 28日以上、というのを証明する。 月 m を 14回場合分けして証明している。 こうやって場合分けすると、0月から13月までは自明に証明できて、 15月以降も自明に証明できる。 14月 (つまり 2月) は閏年かどうかの場合分けが必要で、場合分けすれば証明できる。
Lemma monlen28 (y m : nat) : 3 <= m <= 14 -> 28 <= monlen y m. Proof. do 14 (case: m => [|m]; first by []). case: m => [|m]; last by []. rewrite /monlen. by case: ifP. Qed.
valid な年月日の翌日の年月日は valid であることを証明する。
Lemma succ_ymd_mrange y m d :
valid_ymd (y, m, d) ->
3 <= succ_ymd_m y m d <= 14.
Proof.
rewrite /valid_ymd => /andP [Hm Hd].
rewrite /succ_ymd_m.
case: ifPn => [|Hd2]; first by [].
case: ifPn => [Hm2|]; last by [].
apply/andP.
split; last by [].
case/andP: Hm.
by move/ltnW.
Qed.
Lemma succ_ymd_drange y m d :
valid_ymd (y, m, d) ->
1 <= succ_ymd_d y m d <= monlen (succ_ymd_y y m d) (succ_ymd_m y m d).
Proof.
rewrite /valid_ymd => /andP [Hm Hd].
rewrite /succ_ymd_y /succ_ymd_m /succ_ymd_d.
case: ifPn => [|Hd2]; first by [].
case: ifPn => Hm2.
apply/andP; split; first by [].
apply (@leq_trans 28); first by [].
apply monlen28.
apply/andP.
split; last by [].
apply ltnW.
by case/andP: Hm.
apply/andP; split; first by [].
apply (@leq_trans 28); first by [].
by apply monlen28.
Qed.
Lemma valid_succ_ymd ymd : valid_ymd ymd -> valid_ymd (succ_ymd ymd).
Proof.
case: ymd => [[y m] d] H.
rewrite /succ_ymd /valid_ymd /=.
apply/andP; split.
by apply succ_ymd_mrange.
by apply succ_ymd_drange.
Qed.
グレゴリオ歴は400年周期であることを証明する。 400年の中には97回閏年があって、400*365+97=146097日が周期である。
Lemma cycle400 y m d n :
jd_of_ymd (y + 400%num * n, m, d)
= jd_of_ymd (y, m, d) + (400%num * 365%num + 97) * n.
Proof.
rewrite /jd_of_ymd.
rewrite [365%num * (y + 400%num * n)]mulnDr.
rewrite [LHS]addn.[ACl 3*4*5*6*2*1].
rewrite [RHS]addn.[ACl 2*3*4*5*6*1].
congr (_ + 365%num * y).
rewrite (_ : (400%num * 365%num + 97) * n = 97 * n + 365%num * (400%num * n)); last first.
by rewrite mulnDl addnC [400%num * 365%num]mulnC mulnA.
rewrite addnA.
congr (_ + 365%num * (400%num * n)).
rewrite [RHS]addn.[ACl 1*5*2*3*4].
congr (_ + 30 * (m - 2) + (59 * (m - 2)) %/ 100%num + d).
rewrite [in (y + 400%num * n) %/ 4](_ : 400%num * n = n * 100%num * 4); last first.
by rewrite -[RHS]mulnA mulnC.
rewrite divnDMl; last by [].
rewrite [in (y + 400%num * n) %/ 400%num]mulnC.
rewrite divnDMl; last by [].
rewrite [in (y + 400%num * n) %/ 100%num](_ : 400%num * n = n * 4 * 100%num); last first.
by rewrite -mulnA mulnC.
rewrite divnDMl; last by [].
rewrite [y %/ 4 + n * 100%num + (y %/ 400%num + n)]addnACA.
rewrite -mulnSr.
rewrite subnDAC.
rewrite -addnBA; last first.
by rewrite leq_mul2l orbT.
rewrite (_ : n * 100%num.+1 - n * 4 = 97 * n); last first.
by rewrite -mulnBr mulnC.
rewrite addnBAC; first by [].
apply (@leq_trans (y %/ 4)); last by apply leq_addr.
rewrite -[y %/ 4](@divnMr 25); last by [].
apply leq_div2r.
by apply leq_pmulr.
Qed.
ここが個人的に腑に落ちなかった部分の確認である。0.59 * (m - 2) に月の日数を加えると 0.59 * (m.+1 - 2) になるのである。 ここでも 14回場合分けして証明している。 この場合分け (と内部的な計算) による証明は、正しいという確信は得られるが、 なぜ正しいのかという理由は正直わからない。 でも、(わかりたければ) ここに集中して考えればいいということはわかった。 (たぶんグラフを描くともうちょっとわかる気がするのだが...)
Lemma add_monlen y m :
3 <= m < 14 ->
(59 * (m - 2)) %/ 100%num + monlen y m
= (59 * (m.+1 - 2)) %/ 100%num + 30.
Proof.
do 14 (case: m => [|m]; first by []).
by [].
Qed.
補題を定義する。 この補題が MathComp にあってもおかしくない気がするのだが、ないということはなんかうまい証明のやりかたがあるのだろうか。
Lemma dvdn_mull (d1 d2 m : nat) : d1 * d2 %| m -> d1 %| m. Proof. move/dvdnP => [] k. rewrite mulnA => H. apply/dvdnP. exists (k * d2). rewrite H. by rewrite mulnAC. Qed. Lemma dvdn_mulr (d1 d2 m : nat) : d1 * d2 %| m -> d2 %| m. Proof. rewrite mulnC. by apply dvdn_mull. Qed.
ここで、年月日から翌日の年月日を求めてユリウス日を求めるのと、もともとの年月日からユリウス日を求めて 1 を足すのは等しい、ということを証明する。 けっこう長い証明になった。
難しかったのは、閏年であるという前提 (4 %| y.+1) && ~~ (100%num %| y.+1) || (400%num %| y.+1) があるときに (4 %| y.+1) && ~~ (100%num %| y.+1) の場合と (400%num %| y.+1) の場合に場合分けするとうまくいかないというところがあった。 前者の場合に y.+1 が 400で割りきれるかどうかの情報がないので、証明が進まない。 これはまず (4 %| y.+1) && ~~ (100%num %| y.+1) && ~~ (400%num %| y.+1) || (400%num %| y.+1) に変形して、 (4 %| y.+1) && ~~ (100%num %| y.+1) && ~~ (400%num %| y.+1) と (400%num %| y.+1) に場合分けしないといけないのだった。
Lemma jd_of_ymd_succ y m d :
valid_ymd (y, m, d) ->
jd_of_ymd (succ_ymd (y, m, d)) = (jd_of_ymd (y, m, d)).+1.
Proof.
rewrite /valid_ymd => /andP [Hm Hd].
rewrite /succ_ymd /succ_ymd_y /succ_ymd_m /succ_ymd_d.
case: ifPn => Hd2.
rewrite [in LHS]/jd_of_ymd.
by rewrite addnS.
case: ifPn => Hm2.
have {Hd Hd2}Hdmax : d = monlen y m.
rewrite -leqNgt in Hd2.
move: Hd => /andP [Hd3 Hd4].
apply/eqP.
rewrite eqn_leq.
by rewrite Hd2 Hd4.
have {}Hm : 2 < m.
by case/andP: Hm.
rewrite /jd_of_ymd.
rewrite [LHS]addn1.
congr _.+1.
rewrite -[LHS]addnA.
rewrite [RHS]addn.[ACl 1*2*(3*(4*5))].
congr (365%num * y + (y %/ 4 + y %/ 400%num - y %/ 100%num) + _).
rewrite [in RHS]Hdmax.
rewrite (add_monlen y m); last by rewrite Hm2 Hm.
rewrite [(59 * (m.+1 - 2)) %/ 100%num + 30]addnC.
rewrite [RHS]addnA.
congr (_ + (59 * (m.+1 - 2)) %/ 100%num).
rewrite subSn; last first.
by apply ltnW.
by rewrite mulnSr.
have {Hd Hd2}Hdmax : d = monlen y m.
rewrite -leqNgt in Hd2.
move: Hd => /andP [Hd3 Hd4].
apply/eqP.
rewrite eqn_leq.
by rewrite Hd2 Hd4.
have {Hm Hm2}Hmmax : m = 14.
rewrite -leqNgt in Hm2.
move: Hm => /andP [Hm3 Hm4].
apply/eqP.
rewrite eqn_leq.
by rewrite Hm4 Hm2.
rewrite {}Hdmax {}Hmmax.
rewrite /jd_of_ymd.
rewrite addn1.
congr _.+1.
change (30 * (3 - 2)) with 30.
change ((59 * (3 - 2)) %/ 100%num) with 0.
change (30 * (14 - 2)) with (nat_of_bin 360%num).
change ((59 * (14 - 2)) %/ 100%num) with 7.
rewrite addn0.
rewrite -[_ + 360%num + 7]addnA.
change (360%num + 7) with (nat_of_bin 367%num).
rewrite mulnS.
rewrite [LHS]addn.[ACl 3*4*1*2].
rewrite [RHS]addn.[ACl 2*3*4*1].
congr (_ + 365%num * y).
rewrite -[_ + 30 + 365%num]addnA.
change (30 + 365%num) with (28 + 367%num).
rewrite addnA [RHS]addnAC.
congr (_ + 367%num).
rewrite /monlen.
case: ifPn => Hleap.
suff: (y.+1 %/ 4 + y.+1 %/ 400%num - y.+1 %/ 100%num) =
(y %/ 4 + y %/ 400%num - y %/ 100%num) + 1.
move=> ->.
by rewrite -addnA.
rewrite addnBAC; last first.
apply (@leq_trans (y %/ 4)); last by apply leq_addr.
by apply leq_div2l.
rewrite [y.+1 %/ 100%num]divnS; last by [].
rewrite subnDA.
congr (_ - y %/ 100%num).
rewrite divnS; last by [].
rewrite divnS; last by [].
move: Hleap.
rewrite /is_leap_year.
change (y + (12 < 14)) with (y + 1).
rewrite addn1.
rewrite (_ : (4 %| y.+1) && ~~ (100%num %| y.+1) || (400%num %| y.+1)
= (4 %| y.+1) && ~~ (100%num %| y.+1) && ~~ (400%num %| y.+1) || (400%num %| y.+1)); last first.
by case: (4 %| y.+1); case: (100%num %| y.+1); case: (400%num %| y.+1).
case/orP.
move=> /andP [] /andP [] H4 H100 H400.
rewrite H4 (negbTE H100) (negbTE H400) /=.
rewrite add0n subn0.
by rewrite addn.[ACl 2*3*1].
move=> H400.
have H4: 4 %| y.+1.
by apply (dvdn_mulr 100%num).
have H100: 100 %| y.+1.
by apply (dvdn_mulr 4).
rewrite H4 H100 H400 /=.
by rewrite 2!add1n addn1 addnS.
congr (_ + 28).
rewrite divnS; last by [].
rewrite divnS; last by [].
rewrite divnS; last by [].
move: Hleap.
rewrite /is_leap_year.
change (y + (12 < 14)) with (y + 1).
rewrite addn1.
rewrite negb_or negb_and negbK.
move/andP => [] H H400.
rewrite (negbTE H400) add0n {H400}.
move: H.
rewrite (_ : (~~ (4 %| y.+1) || (100%num %| y.+1)) =
((~~ (4 %| y.+1) && ~~(100%num %| y.+1)) || (100%num %| y.+1))); last first.
by case: (4 %| y.+1); case: (100%num %| y.+1).
case/orP.
case/andP=> H4 H100.
by rewrite (negbTE H4) (negbTE H100) 2!add0n.
move=> H100.
have H4: 4 %| y.+1.
by apply (dvdn_mulr 25).
rewrite H4 H100.
by rewrite add1n addSn add1n subSS.
Qed.
最後に、年月日の n日後を、翌日を求める関数を n回適用して求め、そこからユリウス日を求めるのと、もともとの年月日からユリウス日を求めて n を足すのは等しい、ということを証明する。 これは帰納法を使う。 上の 1日後の定理があるので難しくない。 (でも求まった年月日が valid であるという部分を追加して命題を強化しないといけないという話はあった)
Lemma jd_of_ymd_add y m d n :
valid_ymd (y, m, d) ->
jd_of_ymd (iter n succ_ymd (y, m, d)) = (jd_of_ymd (y, m, d)) + n.
Proof.
move=> Hymd.
suff: valid_ymd (iter n succ_ymd (y, m, d)) /\
jd_of_ymd (iter n succ_ymd (y, m, d)) = jd_of_ymd (y, m, d) + n.
by case.
elim: n y m d Hymd.
move=> y m d Hymd.
by rewrite addn0.
move=> n IH y m d Hymd.
rewrite addnS.
specialize (IH y m d Hymd).
move: IH.
rewrite iterS.
case: (iter n succ_ymd (y, m, d)) => -[] y2 m2 d2 [Hymd2 Hjd].
split.
by apply valid_succ_ymd.
rewrite -Hjd.
by apply jd_of_ymd_succ.
Qed.
ともあれ、グレゴリオ歴の年月日からユリウス日を求める式のが正しいという確信は得られた。
GitHub coq/coq/issues/21452: Termination check passed in Rocq 9.0.0 but not in Rocq 9.1.0
Rocq (旧 Coq) では、ふつうのプログラミング言語に比べると、たくさん名前を作る必要がある。 ふつうのプログラミング言語なら関数をひとつ定義すると関数の名前がひとつ必要になるが、 Rocq だと、関数を定義すると、関数自体に加えてその関数のさまざまな性質を定理として証明して、その性質それぞれに名前をつけることになるからである。
SSReflect には、名前の規則 (慣習) がある。 名前の付け方は mathcomp book の 2.5.2 Search by name にちょっと書いてある。 定理の命題が (fee .. (fie ..(foe ..) ..) ..) なら fee_fie_foe という名前をつける。 例として、seq.v の size_cat があげられていて、これは以下の定理である。
Lemma size_cat s1 s2 : size (s1 ++ s2) = size s1 + size s2.
ここで、演算子 ++ は cat 関数なので、等式の左辺は size (cat s1 s2) であり、ここから size_cat という名前になっていることがわかる。
また、SSReflect では名前の 1文字の suffix をいろいろ使う。 たとえば交換律は C で表すことになっていて、自然数の加算は addn 関数なので、addn の交換律は、addnC である。
suffix のリストは Rocq 本体の ssrfun.v と ssrbool.v についているドキュメントがいちばん一般的なものだと思う。 (SSReflect は部分的に Rocq 本体に添付されていて、ssrfun.v と ssrbool.v は添付されているものである。 なお、他のファイルでもそれぞれのファイルの目的に応じていろいろな suffix は追加される。)
| LR - a lemma moving an operation from the left hand side of a relation to | the right hand side, like canLR: cancel g f -> x = g y -> f x = y. | RL - a lemma moving an operation from the right to the left, e.g., canRL. | Beware that the LR and RL orientations refer to an "apply" (back chaining) | usage; when using the same lemmas with "have" or "move" (forward chaining) | the directions will be reversed!.
| A -- associativity, as in andbA : associative andb.
| AC -- right commutativity.
| ACA -- self-interchange (inner commutativity), e.g.,
| orbACA : (a || b) || (c || d) = (a || c) || (b || d).
| b -- a boolean argument, as in andbb : idempotent_op andb.
| C -- commutativity, as in andbC : commutative andb,
| or predicate complement, as in predC.
| CA -- left commutativity.
| D -- predicate difference, as in predD.
| E -- elimination, as in negbFE : ~~ b = false -> b.
| F or f -- boolean false, as in andbF : b && false = false.
| I -- left/right injectivity, as in addbI : right_injective addb,
| or predicate intersection, as in predI.
| l -- a left-hand operation, as andb_orl : left_distributive andb orb.
| N or n -- boolean negation, as in andbN : a && (~~ a) = false.
| P -- a characteristic property, often a reflection lemma, as in
| andP : reflect (a /\ b) (a && b).
| r -- a right-hand operation, as orb_andr : right_distributive orb andb.
| T or t -- boolean truth, as in andbT: right_id true andb.
| U -- predicate union, as in predU.
| W -- weakening, as in in1W : (forall x, P) -> {in D, forall x, P}.
ここで、ssrfun の LR, RL および、ssrbool の l と r は左右の意味がある。
と、ここまでが背景なのだが、この左右の実際にどのような意味なのか気になったので調べてみた。
ssrfun には、LR と RL は apply したときに動く方向を示しているという説明がある。 例としてあげられている canLR: cancel g f -> x = g y -> f x = y は、 ゴールに f x = y があったときに apply canLR でゴールが x = g y に変わるので、左辺の f が右辺の g に変わる、ということで LR という説明である。 have や move で前提を変形する場合には、逆方向になるので、右辺の g が左辺の f になる、という注意がある。
左右を示す suffix を使っている定理は ssrfun.v には canLR と canRL しかないようだ。
canLR : forall [rT aT : Type] [f : aT -> rT] [g : rT -> aT] [x : rT] [y : aT], cancel f g -> x = f y -> g x = y canRL : forall [rT aT : Type] [f : aT -> rT] [g : rT -> aT] [x : aT] [y : rT], cancel f g -> f x = y -> x = g y
ただ、ssreflect.v に iffLR, iffRL, iffLRn, iffRLn があった。
iffLR : forall [P Q : Prop], P <-> Q -> P -> Q iffRL : forall [P Q : Prop], P <-> Q -> Q -> P iffLRn : forall [P Q : Prop], P <-> Q -> ~ P -> ~ Q iffRLn : forall [P Q : Prop], P <-> Q -> ~ Q -> ~ P
iffLR をみると、命題の等価性 P <-> Q の証明から、P -> Q という「左ならば右」というのを取り出すものになっている。 とすると、apply すると Q が P に変わるということなので、ssrfun の apply すると左が右に変わるというのとは逆っぽい。
ssrbool で定理の名前に左右が出てくるものを抜き出してみる。 (面倒くさくなったので、ドキュメントからの抜粋とする。実際に使うときにはセクション変数が引数に追加されて増えているかもしれない。)
Lemma negbLR b c : b = ~~ c -> ~~ b = c.
Lemma negbRL b c : ~~ b = c -> b = ~~ c.
Lemma contraL (c b : bool) : (c -> ~~ b) -> b -> ~~ c.
Lemma contraR (c b : bool) : (~~ c -> b) -> ~~ b -> c.
Lemma contraLR (c b : bool) : (~~ c -> ~~ b) -> b -> c.
Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2.
Lemma eqbRL (b1 b2 : bool) : b1 = b2 -> b2 -> b1.
Lemma unlessL C P : implies C (\unless C, P).
Lemma unlessR C P : implies P (\unless C, P).
Lemma andb_orl : left_distributive andb orb.
Lemma andb_orr : right_distributive andb orb.
Lemma orb_andl : left_distributive orb andb.
Lemma orb_andr : right_distributive orb andb.
Lemma andb_idl (a b : bool) : (b -> a) -> a && b = b.
Lemma andb_idr (a b : bool) : (a -> b) -> a && b = a.
Lemma andb_id2l (a b c : bool) : (a -> b = c) -> a && b = a && c.
Lemma andb_id2r (a b c : bool) : (b -> a = c) -> a && b = c && b.
Lemma orb_idl (a b : bool) : (a -> b) -> a || b = b.
Lemma orb_idr (a b : bool) : (b -> a) -> a || b = a.
Lemma orb_id2l (a b c : bool) : (~~ a -> b = c) -> a || b = a || c.
Lemma orb_id2r (a b c : bool) : (~~ b -> a = c) -> a || b = c || b.
Lemma implyb_idl (a b : bool) : (~~ a -> b) -> (a ==> b) = b.
Lemma implyb_idr (a b : bool) : (b -> ~~ a) -> (a ==> b) = ~~ a.
Lemma implyb_id2l (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c).
Lemma andb_addl : left_distributive andb addb.
Lemma andb_addr : right_distributive andb addb.
Lemma subrelUl T (r1 r2 : rel T) : subrel r1 (relU r1 r2).
Lemma subrelUr T (r1 r2 : rel T) : subrel r2 (relU r1 r2).
Lemma sym_left_transitive : left_transitive.
Lemma sym_right_transitive : right_transitive.
Lemma on1lW : allQ1l f h -> {on D2, allQ1l f & h}.
Lemma on1lT : {on T2, allQ1l f & h} -> allQ1l f h.
Lemma subon1l (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) : prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.
Lemma canLR_in x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y.
Lemma canRL_in x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y.
Lemma canLR_on x y : {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y.
Lemma canRL_on x y : {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y.
Lemma in_on1lP : {in D1, {on D2, allQ1l f & h}} <-> {in [pred x in D1 | f x \in D2], allQ1l f h}.
Lemma on1lW_in : {in D1, allQ1l f h} -> {in D1, {on D2, allQ1l f & h}}.
Lemma in_on1lW : allQ1l f h -> {in D1, {on D2, allQ1l f & h}}.
Lemma on1lS : (forall x, f x \in D2) -> {on D2, allQ1l f & h} -> allQ1l f h.
Lemma on1lS_in : {homo f : x / x \in D1 >-> x \in D2} -> {in D1, {on D2, allQ1l f & h}} -> {in D1, allQ1l f h}.
Lemma in_on1lS : (forall x, f x \in D2) -> {in T1, {on D2, allQ1l f & h}} -> allQ1l f h.
Lemma homoRL : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR (g x) y -> rR x (f y).
Lemma homoLR : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR x (g y) -> rR (f x) y.
Lemma monoLR : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR (f x) y = aR x (g y).
Lemma monoRL : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR x (f y) = aR (g x) y.
Lemma homoRL_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, aR (g x) y -> rR x (f y)}.
Lemma homoLR_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, aR x (g y) -> rR (f x) y}.
Lemma monoLR_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, rR (f x) y = aR x (g y)}.
Lemma monoRL_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, rR x (f y) = aR (g x) y}.
使ったことのない記法が使われていてよくわからないものもあるが、左右の使い方について分類してみると以下のような感じかな (ここでは組み合わせの規則から想定されるものは名前に左右が入っていなくても入れてある: contra)
apply すると左から右に動く、あるいは右から左に動く
Lemma negbLR b c : b = ~~ c -> ~~ b = c.
Lemma negbRL b c : ~~ b = c -> b = ~~ c.
Lemma canLR_in x y : {in D1, cancel f g} -> y \in D1 -> x = f y -> g x = y.
Lemma canRL_in x y : {in D1, cancel f g} -> x \in D1 -> f x = y -> x = g y.
Lemma canLR_on x y : {on D2, cancel f & g} -> f y \in D2 -> x = f y -> g x = y.
Lemma canRL_on x y : {on D2, cancel f & g} -> f x \in D2 -> f x = y -> x = g y.
Lemma homoRL : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR (g x) y -> rR x (f y).
Lemma homoLR : {homo f : x y / aR x y >-> rR x y} -> forall x y, aR x (g y) -> rR (f x) y.
Lemma homoRL_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, aR (g x) y -> rR x (f y)}.
Lemma homoLR_in : {in aD &, {homo f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, aR x (g y) -> rR (f x) y}.
rewrite すると、左から右に動く、あるいは右から左に動く
Lemma monoLR : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR (f x) y = aR x (g y).
Lemma monoRL : {mono f : x y / aR x y >-> rR x y} -> forall x y, rR x (f y) = aR (g x) y.
Lemma monoLR_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in aD & rD, forall x y, rR (f x) y = aR x (g y)}.
Lemma monoRL_in : {in aD &, {mono f : x y / aR x y >-> rR x y}} -> {in rD & aD, forall x y, rR x (f y) = aR (g x) y}.
等価性から「左ならば右」を得る、あるいは「右ならば左」を得る
Lemma eqbLR (b1 b2 : bool) : b1 = b2 -> b1 -> b2.
Lemma eqbRL (b1 b2 : bool) : b1 = b2 -> b2 -> b1.
対称的な 2引数関数の左右 (第1引数か第2引数) のどちらかを指定
Lemma unlessL C P : implies C (\unless C, P).
Lemma unlessR C P : implies P (\unless C, P).
Lemma subrelUl T (r1 r2 : rel T) : subrel r1 (relU r1 r2).
Lemma subrelUr T (r1 r2 : rel T) : subrel r2 (relU r1 r2).
名前の付いた命題の左右を継承
Lemma andb_orl : left_distributive andb orb.
Lemma andb_orr : right_distributive andb orb.
Lemma orb_andl : left_distributive orb andb.
Lemma orb_andr : right_distributive orb andb.
Lemma andb_addl : left_distributive andb addb.
Lemma andb_addr : right_distributive andb addb.
Lemma sym_left_transitive : left_transitive.
Lemma sym_right_transitive : right_transitive.
後半の _ -> _ のどこに ~~ がついていないか
Lemma contra (c b : bool) : (c -> b) -> ~~ b -> ~~ c.
Lemma contraL (c b : bool) : (c -> ~~ b) -> b -> ~~ c.
Lemma contraR (c b : bool) : (~~ c -> b) -> ~~ b -> c.
Lemma contraLR (c b : bool) : (~~ c -> ~~ b) -> b -> c.
rewrite したときに二項演算子が消えて引数がひとつ残る場合に、左右どちらが消えるか
Lemma andb_idl (a b : bool) : (b -> a) -> a && b = b.
Lemma andb_idr (a b : bool) : (a -> b) -> a && b = a.
Lemma orb_idl (a b : bool) : (a -> b) -> a || b = b.
Lemma orb_idr (a b : bool) : (b -> a) -> a || b = a.
Lemma implyb_idl (a b : bool) : (~~ a -> b) -> (a ==> b) = b.
Lemma implyb_idr (a b : bool) : (b -> ~~ a) -> (a ==> b) = ~~ a.
rewrite したときに二項演算子の引数の片方が変わるときに、左右どちらが変化しないか
Lemma andb_id2l (a b c : bool) : (a -> b = c) -> a && b = a && c.
Lemma andb_id2r (a b c : bool) : (b -> a = c) -> a && b = c && b.
Lemma orb_id2l (a b c : bool) : (~~ a -> b = c) -> a || b = a || c.
Lemma orb_id2r (a b c : bool) : (~~ b -> a = c) -> a || b = c || b.
Lemma implyb_id2l (a b c : bool) : (a -> b = c) -> (a ==> b) = (a ==> c).
使ったことのない記法が入っていて、ちょっとよくわからない
Lemma on1lW : allQ1l f h -> {on D2, allQ1l f & h}.
Lemma on1lT : {on T2, allQ1l f & h} -> allQ1l f h.
Lemma subon1l (Phf : ph (allQ1l f)) (Ph : ph (allQ1l f h)) : prop_on1 d2' Phf Ph -> prop_on1 d2 Phf Ph.
Lemma in_on1lP : {in D1, {on D2, allQ1l f & h}} <-> {in [pred x in D1 | f x \in D2], allQ1l f h}.
Lemma on1lW_in : {in D1, allQ1l f h} -> {in D1, {on D2, allQ1l f & h}}.
Lemma in_on1lW : allQ1l f h -> {in D1, {on D2, allQ1l f & h}}.
Lemma on1lS : (forall x, f x \in D2) -> {on D2, allQ1l f & h} -> allQ1l f h.
Lemma on1lS_in : {homo f : x / x \in D1 >-> x \in D2} -> {in D1, {on D2, allQ1l f & h}} -> {in D1, allQ1l f h}.
Lemma in_on1lS : (forall x, f x \in D2) -> {in T1, {on D2, allQ1l f & h}} -> allQ1l f h.
ふむ、idl と id2l が一貫していないように感じられる。
Lemma andb_idl (a b : bool) : (b -> a) -> a && b = b. Lemma andb_idr (a b : bool) : (a -> b) -> a && b = a. Lemma andb_id2l (a b c : bool) : (a -> b = c) -> a && b = a && c. Lemma andb_id2r (a b c : bool) : (b -> a = c) -> a && b = c && b.
idl, idr は && の左右の引数で (rewrite したときに) 消えるほうを示しているのに、 id2l, id2r は左右の変化しないほうを示している。
うぅむ、id2l は前提の a -> b = c のところをみると、b と c は同じ立場なのに対して、a が別な感じがするから、その別なのが左にあるということだろうか?
eqtype も調べてみよう。 (ここからは Rocq 添付じゃなくて、mathcomp に入っている。)
Lemma predU1l : x = y -> (x == y) || b. Lemma predU1r : b -> (x == y) || b.
eqtype にはこのふたつしか見当たらない。 apply すると or (を示す U) の左右どちらか指定したほうになるというところか。
ssrnat も調べてみよう。
ACl の l が左を意味しているのかどうかはよくわからない
Lemma addnAC : right_commutative addn. (* x + y + z = x + z + y *)
Lemma addnACl m n p: m + n + p = n + (p + m).
eqn/leq/ltn という比較演算子の左右の引数両方に add/sub/mul/exp があって、それらの左右どちらかが共通、つまり (eqn の場合で) add p _ == add p _ なら左、add _ p == add _ p なら右。
Lemma eqn_add2l p m n : (p + m == p + n) = (m == n).
Lemma eqn_add2r p m n : (m + p == n + p) = (m == n).
Lemma leq_add2l p m n : (p + m <= p + n) = (m <= n).
Lemma ltn_add2l p m n : (p + m < p + n) = (m < n).
Lemma leq_add2r p m n : (m + p <= n + p) = (m <= n).
Lemma ltn_add2r p m n : (m + p < n + p) = (m < n).
Lemma leq_sub2r p m n : m <= n -> m - p <= n - p.
Lemma leq_sub2l p m n : m <= n -> p - n <= p - m.
Lemma ltn_sub2r p m n : p < n -> m < n -> m - p < n - p.
Lemma ltn_sub2l p m n : m < p -> m < n -> p - n < p - m.
Lemma leq_sub2rE p m n : p <= n -> (m - p <= n - p) = (m <= n).
Lemma leq_sub2lE m n p : n <= m -> (m - p <= m - n) = (n <= p).
Lemma ltn_sub2rE p m n : p <= m -> (m - p < n - p) = (m < n).
Lemma ltn_sub2lE m n p : p <= m -> (m - p < m - n) = (n < p).
Lemma eqn_sub2rE p m n : p <= m -> p <= n -> (m - p == n - p) = (m == n).
Lemma eqn_sub2lE m n p : p <= m -> n <= m -> (m - p == m - n) = (p == n).
Lemma leq_mul2l m n1 n2 : (m * n1 <= m * n2) = (m == 0) || (n1 <= n2).
Lemma leq_mul2r m n1 n2 : (n1 * m <= n2 * m) = (m == 0) || (n1 <= n2).
Lemma eqn_mul2l m n1 n2 : (m * n1 == m * n2) = (m == 0) || (n1 == n2).
Lemma eqn_mul2r m n1 n2 : (n1 * m == n2 * m) = (m == 0) || (n1 == n2).
Lemma leq_pmul2l m n1 n2 : 0 < m -> (m * n1 <= m * n2) = (n1 <= n2).
Lemma leq_pmul2r m n1 n2 : 0 < m -> (n1 * m <= n2 * m) = (n1 <= n2).
Lemma eqn_pmul2l m n1 n2 : 0 < m -> (m * n1 == m * n2) = (n1 == n2).
Lemma eqn_pmul2r m n1 n2 : 0 < m -> (n1 * m == n2 * m) = (n1 == n2).
Lemma ltn_mul2l m n1 n2 : (m * n1 < m * n2) = (0 < m) && (n1 < n2).
Lemma ltn_mul2r m n1 n2 : (n1 * m < n2 * m) = (0 < m) && (n1 < n2).
Lemma ltn_pmul2l m n1 n2 : 0 < m -> (m * n1 < m * n2) = (n1 < n2).
Lemma ltn_pmul2r m n1 n2 : 0 < m -> (n1 * m < n2 * m) = (n1 < n2).
Lemma leq_exp2l m n1 n2 : 1 < m -> (m ^ n1 <= m ^ n2) = (n1 <= n2).
Lemma ltn_exp2l m n1 n2 : 1 < m -> (m ^ n1 < m ^ n2) = (n1 < n2).
Lemma eqn_exp2l m n1 n2 : 1 < m -> (m ^ n1 == m ^ n2) = (n1 == n2).
Lemma leq_pexp2l m n1 n2 : 0 < m -> n1 <= n2 -> m ^ n1 <= m ^ n2.
Lemma ltn_pexp2l m n1 n2 : 0 < m -> m ^ n1 < m ^ n2 -> n1 < n2.
Lemma ltn_exp2r m n e : e > 0 -> (m ^ e < n ^ e) = (m < n).
Lemma leq_exp2r m n e : e > 0 -> (m ^ e <= n ^ e) = (m <= n).
Lemma eqn_exp2r m n e : e > 0 -> (m ^ e == n ^ e) = (m == n).
名前に 2 は入っていないが、subn の両方の引数が addn で、addn の左右どちらかの引数が共通
Lemma subnDl p m n : (p + m) - (p + n) = m - n.
Lemma subnDr p m n : (m + p) - (n + p) = m - n.
rewrite すると左にある predn が消える
Lemma ltn_predL n : (n.-1 < n) = (0 < n).
rewrite すると右にある predn が左に移って succn に変わる
Lemma ltn_predRL m n : (m < n.-1) = (m.+1 < n).
左右どちらかから足される
Lemma leq_addl m n : n <= m + n.
Lemma leq_addr m n : n <= n + m.
Lemma ltn_addl m n p : m < n -> m < p + n.
Lemma ltn_addr m n p : m < n -> m < n + p.
rewrite すると 左の subn が右に移って addn に変わる
Lemma leq_subLR m n p : (m - n <= p) = (m <= n + p).
subn と右引数が付加される (n に対して n - m は subn と右引数 m が付加されている)
Lemma leq_subr m n : n - m <= n.
subn と右 (r) 引数が付加されたものが ltn/leq の右 (R) 引数にある
Lemma ltn_subrR m n : (n < n - m) = false.
Lemma leq_subrR m n : (n <= n - m) = (m == 0) || (n == 0).
subn と右 (r) 引数が付加されたものが ltn の左 (L) 引数にある
Lemma ltn_subrL m n : (n - m < n) = (0 < m) && (0 < n).
addn の左右どちらかの引数に subn (B) がある
Lemma addnBr_leq n p m : n <= p -> m + (n - p) = m.
Lemma addnBl_leq m n p : m <= n -> m - n + p = p.
subn の左右どちらかの引数に subn (B) がある
Lemma subnBr_leq n p m : n <= p -> m - (n - p) = m.
Lemma subnBl_leq m n p : m <= n -> (m - n) - p = 0.
ltn/leq の左右どちらかに subn があり、rewrite すると反対に移って addn に変わる
Lemma ltn_subRL m n p : (n < p - m) = (m + n < p).
Lemma leq_psubRL m n p : 0 < n -> (n <= p - m) = (m + n <= p).
Lemma ltn_psubLR m n p : 0 < p -> (m - n < p) = (m < n + p).
Lemma leq_subRL m n p : m <= p -> (n <= p - m) = (m + n <= p).
Lemma ltn_subLR m n p : n <= m -> (m - n < p) = (m < n + p).
leq/ltn の左右どちらかに subn があり、rewrite すると、subn の右引数と leq/ltn の反対側の引数が交換される (交換だから C なのか?)
Lemma leq_subCl m n p : (m - n <= p) = (m - p <= n).
Lemma ltn_subCr m n p : (p < m - n) = (n < m - p).
Lemma leq_psubCr m n p : 0 < p -> 0 < n -> (p <= m - n) = (n <= m - p).
Lemma ltn_psubCl m n p : 0 < p -> 0 < n -> (m - n < p) = (m - p < n).
Lemma leq_subCr m n p : n <= m -> p <= m -> (p <= m - n) = (n <= m - p).
Lemma ltn_subCl m n p : n <= m -> p <= m -> (m - n < p) = (m - p < n).
maxn/minn が左右どちらかの引数をそのまま返す
Lemma maxn_idPl {m n} : reflect (maxn m n = m) (m >= n).
Lemma maxn_idPr {m n} : reflect (maxn m n = n) (m <= n).
Lemma minn_idPl {m n} : reflect (minn m n = m) (m <= n).
Lemma minn_idPr {m n} : reflect (minn m n = n) (m >= n).
左右どちらかから maxn/minn が適用される (leq_addl などと一貫性がないような気がする)
Lemma leq_maxl m n : m <= maxn m n.
Lemma leq_maxr m n : n <= maxn m n.
Lemma geq_minl m n : minn m n <= m.
Lemma geq_minr m n : minn m n <= n.
名前の付いた命題の左右を継承
Lemma addn_maxl : left_distributive addn maxn.
Lemma addn_maxr : right_distributive addn maxn.
Lemma subn_maxl : left_distributive subn maxn.
Lemma addn_minr : right_distributive addn minn.
Lemma addn_minl : left_distributive addn minn.
Lemma subn_minl : left_distributive subn minn.
Lemma maxn_minl : left_distributive maxn minn.
Lemma maxn_minr : right_distributive maxn minn.
Lemma minn_maxl : left_distributive minn maxn.
Lemma minn_maxr : right_distributive minn maxn.
Lemma mulnDl : left_distributive muln addn.
Lemma mulnDr : right_distributive muln addn.
Lemma mulnBl : left_distributive muln subn.
Lemma mulnBr : right_distributive muln subn.
iterSr は右側にひとつ取り出す (iterS は左側にひとつ取り出す)
Lemma iterSr n f x : iter n.+1 f x = iter n f (f x).
Lemma iterS n f x : iter n.+1 f x = f (iter n f x).
mulSnr は右側にひとつ取り出す (mulSn は左側にひとつ取り出す)
Lemma mulSn m n : m.+1 * n = n + m * n.
Lemma mulSnr m n : m.+1 * n = m * n + n.
mulnSr は右側にひとつ取り出す (mulnS は左側にひとつ取り出す)
Lemma mulnS m n : m * n.+1 = m + m * n.
Lemma mulnSr m n : m * n.+1 = m * n + m.
expnSr は右側にひとつ取り出す (mulSn は左側にひとつ取り出す)
Lemma expnS m n : m ^ n.+1 = m * m ^ n.
Lemma expnSr m n : m ^ n.+1 = m ^ n * m.
leq の左引数に、左右どちらかから muln する (m <= m は常に成り立ち、その左引数に左から muln した m <= n * m も (n > 0 という条件付きで) 成り立つ)
Lemma leq_pmull m n : n > 0 -> m <= n * m.
Lemma leq_pmulr m n : n > 0 -> m <= m * n.
ltn の左引数に、左右どちらかから muln する
Lemma ltn_Pmull m n : 1 < n -> 0 < m -> m < n * m.
Lemma ltn_Pmulr m n : 1 < n -> 0 < m -> m < m * n.
ltn の左右両方に muln があり、左右で対応する引数の大小関係がひっくりかえっていない。名前の左右は前提で ltn になっているのが muln のどちらにあるか。
Lemma ltn_mull m1 m2 n1 n2 : 0 < n2 -> m1 < n1 -> m2 <= n2 -> m1 * m2 < n1 * n2.
Lemma ltn_mulr m1 m2 n1 n2 : 0 < n1 -> m1 <= n1 -> m2 < n2 -> m1 * m2 < n1 * n2.
Lemma maxnMr : right_distributive muln maxn.
Lemma maxnMl : left_distributive muln maxn.
Lemma minnMr : right_distributive muln minn.
Lemma minnMl : left_distributive muln minn.
ltn の右引数に、左から expn する
Lemma ltn_expl m n : 1 < m -> n < m ^ n.
mulnbl と mulnbr は、muln の引数の片方が bool の場合を扱っていて、bool 引数が左右どちらかにあるか
なお、他の命名規則との一貫性からは mulnb と mulbn にするのではないかと思うのだが、mulnb は両方の引数が bool である場合に使っているからこういう名前になっているのかな
また、この mulnb は、mulbb じゃないのかとも思うが、muln についての性質だから n をひとつは入れたかったのだろうと思う
Lemma mulnbl (b : bool) n : b * n = (if b then n else 0).
Lemma mulnbr (b : bool) n : n * b = (if b then n else 0).
Lemma mulnb (b1 b2 : bool) : b1 * b2 = b1 && b2.
rewrite すると .*2 が muln の左右どちらかの引数につく
Lemma doubleMl m n : (m * n).*2 = m.*2 * n.
Lemma doubleMr m n : (m * n).*2 = m * n.*2.
leq_maxl は leq_addl とかと一貫性がない気がする。 以下のように並べると、addn/maxn の左引数に指定したものが、leq の左引数になるかならないか合わない
Lemma leq_addl m n : n <= m + n. Lemma leq_maxl m n : m <= maxn m n.
seq.v も調べてみよう。
take が二重になっていて、rewrite すると左右 (外側と内側) のどちらかがが残る
Lemma take_takel i j s : i <= j -> take i (take j s) = take i s.
Lemma take_taker i j s : j <= i -> take i (take j s) = take j s.
catrev の左右どちらかの引数に cat がある
Lemma catrev_catl s t u : catrev (s ++ t) u = catrev t (catrev s u).
Lemma catrev_catr s t u : catrev s (t ++ u) = catrev s t ++ u.
なんでこれが LR なんだろう?
(all_iff は知らなかったので調べたところ、all_iff A [:: B; C; D] は (A -> B) /\ (B -> C) /\ (C -> D) /\ (D -> A) みたいになるもののようだ。中身ではなぜか and じゃなくた独自の帰納型 all_iff_and を定義して使っているけど)
Lemma all_iffLR P0 Ps : all_iff P0 Ps -> forall m n, nth P0 (P0 :: Ps) m -> nth P0 (P0 :: Ps) n.
rcons の左右どちらかの引数から返値が単射である
Lemma rcons_injl x : injective (rcons^~ x).
Lemma rcons_injr s : injective (rcons s).
2つの seq が等しい場合、それぞれの seq のいちばん {左,右} の x を選ぶと、そこで分割した両側はそれぞれに等しい
Lemma eqseq_pivot2l x s1 s2 s3 s4 : x \notin s1 -> x \notin s3 -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
Lemma eqseq_pivot2r x s1 s2 s3 s4 : x \notin s2 -> x \notin s4 -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
(s1 ++ x :: s2 == s3 ++ x :: s4) の {左,右} に x がひとつしか入っていなければ、そこで分割した両側はそれぞれに等しい
Lemma eqseq_pivotl x s1 s2 s3 s4 : x \notin s1 -> x \notin s2 -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
Lemma eqseq_pivotr x s1 s2 s3 s4 : x \notin s3 -> x \notin s4 -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
(s1 ++ x :: s2 == s3 ++ x :: s4) の {左,右} が uniq ならば、x のところで分割した両側はそれぞれに等しい
Lemma uniq_eqseq_pivotl x s1 s2 s3 s4 : uniq (s1 ++ x :: s2) -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
Lemma uniq_eqseq_pivotr x s1 s2 s3 s4 : uniq (s3 ++ x :: s4) -> (s1 ++ x :: s2 == s3 ++ x :: s4) = (s1 == s3) && (s2 == s4).
前提に使っている perm_eql の l を継承
Lemma permEl s1 s2 : perm_eql s1 s2 -> perm_eq s1 s2.
perm_eq{l,r} の左右を継承
Lemma permPl s1 s2 : reflect (perm_eql s1 s2) (perm_eq s1 s2).
Lemma permPr s1 s2 : reflect (perm_eqr s1 s2) (perm_eq s1 s2).
perm_eq の2つの引数両方で、{左,右} から共通の s1 を cat している
Lemma perm_cat2l s1 s2 s3 : perm_eq (s1 ++ s2) (s1 ++ s3) = perm_eq s2 s3.
Lemma perm_cat2r s1 s2 s3 : perm_eq (s2 ++ s1) (s3 ++ s1) = perm_eq s2 s3.
perm_eql の2つの引数両方で、{左,右} から共通の s を cat している
Lemma perm_catl s t1 t2 : perm_eq t1 t2 -> perm_eql (s ++ t1) (s ++ t2).
Lemma perm_catr s1 s2 t : perm_eq s1 s2 -> perm_eql (s1 ++ t) (s2 ++ t).
subseq の2つの引数両方で、{左,右} から共通の s を cat している
Lemma subseq_cat2l s s1 s2 : subseq (s ++ s1) (s ++ s2) = subseq s1 s2.
Lemma subseq_cat2r s s1 s2 : subseq (s1 ++ s) (s2 ++ s) = subseq s1 s2.
iotaD は iota の第2引数に加算 (D) がある
iotaDl は iota の第1引数に加算 (D) がある (第1引数は第2引数の左にあるということか?)
Lemma iotaD m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
Lemma iotaDl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
uniq (zip s t) の s t の {左,右} が uniq の場合
Lemma zip_uniql (S T : eqType) (s : seq S) (t : seq T) : uniq s -> uniq (zip s t).
Lemma zip_uniqr (S T : eqType) (s : seq S) (t : seq T) : uniq t -> uniq (zip s t).
reshape の適用をキャンセルして {左,右} の引数に戻す
Lemma reshapeKl sh s : size s >= sumn sh -> shape (reshape sh s) = sh.
Lemma reshapeKr sh s : size s <= sumn sh -> flatten (reshape sh s) = s.
flatten_index の適用をキャンセルして r c のうちの {左,右} の引数に戻す
Lemma flatten_indexKl sh r c : c < nth 0 sh r -> reshape_index sh (flatten_index sh r c) = r.
Lemma flatten_indexKr sh r c : c < nth 0 sh r -> reshape_offset sh (flatten_index sh r c) = c.
rewrite すると cat の右の引数が (prefix の引数に) 残る
Lemma prefix_catr s1 s2 s1' s3 : size s1 = size s1' -> prefix (s1 ++ s2) (s1' ++ s3) = (s1 == s1') && prefix s2 s3.
rewrite すると rev が左の引数から右の引数に動く (あと prefix が suffix に変わる)
Lemma prefix_revLR s1 s2 : prefix (rev s1) s2 = suffix s1 (rev s2).
suffix の右引数が cat である
Lemma suffix_catr s1 s2 s3 : suffix s1 s2 -> suffix s1 (s3 ++ s2).
rewrite すると rev が左引数から右引数に動く
Lemma infix_revLR s1 s2 : infix (rev s1) s2 = infix s1 (rev s2).
apply すると infix の第1引数に cat が発生して cat の {左,右} 引数が付加される
Lemma catl_infix s s1 s2 : infix (s ++ s1) s2 -> infix s1 s2.
Lemma catr_infix s s1 s2 : infix (s1 ++ s) s2 -> infix s1 s2.
apply すると infix の2つの引数両方に cat が発生して cat の {左,右} 引数がもともとの引数となる
Lemma catl2_infix s s1 s2 : infix (s1 ++ s) (s2 ++ s) -> infix s1 s2.
Lemma catr2_infix s s1 s2 : infix (s ++ s1) (s ++ s2) -> infix s1 s2.
apply すると infix の第2引数の cat とその {左,右} 引数が消える
Lemma infix_catl s1 s2 s3 : infix s1 s2 -> infix s1 (s3 ++ s2).
Lemma infix_catr s1 s2 s3 : infix s1 s2 -> infix s1 (s2 ++ s3).
[seq f x y | x <- X, y <- Y] のネストした map で、X Y の {左,右} が空なら結果は空
Lemma allpairs0l f t : [seq f x y | x <- [::], y <- t x] = [::].
Lemma allpairs0r f s : [seq f x y | x <- s, y <- [::]] = [::].
[seq f x y | x <- X, y <- Y] のネストした map で、X Y の {左,右} が単一要素の場合
Lemma allpairs1l f x t : [seq f x y | x <- [:: x], y <- t x] = [seq f x y | y <- t x].
Lemma allpairs1r f s y : [seq f x y | x <- s, y <- [:: y x]] = [seq f x (y x) | x <- s].
[seq f x y | x <- X, y <- Y] のネストした map で、X Y の {左,右} が map の場合
Lemma allpairs_mapl f (g : S' -> S) s t : [seq f x y | x <- map g s, y <- t x] = [seq f (g x) y | x <- s, y <- t (g x)].
Lemma allpairs_mapr f (g : forall x, T' x -> T x) s t : [seq f x y | x <- s, y <- map (g x) (t x)] = [seq f x (g x y) | x <- s, y <- t x].
allrel X Y で X Y の {左,右} が単一要素の場合
Lemma allrel1l x ys : allrel [:: x] ys = all (r x) ys.
Lemma allrel1r xs y : allrel xs [:: y] = all (r^~ y) xs.
allrel X Y で X Y の {左,右} が cat の場合
Lemma allrel_catl xs xs' ys : allrel (xs ++ xs') ys = allrel xs ys && allrel xs' ys.
Lemma allrel_catr xs ys ys' : allrel xs (ys ++ ys') = allrel xs ys && allrel xs ys'.
allrel の右引数が mask
Lemma allrel_maskr m xs ys : allrel xs ys -> allrel xs (mask m ys).
allrel の {左,右} 引数が filter
Lemma allrel_filterl a xs ys : allrel xs ys -> allrel (filter a xs) ys.
Lemma allrel_filterr a xs ys : allrel xs ys -> allrel xs (filter a ys).
allrel の {左,右} 引数が rev
Lemma allrel_revl {T S : Type} (r : T -> S -> bool) (s1 : seq T) (s2 : seq S) : allrel r (rev s1) s2 = allrel r s1 s2.
Lemma allrel_revr {T S : Type} (r : T -> S -> bool) (s1 : seq T) (s2 : seq S) : allrel r s1 (rev s2) = allrel r s1 s2.
Lemma eq_allrel_meml {T : eqType} {S} (r : T -> S -> bool) (s1 s1' : seq T) s2 : s1 =i s1' -> allrel r s1 s2 = allrel r s1' s2.
tallyEl は tally の結果中の対の左側だけの等式 (順序無視)
tallyE は tally の結果全体の等式 (順序無視)
Lemma tallyEl s : perm_eq (unzip1 (tally s)) (undup s).
Lemma tallyE s : perm_eq (tally s) [seq (x, count_mem x s) | x <- undup s].
こうやってえんえんとみていくと、一貫していないと感じられるところもあって、自分で名前をつけるときに悩みすぎても仕方ないという気分になった。