pure Coq で 0 + 0 というのは Nat.add O O であるが、 Coq/SSReflect での 0 + 0 は addn O O である。
(addn をぜんぶ書くと mathcomp.ssreflect.ssrnat.addn)
Nat.add と addn は等しい (convertible な) 関数である。 実際、reflexivity 一発で等しいと証明できる。
Goal Nat.add = addn. Proof. reflexivity. Qed.
それなのになんでわざわざ Nat.add から addn に変えているんだっけ、と 調べてみると、 simpl で勝手に展開されるのを防ぐためのようだ。
Coq reference manual, SSReflect proof language , Locking, unlocking にちょうど addn がどう定義してあるか書いてあって、これが、(addn (S n) m) が (S (addn n m)) に変わってしまうことを防いでいるというようなことが書いてある。
Definition addn := nosimpl plus.
実際には以下のようになっているようだが、nosimpl が使われているというところはあっている。
Definition addn := nosimpl addn_rec. Definition addn_rec := Nat.add.
本当に simpl で変わらないかどうか試してみよう
Goal 0 = Nat.add 1 2. (* eq O (Nat.add (S O) (S (S O))) *) simpl. (* eq O (S (S (S O))) *) Abort. Goal 0 = addn 1 2. (* eq O (addn (S O) (S (S O))) *) simpl. (* eq O (addn (S O) (S (S O))) *) Abort.
たしかに、Nat.add では 変わるけれど、addn では変わらない。
では、なんで変わらないのか?
たぶん、nosimpl というのが理由なのだろうが、まずその前に、 Arguments コマンドで simpl の挙動を設定できたはずなので、 その設定を確認しよう
About Nat.add. (* Nat.add : nat -> nat -> nat Nat.add is not universe polymorphic Arguments Nat.add (_ _)%nat_scope Nat.add is transparent Expands to: Constant Coq.Init.Nat.add *) About addn. (* addn : nat -> nat -> nat addn is not universe polymorphic Arguments addn (_ _)%nat_scope addn is transparent Expands to: Constant mathcomp.ssreflect.ssrnat.addn *)
About で調べると、両方とも、Arguments のところには simpl についての記述はない
ちなみに、以下のように myplus を定義して、Arguments で simpl never と指定すると、 About でも simpl never と出てくるので、Nat.add と addn にはこの種の設定はされていないのだろう
Definition myplus := Nat.add. Arguments myplus : simpl never. About myplus. (* myplus : nat -> nat -> nat myplus is not universe polymorphic Arguments myplus (_ _)%nat_scope : simpl never The reduction tactics never unfold myplus myplus is transparent Expands to: Constant Top.myplus *)
では、nosimpl とはなんなのか調べてみる
About nosimpl. (* Notation nosimpl t := (let 'tt := tt in t) Expands to: Notation Coq.ssr.ssreflect.nosimpl *)
これは notation で、nosimpl t は let 'tt := tt in t の略記らしい。 let 束縛の左辺に ' がついているのは、コンストラクタがひとつだけの場合の match を書く記法で、match tt with tt => t end と同じである。
ということは、nosimpl plus というのは match tt with tt => plus end と同じということになるが、 なんでこうすると simpl で変化しなくなるのだろうか
という疑問を調べる前にいちおう nosimpl を使わずに自分で同じことをして確認してみる。
Definition myadd := match tt with tt => Nat.add end. Goal 0 = myadd 1 2. (* @eq nat O (myadd (S O) (S (S O))) *) simpl. (* @eq nat O (myadd (S O) (S (S O))) *) Abort.
自分でやってもやはり simpl で展開されない
いちおう、match を使わないのも試してみる
Definition myadd0 := Nat.add. Goal 0 = myadd0 1 2. (* @eq nat O (myadd0 (S O) (S (S O))) *) simpl. (* @eq nat O (S (S (S O))) *) Abort.
これは simpl で変化する
やはり、match が simpl の挙動に影響するようだ
そもそも、simpl というのはどういう変形をするものなのかを調べてみる
simpl というのは、定数を unfold する条件として、unfold して iota-reduction が起きるときだけ unfold する、 というものらしい。 さらに、fix 項の iota-reduction では、iota-reduction した結果には fix 項が入っているが、 これをもともとの定数で表現する、という仕掛けのようだ。
たしかに考えてみれば、reduction をするだけなら S m + n は S ((fix ...) m n) になるから、 これが S (m + n) になるのはちょっと難しいことをやっている気はする。 いままで気にしてなかったけど。
それはそれとして、simpl で addn が展開されないのは、 fix 項の iota-reduction で展開された fix 項を addn で表現することができることを simpl が見抜けない、からかなぁ。 match tt with tt => Nat.add end は Nat.add と convertible なので、 addn で表現することは可能なわけで、でもそのことを見抜けないから展開されない、のだと思う。
manual には fix 項の展開結果を、もとの定数で表現できないケースとして succ := plus (S O) という例が載っているので これを試してみよう。
Definition succ := plus (S O). Goal forall n, 0 = succ (S n). (* forall n : nat, @eq nat O (succ (S n)) *) simpl. (* forall n : nat, @eq nat O (succ (S n)) *) Abort.
たしかに simpl では展開されないようだ。
succ を plus に展開して計算を進めることを考えると、 plus の計算を進めることにより plus の第1引数が O になってしまうので、 plus の第1引数が S O であるという、succ には戻せない形になる、かな。 (もちろん、もっと計算を進めれば S (S n) になるので、plus さえ出てこない形になる)
succ (S n) => plus (S O) (S n) => (fix ...) (S O) (S n) => S ((fix ...) O (S n)) => S (plus O (S n))
あと、reference manual の simpl の次に cbn の説明があるのだが、 cbn というのはキレイな simpl なのだな (cbn was intended to be a more principled, faster and more predictable replacement for simpl. と書いてある)
そして、simpl と cbn の違いとして、再帰でもともとの定数を再利用できなくても unfold する、とある。
Goal forall m n, 0 = addn m.+1 n. (* forall m n : nat, @eq nat O (addn (S m) n) *) cbn. (* forall m n : nat, @eq nat O (S (addn_rec m n)) *) Abort.
ふむ、cbn だと addn も展開されるようだ。 (そして addn には戻せないようで、addn_rec になっている)
ということは、nosimpl は cbn には効かないわけで、 SSReflect では simpl の動作に依存しているということになるか。
あと、simpl はどのくらい見抜いてくれるのか、というところで、 とりあえず Nat.add を let で束縛してみると、 とくに問題なく見抜いてくれる。 (simpl がゴールを変形し、かつ、結果には myadd1 が使われている)
Definition myadd1 := let x := Nat.add in x. Goal forall m n, 0 = myadd1 (S m) n. (* forall m n : nat, @eq nat O (myadd1 (S m) n) *) simpl. (* forall m n : nat, @eq nat O (S (myadd1 m n)) *) Abort.
では、余計な引数をつけた関数にするとどうか、というと、これも問題ない。
Definition myadd2 (dummy : bool) := Nat.add. Goal forall m n, 0 = myadd2 true (S m) n. (* forall m n : nat, @eq nat O (myadd2 true (S m) n) *) simpl. (* forall m n : nat, @eq nat O (S (myadd2 true m n)) *) Abort.
なかなか。
以下のように試した限りは、 関数の型に直接にソート (Type とか Set とか) を書けばそうなるけれど、 ちょっとでも型の書き方を複雑にするとそうならなくなってしまう感じかな (明示的に Arguments コマンドで設定することはできる)
ここで、x*y がふつうは自然数の乗算 (Nat.mul x y) なのだが、 type_scope では組を表現する型 (prod x y) なので、 その違いを使って引数の解釈を確認している
Fail Check @id (nat * nat). (* なんか動かない The term "nat" has type "Set" while it is expected to have type "nat". というエラーなので、x*y が Nat.mul と解釈されているようだ *) About id. (* Arguments id [A] _ と出てくる *) Definition id1 (A : Type) (x : A) := x. Check id1 (nat * nat). (* 自分で id と同じ定義をすると動く *) About id1. (* Arguments id1 _%type_scope _ と出てきて、第1引数が type_scope と解釈される設定になっているぽい *) (* Coq のソースの theories/Init/Datatypes.v では ID という型を定義して 使っているので、それを真似して定義してみる *) Definition ID2 := forall A:Type, A -> A. Definition id2 : ID2 := fun A x => x. Fail Check @id2 (nat * nat). (* これは id と同様に失敗する *) About id2. (* なぜかわからないが Arguments は出てこない *) Arguments id2 _%type_scope _. Check @id2 (nat * nat). (* 明示的に Arguments で設定すれば動く *) (* ID を展開してみる *) Definition id3 : forall A:Type, A -> A := fun A x => x. Check @id3 (nat * nat). (* これは動く *) About id3. (* Arguments id3 _%type_scope _ と出てくる *) (* Type というのを T という定数にしてみる *) Definition T := Type. Definition id4 : forall A:T, A -> A := fun A x => x. Fail Check @id4 (nat * nat). (* これは動かない *) About id4. (* なぜか Arguments はでてこない *) (* Type だけじゃなくて Set も試してみる *) Definition id5 : forall A:Set, A -> A := fun A x => x. Check @id5 (nat * nat). (* これは動く*)
なお、Coq 8.13.1 で試した
オンラインでちょっと聞いてみた