Coq初心者の忘備録

はじめに

こんにちはAAGです。
今回は、公理的集合論で遊ぶのに向けてCoqを学習している時に書いた忘備録です。
初めてから一週間ほどのガチで初心者なのでやさしく訂正等していただけると助かります。
CoqはWeb上でできるというサイトがあったので借りました。参考文献[2]です。

本題（小学生並みの感想）

リストの性質 rev_app_distr (和の反転は逆順の反転の和)をほかのリストの性質に頼らず証明しました。
試行錯誤してinductionできるのが変数だけでないと分かりました。

コード

      Require Import List.

Goal forall(A:Type)(l1 l2:list A),rev(l1++l2)=rev l2 ++ rev l1.
Proof.
intros.
induction l1.
 (*1*)
 simpl.
 induction l2.
  (*1-1*)
  reflexivity.
  (*1-2*)
  simpl.
  induction (rev l2).
   (*1-2-1*)
   reflexivity.
   (*1-2-2*)
   induction ((a0 :: l) ++ a :: nil ).
    (*1-2-2-1*)
    reflexivity.
    (*1-2-2-2*)
    simpl.
    f_equal.
    apply IHl0.
 (*2*)
 simpl.
 rewrite IHl1.
 induction l2.
  (*2-1*)
  reflexivity.
  (*2-2*)
  simpl.
  induction (rev l2 ++ a0 :: nil).
   (*2-2-1*)
   reflexivity.
   (*2-2-2*)
   simpl.
   f_equal.
   apply IHl.
Qed.
    

今後

今はrev(rev l)=lの独立した証明を探しています。
帰納法でやるとrev(rev l) -> rev(rev l ++ a::nil)=a::l
は分かるのですが、rev_app_distrの証明と同じようにするために、
rev lについての帰納法ができないので苦戦中です。