名古屋Scala 懇親会に(のみ)行ってきた

Coq

所謂一つのKOM ですね．

  • Scala は，ScalaCheck があっていいね．
    • Java には，why があるよ．
      • ネットが繋がらない．懇親会会場--
      • で，Coq の次の一手なんですが．

ということで id:yoshihiro503 の人が居たので，Coq の次の一手(ProofGeneral の後) を聞いてみた．

以下が聞いたこと．Theorem とかはなんとなく書けるとする．

これだけは覚えとけタクティック

  • intros // goal が forall だったときに使う．forall は カンマまで．仮定を取り出す
  • induction // 〜に関する帰納法を開始する
  • simpl // 1step 簡約する．(simple ではないのが萌え．．．ません)
  • reflexivity // goal に自明な等式があったとき式を閉じる
  • rewrite // 式に仮定があったときに置き換える

普通の再帰の証明の流れは，こんな感じのテンプレ？

intros ???. (* 仮定を明かにする *)
induction ???. (* 帰納法開始 *)
  simpl.
  reflexivity. (* 自明な方は大抵すぐにできる *)

  simpl.
  rewrite ???. (* 帰納法の仮定とか他の物を持ってくる *)
  reflexivity.
Qed.

ということで，reverse (reverse xs) = xs を書いてみた．
append_assoc の部分は Proof Cafe. でやるとして．
もっといいやり方があると思うのでそのときに聞こう．

Fixpoint reverse {A : Type} (xs : list A) : list A :=
  match xs with
    | nil => nil
    | cons x xs => reverse xs ++ (cons x nil)
  end.

Theorem append_with_nil : forall (A : Type) (xs : list A),
  xs ++ nil = xs.
Proof.
  intros A xs.
  induction xs.
    simpl.
    reflexivity.

    simpl.
    rewrite IHxs.
    reflexivity.
Qed.

Theorem reverse_append_dist : forall (A : Type) (xs ys : list A),
  reverse (xs ++ ys) = (reverse ys) ++ (reverse xs).
Proof.
  intros A xs ys.
  induction xs.
    simpl.
    rewrite append_with_nil.
    reflexivity.

    simpl.
    rewrite IHxs.
    rewrite append_assoc.
    reflexivity.
Qed.

Theorem reverse_reverse_id : forall (A : Type) (xs : list A),
  reverse (reverse xs) = xs.
Proof.
  intros A xs.
  induction xs.
    simpl.
    reflexivity.

    simpl.
    rewrite reverse_append_dist.
    rewrite IHxs.
    simpl.
    reflexivity.
Qed.

下のも一回見た気がするんだけど，やっぱり人に聴くとわかった気になった．

参考