match goal の中で dependent destruction すると fail する

久しぶりに Coq を触っててしばらくはまった話。

とりあえず準備。

Require Import Program.

Set Implicit Arguments.

Inductive fin : nat -> Set :=
| First : forall n, fin (S n)
| Next : forall n, fin n -> fin (S n).

fin n はサイズ n の有限集合の型みたいなのです。手っ取り早く例を作るために cpdt から拾ってきました。

で，これから fin 2 の要素はふたつしかないよ，ということを証明してみます。とりあえず通る証明。

Coq < Goal forall x : fin 2, x = First 1 \/ x = Next (First 0).
1 subgoal
  
  ============================
   forall x : fin 2, x = First 1 \/ x = Next (First 0)

Unnamed_thm < intro x.
1 subgoal
  
  x : fin 2
  ============================
   x = First 1 \/ x = Next (First 0)

Unnamed_thm < dependent destruction x.
2 subgoals
  
  ============================
   First 1 = First 1 \/ First 1 = Next (First 0)

subgoal 2 is:
 Next x = First 1 \/ Next x = Next (First 0)

Unnamed_thm < auto.
1 subgoal
  
  x : fin 1
  ============================
   Next x = First 1 \/ Next x = Next (First 0)

Unnamed_thm < dependent destruction x.
2 subgoals
  
  ============================
   Next (First 0) = First 1 \/ Next (First 0) = Next (First 0)

subgoal 2 is:
 Next (Next x) = First 1 \/ Next (Next x) = Next (First 0)

Unnamed_thm < auto.
1 subgoal
  
  x : fin 0
  ============================
   Next (Next x) = First 1 \/ Next (Next x) = Next (First 0)

Unnamed_thm < inversion x.
Proof completed.

これで一応証明はできてます。でもこの証明だと，システムが付けた x っていう名前に依存してて嫌だなあとか思ったりします。最初のは intro で導入された x なので同じ名前ですけど，二回目の dependent destruction とかはたまたま同じ名前になってるだけです。dependent destruction は同じ名前にしてくれるように作ってあるのかもしれませんけど，例えば (この例だと fail するけど) destruct を使ったりすると別の名前になってしまうことがあります。なので，ここで x という名前に依存しているのは，あまりよい proof script ではないように思います。

ということで，変数の名前を使わないで証明を書き直したくなりました。名前を直接書かずに仮定に言及するにはどうしたらよいかというと，まあパターンマッチを使うのでしょう。

Unnamed_thm < Restart.
1 subgoal
  
  ============================
   forall x : fin 2, x = First 1 \/ x = Next (First 0)

Unnamed_thm < intro.
1 subgoal
  
  x : fin 2
  ============================
   x = First 1 \/ x = Next (First 0)

Unnamed_thm < match goal with [a : fin _ |- _] => dependent destruction a end.
Error: No matching clauses for match goal
       (use "Set Ltac Debug" for more info).

なんか失敗しました。なんででしょう。idtac にしてみると

Unnamed_thm < match goal with [a : fin _ |- _] => idtac a end.
x
1 subgoal
  
  x : fin 2
  ============================
   x = First 1 \/ x = Next (First 0)

となるので意図した通りに仮定にマッチしていそうです。

で，どうもよくわからないのですがなんとなく lazymatch を使ってみたら

Unnamed_thm < lazymatch goal with [a : fin _ |- _] => dependent destruction a end.
Toplevel input, characters 40-63:
> lazymatch goal with [a : fin _ |- _] => dependent destruction a end.
>                                         ^^^^^^^^^^^^^^^^^^^^^^^
Error: Ltac variable a is bound to x which cannot be coerced to
a fresh identifier.

エラーの内容が変化しました。どうやら a の値が fresh identifier でないといけないけどそうでないと言われている気がします。

coq-8.3pl3/theories/Program/Equality.v を見てみると以下のような記述がありました。

Tactic Notation "dependent" "destruction" ident(H) := 
  do_depelim' ltac:(fun hyp => do_case hyp) H.

つまり引数は ident でなければならないらしいです。これは ident に束縛されていることにはならないんだろうかという気もするんですけどそのへんよくわからないので，とりあえず fresh ident ならいいんだろうか，ということでこうしてみた。

Unnamed_thm < match goal with [a : fin _ |- _] => let id := fresh in rename a into id; dependent destruction id end.
2 subgoals
  
  ============================
   First 1 = First 1 \/ First 1 = Next (First 0)

subgoal 2 is:
 Next H = First 1 \/ Next H = Next (First 0)

なんかうまく動くらしい。

というわけで最終的な証明。

  intro; repeat
    match goal with
      | [a : fin _ |- _] =>
        let id := fresh in
          rename a into id; dependent destruction id; auto
    end.
Qed.

簡単になったのかなってないのかよくわからないけど，変数名に依存しない形にはなりました。

たぶんこれ，tactic 書くときに使いどころがあるかも。

Ltac destruct_fin :=
  match goal with
    | [a : fin 0 |- _] => let id := fresh in rename a into id; dependent destruction id
    | [a : fin (S _) |- _] => let id := fresh in rename a into id; dependent destruction id
  end.

Goal forall x : fin 2, x = First 1 \/ x = Next (First 0).
Proof.
  intro; repeat destruct_fin; auto.
Qed.

ちなみによくわからないのは，dependent destruction じゃなくて inversion も引数に ident を要求すると reference manual には書いてあるんですが，dependent destruction と書いたところを inversion に変えるとエラーにはならなかったりするんですよね (この問題は inversion では解けないけど)。

で，試してみたら

Coq < Goal forall n, 0 < n -> 1 <= n.
1 subgoal
  
  ============================
   forall n : nat, 0 < n -> 1 <= n

Unnamed_thm < intros n H.
1 subgoal
  
  n : nat
  H : 0 < n
  ============================
   1 <= n

Unnamed_thm < match goal with [H : _ < _ |- _] => dependent destruction H end.
Error: No matching clauses for match goal
       (use "Set Ltac Debug" for more info).

Unnamed_thm < Tactic Notation "my_inversion" ident(H) := inversion H.

Unnamed_thm < match goal with [H : _ < _ |- _] => my_inversion H end.
Error: No matching clauses for match goal
       (use "Set Ltac Debug" for more info).

Unnamed_thm < match goal with [H : _ < _ |- _] => inversion H end.
2 subgoals
  
  n : nat
  H : 0 < n
  H0 : 1 = n
  ============================
   1 <= 1

subgoal 2 is:
 1 <= S m

となるので Tactic Notation と絡むときだけ発生する問題かも。