Ltac と proof term 2

今度は算術でやってみました。

Coq < Goal forall n, n = 0 \/ 1 <= n.
1 subgoal
  
  ============================
   forall n : nat, n = 0 \/ 1 <= n

こんなのを証明してみましょう。帰納法に決まってるので帰納法を使います。

Unnamed_thm < induction n.
2 subgoals
  
  ============================
   0 = 0 \/ 1 <= 0

subgoal 2 is:
 S n = 0 \/ 1 <= S n

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> 0 = 0 \/ 1 <= 0
2 -> forall n : nat, n = 0 \/ 1 <= n -> S n = 0 \/ 1 <= S n
Proof: fun n : nat =>
       nat_ind (fun n0 : nat => n0 = 0 \/ 1 <= n0) 
         ?1 (fun (n0 : nat) (IHn : n0 = 0 \/ 1 <= n0) => ?2 n0 IHn) n

nat_ind に展開されるようです。nat を定義したときに自動的に生成される induction principle ですね。

型を確認してみます。

Unnamed_thm < Check nat_ind.
nat_ind
     : forall P : nat -> Prop,
       P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n

上の proof term と見比べると，?1 が P 0 で IHn が P n 型の仮引数，?2 n0 IHn が P (S n0) 型となることがわかります。

最初の subgoal を片付けましょう。いかにも成り立ちそうなものが左側に見えています。

Unnamed_thm < left.
2 subgoals
  
  ============================
   0 = 0

subgoal 2 is:
 S n = 0 \/ 1 <= S n

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> 0 = 0
2 -> forall n : nat, n = 0 \/ 1 <= n -> S n = 0 \/ 1 <= S n
Proof: fun n : nat =>
       nat_ind (fun n0 : nat => n0 = 0 \/ 1 <= n0) 
         (or_introl (1 <= 0) ?1)
         (fun (n0 : nat) (IHn : n0 = 0 \/ 1 <= n0) => ?2 n0 IHn) n

proof term に or_introl が現れました。

left はコンストラクタを二つもつ型が goal のとき，その一つ目を適用する tactic で，ここでは apply or_introl と同じです(たぶん)。

Unnamed_thm < reflexivity.
1 subgoal
  
  n : nat
  IHn : n = 0 \/ 1 <= n
  ============================
   S n = 0 \/ 1 <= S n

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> forall n : nat, n = 0 \/ 1 <= n -> S n = 0 \/ 1 <= S n
Proof: fun n : nat =>
       nat_ind (fun n0 : nat => n0 = 0 \/ 1 <= n0)
         (or_introl (1 <= 0) (eq_refl 0))
         (fun (n0 : nat) (IHn : n0 = 0 \/ 1 <= n0) => ?1 n0 IHn) n

reflexivity は apply refl_equal と等価なのでした。proof term では eq_refl になってますが，refl_equal は Notation で，eq_refl に展開されるように定義されています。

これで or_introl に渡される引数が完成しました。次はもうひとつの subgoal ですが，今度は左側がいかにも成り立ちそうにないので右側を狙います。

Unnamed_thm < right.
1 subgoal
  
  n : nat
  IHn : n = 0 \/ 1 <= n
  ============================
   1 <= S n

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> forall n : nat, n = 0 \/ 1 <= n -> 1 <= S n
Proof: fun n : nat =>
       nat_ind (fun n0 : nat => n0 = 0 \/ 1 <= n0)
         (or_introl (1 <= 0) (eq_refl 0))
         (fun (n0 : nat) (IHn : n0 = 0 \/ 1 <= n0) =>
          or_intror (S n0 = 0) (?1 n0 IHn)) n

さっきとだいたい同じですね。or の二つ目のコンストラクタは or_intror という名前だそうです。

場合分けします。

Unnamed_thm < destruct IHn.
2 subgoals
  
  n : nat
  H : n = 0
  ============================
   1 <= S n

subgoal 2 is:
 1 <= S n

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> forall n : nat, n = 0 -> 1 <= S n
2 -> forall n : nat, 1 <= n -> 1 <= S n
Proof: fun n : nat =>
       nat_ind (fun n0 : nat => n0 = 0 \/ 1 <= n0)
         (or_introl (1 <= 0) (eq_refl 0))
         (fun (n0 : nat) (IHn : n0 = 0 \/ 1 <= n0) =>
          or_intror (S n0 = 0)
            match IHn with
            | or_introl H => ?1 n0 H
            | or_intror H => ?2 n0 H
            end) n

destruct するとやはり match 式が現れます。

n の値がわかっているので代入したい。

Unnamed_thm < subst.
2 subgoals
  
  ============================
   1 <= 1

subgoal 2 is:
 1 <= S n

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> 1 <= 1
2 -> forall n : nat, 1 <= n -> 1 <= S n
Proof: fun n : nat =>
       nat_ind (fun n0 : nat => n0 = 0 \/ 1 <= n0)
         (or_introl (1 <= 0) (eq_refl 0))
         (fun (n0 : nat) (IHn : n0 = 0 \/ 1 <= n0) =>
          or_intror (S n0 = 0)
            match IHn with
            | or_introl H => eq_ind_r (fun n1 : nat => 1 <= S n1) ?1 H
            | or_intror H => ?2 n0 H
            end) n

