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].
こうやってえんえんとみていくと、一貫していないと感じられるところもあって、自分で名前をつけるときに悩みすぎても仕方ないという気分になった。
ふと、3つのコンストラクタをもつ帰納型を有限型 (finType) として扱いたくなったのだが、どうやればいいのか調べるのにけっこう苦労した。
結局、以下のようにすれば可能なようだ。
From mathcomp Require Import all_ssreflect.
From HB Require Import structures.
Inductive mytype :=
| C1 : bool -> mytype
| C2 : bool -> mytype
| C3 : bool -> mytype.
Lemma sum_of_mytypeK : cancel
(fun (v : mytype) =>
match v with
| C1 b => inl (inl b)
| C2 b => inl (inr b)
| C3 b => inr b
end)
(fun (v : bool + bool + bool) =>
match v with
| inl (inl b) => C1 b
| inl (inr b) => C2 b
| inr b => C3 b
end).
Proof. by case; case. Qed.
HB.instance Definition _ := Finite.copy mytype (can_type sum_of_mytypeK).
Check mytype : choiceType.
Check mytype : countType.
Check mytype : eqType.
Check mytype : finType.
ここでは、bool + bool + bool 型 (つまり sum (sum bool bool) bool 型) と mytype が同型であることを証明して、それにより mytype が有限型であることを登録している。
これをやると、finType の継承元 (choiceType, countType, eqType) としても mytype が自動的に登録されるようだ。 (登録されるので、mytype : choiceType のようなキャストが通る。このキャストは型を、登録された choiceType の値からその型を取り出す式に変換している。)
もちろん、mytype などというものは定義せずに、bool + bool + bool 型を使うという方法もあるが、 そうすると inl (inr b) みたいなわかりにくい表現を使わないといけない。 (inl (inr b) を呼び出す関数として C1 を定義して、Arguments C1 : simpl never. とすればかなり inl (inr b) という内部表現を隠せるが、それでも出てきてしまうことはあって、change で修正しなければいけないので面倒くさい )
まぁ、Notation で inl (inr b) を C1 b にみせかければよかったのかもしれない。 でも、sum 型を他の用途でも使っているとそっちにも影響するし、分解を [a|b|c] と書きたいところを [[a|b]|c] と書かなければならない問題は残る。
なお、環境は Rocq 9.0.0 と rocq-mathcomp-ssreflect 2.4.0 である。
演算子の優先順位というのは、式の中に ... op1 e op2 ... という部分があったとき、つまり式 e が演算子 op1 と演算子 op2 ではさまれていたときに、 その式 e が優先順位の高い方の演算子の引数となるということである。 綱引きみたいな感じ。
ここでいう演算子は二項演算子や単項演算子だけとはかぎらない。 一般には、式の導出規則で式が左右の端に出現するものは、その端に出現する式を他の演算子とではさむことができるので、その式がどちらに属するかを優先順位によって指定することができる。
yacc とかの優先順位は、衝突があったときに shift と reduce のどちらかを選ぶ、と実装される。 SDF では (SGLR により曖昧なものも含めてすべての構文木を生成する仕掛けなので) 導出の抑制を指定するという話になっている。
ただ、SDF の導出抑制は抑制しすぎて受け付ける言語が小さくなってしまう場合があるようで、よろしくない。
ということで、そういうことが起きない (受け付ける言語が変わらない) ように、 文法を優先順位を反映するように変形する、という話がある。
前者の著者の D論が後者で、Chapter 4 に前者の Safe Specification of Operator Precedence Rules が入っている。 (D論のほうが後で書かれているだろうから、修正がおこなわれているかもしれない)
ここであげられているアルゴリズムで以下のように文法を変形できるという例が記述されている。
入力として以下の文法が与えられる。 (E + E が左結合というのが (left) という記述で指定され、E + E よりも i E と a のほうが優先順位が低いというのが不等号 > で指定されている。 )
E ::= E + E (left)
> i E
| a
出力として以下の文法が生成される。
E ::= E1 + E2 | i E | a E1 ::= E1 + E3 | a E2 ::= i E | a E3 ::= a
この文法は、以下のような足し算と OCaml スタイルの if 式を表現している。 (区別しやすくするため、トークンを double quote でくくってある)
E ::= E "+" E
| "if" E "then" E "else" E
| "a"
i E というのは i と E の連結で、i は "if" E "then" E "else" に対応している。 OCaml スタイルの if 式は "if" E "then" E "else" E だが、"if" から "else" までは両端がトークンなので、かっこみたいなものとみなせる。 そのため優先順位には関係しないので、i としてまとめている。 こうやってまとめると、i は前置単項演算子とみなせる。
ということで、二項演算子 + と、前置単項演算子 i からなる式で、後者のほうが優先順位が低いという文法を考えていることになる。 (二項演算子よりも前置単項演算子の優先順位が高いなら、単項演算子のプラスやマイナスと同じになるので、単項演算子の優先順位が低いというのがこの例の面白く難しい点である。)
さて、変形された文法を少し展開して単純にすると、以下のようになる。
E ::= E1 + E2 | i E | a E1 ::= E1 + a | a E2 ::= i E | a
これを眺めてしばらく考える。
まぁ、なんとかわかった気がする。 ... i a + ... という列があったときに、a は (優先順位が i よりも高い) + の引数になるようになっていると思う。
でも、この文法はわかりやすくはないよな。+ が 2箇所、i が 2箇所、a が 4箇所出現していて、(優先順位で記述されていた文法と違って) 重複があるし。
優先順位を使った文法のほうが、意図を素直に表現できていると思う。
なお、件のD論の Chapter 5 Operator Precedence for Data-dependent Grammars では、 (Chapter 3 で説明されている) data-dependent grammar というものを使って、そういう重複を起こさずに優先順位を実装する方法を述べている。 これは GLL ベースで、attributed grammar ぽいことをやって、優先順位に反する構文木を除去していくというものだと思う。 ただ、これって決定的な動作をするかどうかいまいち確信できないような気がする。
GLL parsing をちょっと調べたのだが、 これは Earley parsing に近いと思った。
まぁ、lookahead で枝刈りするのは Earley にはないから、ちょっと違うか。