定理証明手習いをCoqで 第3章

定理証明手習い

@suharahiromichi
この文書のソースコードは以下にあります。
https://github.com/suharahiromichi/coq/blob/master/lisp/tlp_lisp_3.v

「The Little Prover」のCoqでの実現

以下のコードを実行するときは、氏のCoqコードを読み込んだ後にお願いします。

本格的な証明に入る。

(** Chapter3 名前に何が？ *)

Definition PAIR (x y: star) : star :=
  (CONS x (CONS y '())).
Definition FIRST_OF (x: star) : star :=
  (CAR x).
Definition SECOND_OF (x: star) : star :=
  (CAR (CDR x)).
Theorem first_of_pair (a b:star):
  (EQUAL (FIRST_OF (PAIR a b)) a).
Proof.
  rewrite /PAIR.
  rewrite /FIRST_OF.
  rewrite (equal_eq (car_cons a (CONS b '()))).
  rewrite equal_same.
  done.
Qed.

Theorem second_of_pair (a b:star):
  (EQUAL (SECOND_OF (PAIR a b)) b).
Proof.
  rewrite /PAIR.
  rewrite /SECOND_OF.
  rewrite (equal_eq (cdr_cons a (CONS b '()))).
  rewrite (equal_eq (car_cons b '())).
  by rewrite equal_same.
Qed.

Definition IN_PAIR (xs: star) : star :=
  (_IF (EQUAL (FIRST_OF xs) '?)
    'T
    (EQUAL (SECOND_OF xs) '?)).
Theorem in_first_of_pair (b:star):
  (EQUAL (IN_PAIR (PAIR '? b)) 'T).
Proof.
  rewrite /PAIR.
  rewrite /IN_PAIR.
  rewrite /FIRST_OF.
  rewrite (equal_eq (car_cons '? (CONS b '()))).
  rewrite equal_same2.
  rewrite (equal_eq (if_true 'T (EQUAL (SECOND_OF (CONS '? (CONS b '()))) '?))).
  by rewrite equal_same.
Qed.

Theorem in_second_of_pair (a:star):
  (EQUAL (IN_PAIR (PAIR a '?)) 'T).
Proof.
  rewrite /PAIR.
  rewrite /IN_PAIR.
  (* rewrite /FIRST_OF.
  rewrite (equal_eq (car_cons a (CONS '? '()))). *)
  rewrite /SECOND_OF.
  rewrite (equal_eq (cdr_cons a (CONS '? '()))).
  rewrite (equal_eq (car_cons '? '())).
  rewrite equal_same2.
  rewrite (equal_eq (if_same (EQUAL (FIRST_OF (CONS a (CONS '? '()))) '?) 'T)).
  by rewrite equal_same.
Qed.