eq_ind_r って何でしょう。eq_ind とは違うのか，と思って確認してみました。

Coq < Print eq_ind.
eq_ind = 
fun (A : Type) (x : A) (P : A -> Prop) => eq_rect x P
     : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, x = y -> P y

Coq < Print eq_ind_r.
eq_ind_r = 
fun (A : Type) (x : A) (P : A -> Prop) (H : P x) (y : A) (H0 : y = x) =>
eq_ind x (fun y0 : A => P y0) H y (eq_sym H0)
     : forall (A : Type) (x : A) (P : A -> Prop),
       P x -> forall y : A, y = x -> P y

だそうです。等式の左右が違うのか。

ところで今は変数への代入を使いましたが，より一般的な書き換えを行う tactic として rewrite があります。こっちを使うと proof term はどうなるんでしょう。試してみましょう。

Unnamed_thm < Undo.
2 subgoals
  
  n : nat
  H : n = 0
  ============================
   1 <= S n

subgoal 2 is:
 1 <= S n

Unnamed_thm < rewrite H.
2 subgoals
  
  n : nat
  H : n = 0
  ============================
   1 <= 1

subgoal 2 is:
 1 <= S n

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> forall n : nat, n = 0 -> 1 <= 1
2 -> forall n : nat, 1 <= n -> 1 <= S n
Proof: fun n : nat =>
       nat_ind (fun n0 : nat => n0 = 0 \/ 1 <= n0)
         (or_introl (1 <= 0) (eq_refl 0))
         (fun (n0 : nat) (IHn : n0 = 0 \/ 1 <= n0) =>
          or_intror (S n0 = 0)
            match IHn with
            | or_introl H => eq_ind_r (fun n1 : nat => 1 <= S n1) (?1 n0 H) H
            | or_intror H => ?2 n0 H
            end) n

なんかちょっとだけ長くなりました。何が違うかよく見てみると，?1 に引数が渡ってますね。

subst は代入した後で clear してしまいますが，rewrite はそんなことしないので，残った n0 と H が ?1 への引数として (実際の意図としては，?1 の中で使われる可能性がある変数として？) 渡されることになるのですね。

不等式の証明をすることになるのですが，まずは不等号の定義を見てみましょう。実体は le という inductive predicate です。

Unnamed_thm < Print le.
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m

le_n が反射性，le_S が推移性もどきの形をしていることがわかります。le のコンストラクタの与え方は他にも考えられますが (0 <= n | n <= m -> S n <= S m とか)，運のいいことに Coq で採用されている上の定義が今の goal にはちょうどよい形をしています。

Unnamed_thm < constructor.
1 subgoal
  
  n : nat
  H : 1 <= n
  ============================
   1 <= S n

Unnamed_thm < Show Proof.
LOC: 
Subgoals
1 -> forall n : nat, 1 <= n -> 1 <= S n
Proof: fun n : nat =>
       nat_ind (fun n0 : nat => n0 = 0 \/ 1 <= n0)
         (or_introl (1 <= 0) (eq_refl 0))
         (fun (n0 : nat) (IHn : n0 = 0 \/ 1 <= n0) =>
          or_intror (S n0 = 0)
            match IHn with
            | or_introl H => eq_ind_r (fun n1 : nat => 1 <= S n1) (le_n 1) H
            | or_intror H => ?1 n0 H
            end) n

一つ目のコンストラクタ le_n の型が goal にマッチするので，これが apply されました。マッチングで機械的に求まる引数の 1 は自動的に推論されて，subgoal が完成しました。eq_ind_r の第二引数にこの式が現れています。

次の goal は le_S の型にマッチします。le_S の引数が subgoal として残りますが，これは local context にあるものがそのまま使えます。

Unnamed_thm < constructor.
1 subgoal
  
  n : nat
  H : 1 <= n
  ============================
   1 <= n

Unnamed_thm < assumption.
Proof completed.

Unnamed_thm < Qed.
induction n.
 left.
 reflexivity.
 
 right.
 destruct IHn.
  rewrite H.
  constructor.
  
  constructor.
  assumption.
  
Unnamed_thm is defined

Coq < Print Unnamed_thm.
Unnamed_thm = 
fun n : nat =>
nat_ind (fun n0 : nat => n0 = 0 \/ 1 <= n0) (or_introl (1 <= 0) (eq_refl 0))
  (fun (n0 : nat) (IHn : n0 = 0 \/ 1 <= n0) =>
   or_intror (S n0 = 0)
     match IHn with
     | or_introl H => eq_ind_r (fun n1 : nat => 1 <= S n1) (le_n 1) H
     | or_intror H => le_S 1 n0 H
     end) n
     : forall n : nat, n = 0 \/ 1 <= n

というわけで完成しました。最後の式を見ると ?1 n0 H だった部分の n0 H がそのまま残ってるようで一瞬不思議に思いましたが，偶然そういう形になっただけです(たぶん)。

subst や rewrite が eq_ind_r を使った proof term を生成する (rewrite <- を使うと，r のつかない eq_ind になります) ということには，ただ tactic 書いてるだけだと気付きにくいかな，と思います。