Ltac と proof term 3

今度は等式の証明でやってみました。append の結合性。

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

induction をするに決まっている。

Unnamed_thm0 < 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_thm0 < Show Proof.
LOC: 
Subgoals
1 -> forall (A : Type) (ys zs : list A), nil ++ ys ++ zs = (nil ++ ys) ++ zs
2 -> 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) 
         (?1 A)
         (fun (a : A) (xs0 : list A)
            (IHxs : forall ys zs : list A,
                    xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) => 
          ?2 A a xs0 IHxs) xs

なんだか長い式が出てきますが，list_ind を使っただけです。

最初の subgoal は，append の定義に従って計算すると両辺が同じものになるので reflexivity でできますね。

Unnamed_thm0 < 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_thm0 < 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) => 
          ?1 A a xs0 IHxs) xs

eq_refl そのままですね。簡約すると一致するのでこれでいいんでしょうか。

ちょっと戻って，明示的に簡約したときに proof term がどうなるのか見てみましょう。

Unnamed_thm0 < Undo.
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_thm0 < simpl.
2 subgoals
  
  A : Type
  ============================
   forall ys zs : list A, ys ++ zs = ys ++ zs

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

Unnamed_thm0 < Show Proof.
LOC: 
Subgoals
1 -> forall (A : Type) (ys zs : list A), ys ++ zs = ys ++ zs
2 -> 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) 
         (?1 A)
         (fun (a : A) (xs0 : list A)
            (IHxs : forall ys zs : list A,
                    xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) => 
          ?2 A a xs0 IHxs) xs

Unnamed_thm0 < 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_thm0 < 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 (ys ++ zs))
         (fun (a : A) (xs0 : list A)
            (IHxs : forall ys zs : list A,
                    xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) => 
          ?1 A a xs0 IHxs) xs

簡約しても proof term は ?1 A のまま変わらないみたいですね。最終的な形も simpl しなかったときと同じです。そういえば二つの型が convertible なら一方の型をもつ term はもう一方の型ももつ，という規則が CIC にあったような気がします。

次の subgoal は IH で rewrite するのですが，たぶん束縛変数を含む項は rewrite できないのでまず intros します。

Unnamed_thm0 < 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_thm0 < 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 (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

おそらく予想通りでしょうが，関数抽象が現れました。書き換えます。

Unnamed_thm0 < rewrite IHxs.
Toplevel input, characters 0-12:
> rewrite IHxs.
> ^^^^^^^^^^^^
Error: Found no subterm matching "xs ++ ?117 ++ ?118" in the current goal.

間違えました。先に simpl しないと書き換えられる形になりません。

Unnamed_thm0 < simpl; rewrite IHxs.
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_thm0 < 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 (ys ++ zs))
         (fun (a : A) (xs0 : list A)
            (IHxs : forall ys zs : list A,
                    xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) 
            (ys zs : list A) =>
          eq_ind_r (fun l : list A => a :: l = a :: (xs0 ++ ys) ++ zs)
            (?1 A a xs0 IHxs ys zs) (IHxs ys zs)) xs

例によつて eq_ind_r が現れました。

ついてきてますか。ぼくは proof term を真面目に読まないで適当にやってたらよくわからなくなってやり直しました。

でも subgoal は自明な等式なので，とりあえず証明は完成です。

Unnamed_thm0 < reflexivity.
Proof completed.

Unnamed_thm0 < 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 (ys ++ zs))
         (fun (a : A) (xs0 : list A)
            (IHxs : forall ys zs : list A,
                    xs0 ++ ys ++ zs = (xs0 ++ ys) ++ zs) 
            (ys zs : list A) =>
          eq_ind_r (fun l : list A => a :: l = a :: (xs0 ++ ys) ++ zs)
            (eq_refl (a :: (xs0 ++ ys) ++ zs)) (IHxs ys zs)) xs

Unnamed_thm0 < Qed.
induction xs.
 simpl.
 reflexivity.
 
 intros.
 simpl; rewrite IHxs.
 reflexivity.
 
Unnamed_thm0 is defined

新しい発見があったのかなかったのかよくわかりませんでしたが，どうやら簡約は proof term に影響を及ぼさないようです。