Schedule/ProofCafe_25

• 11/24 Schedule/ProofCafe_25
• 時間: 14:30 - 17:30
• 場所: 名古屋大学 多元数理科学棟(旧理学部1号館) 409
• 参加登録: PARTAKE: ProofCafe
• ソフトウェアの基礎の命題と論拠の最初から
• ドキュメントはCoqソースコードから自動生成されています。ソースコード全体はこちら: http://proofcafe.org/sf/sfja.tar.gz

加者 6人

練習問題: ★★ (not_eq_beq_false)

Require Import Arith.

Theorem not_eq_beq_false : forall n n' : nat,
     n <> n' ->
     beq_nat n n' = false.
Proof.
  induction n; destruct n'; simpl; intros; try reflexivity.
  induction H; reflexivity.
  apply IHn.
  intro H'; rewrite H' in *; apply H.
  reflexivity.
Qed.