[Coq] Coq Advent Calender : rewrite (3 of 25)

　Coq でよく使われる tactic の３つ目は rewrite です。

　rewrite は仮定にある等式を使ってゴールを書き換えます。下記の例では、リスト xs について帰納法を用いて証明していますが、ゴールの中に含まれるlength (xs ++ ys)を、帰納法の仮定IHxsを用いてrewriteすることでlength xs + length ysに書き換えています。

Coq < Lemma Sample_of_rewrite : forall (A:Set)(xs ys:list A), 
Coq < length (xs ++ ys) = length xs + length ys.
1 subgoal
  
  ============================
   forall (A : Set) (xs ys : list A),
   length (xs ++ ys) = length xs + length ys

Sample_of_rewrite < intros A xs ys.
1 subgoal
  
  A : Set
  xs : list A
  ys : list A
  ============================
   length (xs ++ ys) = length xs + length ys

Sample_of_rewrite < induction xs.                        
2 subgoals
  
  A : Set
  ys : list A
  ============================
   length (nil ++ ys) = length nil + length ys

subgoal 2 is:
 length ((a :: xs) ++ ys) = length (a :: xs) + length ys

Sample_of_rewrite < reflexivity.       
1 subgoal
  
  A : Set
  a : A
  xs : list A
  ys : list A
  IHxs : length (xs ++ ys) = length xs + length ys
  ============================
   length ((a :: xs) ++ ys) = length (a :: xs) + length ys

Sample_of_rewrite < simpl.
1 subgoal
  
  A : Set
  a : A
  xs : list A
  ys : list A
  IHxs : length (xs ++ ys) = length xs + length ys
  ============================
   S (length (xs ++ ys)) = S (length xs + length ys)

Sample_of_rewrite < rewrite IHxs.
1 subgoal
  
  A : Set
  a : A
  xs : list A
  ys : list A
  IHxs : length (xs ++ ys) = length xs + length ys
  ============================
   S (length xs + length ys) = S (length xs + length ys)

Sample_of_rewrite < reflexivity.
Proof completed.

Sample_of_rewrite < Qed.
intros A xs ys.
induction xs.
 reflexivity.
 
 simpl in |- *.
 rewrite IHxs in |- *.
 reflexivity.
 
Sample_of_rewrite is defined

Coq <