Ltac と proof term 4

append の結合性の別証明。f_equal を使ったらどうなるかやってみました。

Coq < Goal forall A (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs.
1 subgoal
  
  ============================
   forall (A : Type) (xs ys zs : list A), xs ++ ys ++ zs = (xs ++ ys) ++ zs

Unnamed_thm2 < induction xs.
2 subgoals
  
  A : Type
  ============================
   forall ys zs : list A, nil ++ ys ++ zs = (nil ++ ys) ++ zs

subgoal 2 is:
 forall ys zs : list A, (a :: xs) ++ ys ++ zs = ((a :: xs) ++ ys) ++ zs

Unnamed_thm2 < reflexivity.
1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : forall ys zs : list A, xs ++ ys ++ zs = (xs ++ ys) ++ zs
  ============================
   forall ys zs : list A, (a :: xs) ++ ys ++ zs = ((a :: xs) ++ ys) ++ zs

Unnamed_thm2 < intros.
1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : forall ys zs : list A, xs ++ ys ++ zs = (xs ++ ys) ++ zs
  ys : list A
  zs : list A
  ============================
   (a :: xs) ++ ys ++ zs = ((a :: xs) ++ ys) ++ zs

Unnamed_thm2 < simpl.
1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : forall ys zs : list A, xs ++ ys ++ zs = (xs ++ ys) ++ zs
  ys : list A
  zs : list A
  ============================
   a :: xs ++ ys ++ zs = a :: (xs ++ ys) ++ zs

Unnamed_thm2 < Show Proof.
LOC: 
Subgoals
1 -> forall (A : Type) (a : A) (xs : list A),
     (forall ys zs : list A, xs ++ ys ++ zs = (xs ++ ys) ++ zs) ->
     forall ys zs : list A, a :: xs ++ ys ++ zs = a :: (xs ++ ys) ++ zs
Proof: fun (A : Type) (xs : list A) =>
       list_ind
         (fun xs0 : list A =>
          forall ys zs : list A, xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs)
         (fun ys zs : list A => eq_refl ((nil ++ ys) ++ zs))
         (fun (a : A) (xs0 : list A)
            (IHxs : forall ys zs : list A,
                    xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) 
            (ys zs : list A) => ?1 A a xs0 IHxs ys zs) xs

ここまではだいたい前と同じ(だったと思う)。

ここで goal の両辺が cons a (なんか) の形になっているので f_equal が使えます。使ってみましょう。

Unnamed_thm2 < f_equal.
1 subgoal
  
  A : Type
  a : A
  xs : list A
  IHxs : forall ys zs : list A, xs ++ ys ++ zs = (xs ++ ys) ++ zs
  ys : list A
  zs : list A
  ============================
   xs ++ ys ++ zs = (xs ++ ys) ++ zs

Unnamed_thm2 < Show Proof.
LOC: 
Subgoals
1 -> forall A : Type,
     A ->
     forall xs : list A,
     (forall ys zs : list A, xs ++ ys ++ zs = (xs ++ ys) ++ zs) ->
     forall ys zs : list A, xs ++ ys ++ zs = (xs ++ ys) ++ zs
Proof: fun (A : Type) (xs : list A) =>
       list_ind
         (fun xs0 : list A =>
          forall ys zs : list A, xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs)
         (fun ys zs : list A => eq_refl ((nil ++ ys) ++ zs))
         (fun (a : A) (xs0 : list A)
            (IHxs : forall ys zs : list A,
                    xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) 
            (ys zs : list A) =>
          let H := ?1 A a xs0 IHxs ys zs in
          (let H0 := eq_refl a in
           (let H1 := eq_refl A in
            (fun (_ : A = A) (_ : a = a)
               (H4 : xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) =>
             eq_trans
               (f_equal (fun f : list A -> list A => f (xs0 ++ ys ++ zs))
                  (eq_refl (cons a))) (f_equal (cons a) H4)) H1) H0) H) xs

なんか複雑なことになりました。let H := ?1 A ... から後が f_equal の生成した proof term です。頑張って読んでみましょう。

H, H0, H1 は cons の各引数が両辺で等しいことの証明なのでしょう。H の定義の中に ?1 が現れているので，H がまだ解かれていない subgoal の proof term に束縛されるようです。H0, H1 は自明なので自動的に解かれて，その結果できた proof term である eq_refl に束縛されています。

後ろのほうはどうなっているんでしょう。引数と閉じ括弧が並んでいますが，この括弧は let を閉じているだけなので関数適用を中へ放り込んでもだいたい同じ意味で(たぶん)，そうすると等式の証明を三つ受け取る関数リテラルに H1, H0, H を順に渡していることになります。H1, H0 を受け取る引数の部分は wildcard になっているので，これらは結局使われていません。

というわけで，複雑に見えますが簡約してやればすっきりしそうです。問題の let H := 以下を簡約してみましょう。

let H := ?1 A a xs0 IHxs ys zs in
   eq_trans
     (f_equal (fun f : list A -> list A => f (xs0 ++ ys ++ zs))
        (eq_refl (cons a)))
     (f_equal (cons a) H)

たぶんこうなります。いま手動でやってみたのですが，もし間違っていたら教えてください。

eq_trans が何をするかは名前から明らかですが，問題は f_equal です。これ何でしょう。知らないので調べる。

Coq < Check f_equal.
f_equal
     : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

x = y の証明から f x = f y の証明を作るそうです。ちなみに定義は

Coq < Print f_equal.
f_equal = 
fun (A B : Type) (f : A -> B) (x y : A) (H : x = y) =>
match H in (_ = y0) return (f x = f y0) with
| eq_refl => eq_refl (f x)
end
     : forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

となってました。読みづらい式ですがさしあたり読めなくても問題ないと思うので気にしないことにしましょう。

話を戻して，問題の proof term ですが，

     (f_equal (fun f : list A -> list A => f (xs0 ++ ys ++ zs))
        (eq_refl (cons a)))

の部分の型は

cons a (xs0 ++ ys ++ zs) = cons a (xs0 ++ ys ++ zs)

となります。なんだ，自明な等式ですね。

二つ目の f_equal (cons a) H は，H の型が xs ++ ys ++ zs = (xs ++ ys) ++ zs なので，これがもともと示したかった等式に一致します。

というわけで，この例に限っては f_equal が生成する proof term は冗長なものになっているようです。

残りの部分は特に目新しいこともありませんが一応載せておきます。

Unnamed_thm2 < apply IHxs.
Proof completed.

Unnamed_thm2 < Show Proof.
LOC: 
Subgoals
Proof: fun (A : Type) (xs : list A) =>
       list_ind
         (fun xs0 : list A =>
          forall ys zs : list A, xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs)
         (fun ys zs : list A => eq_refl ((nil ++ ys) ++ zs))
         (fun (a : A) (xs0 : list A)
            (IHxs : forall ys zs : list A,
                    xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) 
            (ys zs : list A) =>
          let H := IHxs ys zs in
          (let H0 := eq_refl a in
           (let H1 := eq_refl A in
            (fun (_ : A = A) (_ : a = a)
               (H4 : xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) =>
             eq_trans
               (f_equal (fun f : list A -> list A => f (xs0 ++ ys ++ zs))
                  (eq_refl (cons a))) (f_equal (cons a) H4)) H1) H0) H) xs

Unnamed_thm2 < Qed.
induction xs.
 reflexivity.
 
 intros.
 simpl.
 f_equal.
 apply IHxs.
 
Unnamed_thm2 is defined