読者です 読者をやめる 読者になる 読者になる

それわかるぅ〜

日々「それわかるぅ〜」と思ったこと、忘れたくないことを徒然なるままに。Inputした情報を定着させるためのOutputの場として使用しています。誤字脱字等はたぶん仕様です。

false_beq_nat (ソフトウェアの基礎、Coq)のメモ

プログラミング関係

Coqの帰納法を忘れかけてたのでメモ

(** **** Exercise: 2 stars (false_beq_nat)  *)
Theorem false_beq_nat : forall n m : nat,
     n <> m ->
     beq_nat n m = false.
Proof.
  intros n.
  unfold not.
  induction n as [ | n'].
    - intros m H (**ここでmをintros**). destruct m as [ | n'].
                 * apply ex_falso_quodlibet. apply H. reflexivity.
                 * simpl. reflexivity.
    - intros m H (**ここでmをintros**). destruct m as [ | m'].
                 * simpl. reflexivity.
                 * simpl. apply IHn'. intros H1. apply H. rewrite -> H1. reflexivity. Qed.