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

定理証明手習い

この本を練習しようと思った。
Schemeでやるのはつらいな〜と思っていたら、Coqで出来るようにした記事があった。

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

「The Little Prover」のCoqでの実現

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

(** Chapter 1 いつものゲームに新しいルールを *)

Notation "'ham" := (S_ATOM (ATOM_SYM "ham")).
Notation "'eggs" := (S_ATOM (ATOM_SYM "eggs")).
Theorem chapter1_example1:
  (EQUAL (CAR (CONS 'ham 'eggs)) 'ham).
Proof.
  apply car_cons.
Qed.

Notation "'()" := (S_ATOM (ATOM_SYM "()")).
Theorem chapter1_example2:
  (ATOM '()).
Proof.
  done.
Qed.

Theorem chapter1_example3:
  (EQUAL (ATOM (CONS 'ham 'eggs)) 'NIL).
Proof.
  apply atom_cons.
Qed.

Theorem chapter1_example4 (a b:star):
  (EQUAL (ATOM (CONS a b)) 'NIL).
Proof.
  apply atom_cons.
Qed.

Notation "'flapjack" := (S_ATOM (ATOM_SYM "flapjack")).
Theorem chapter1_example5 (a b:star):
  (EQUAL (EQUAL 'flapjack (ATOM (CONS a b))) 'NIL).
Proof.
  apply (atom_cons a b).
Qed.

Theorem chapter1_example6_7 (p q:star):
  (ATOM (CDR (CONS (CAR (CONS p q)) '()))).
Proof.
  rewrite (equal_eq (car_cons p q)).
  rewrite (equal_eq (cdr_cons p '())).
  done.
Qed.

Theorem equal_same2 (x : star) :
  (EQUAL x x) = 'T.
Proof.
  rewrite /EQUAL.
    by rewrite refl_eqStar.
Qed.
Notation "'(and crumpets)" := (S_ATOM (ATOM_SYM "(and crumpets)")).
Theorem chapter1_example8 (x y:star):
  (CAR (CONS (EQUAL (CONS x y) (CONS x y)) '(and crumpets))) = 'T.
Proof.
  rewrite equal_same2.
  rewrite (equal_eq (car_cons 'T '(and crumpets))).
  done.
Qed.

Notation "'bagels" := (S_ATOM (ATOM_SYM "bagels")).
Notation "'(and lox)" := (S_ATOM (ATOM_SYM "(and lox)")).
Theorem chapter1_example9 (x y:star):
  (EQUAL (CONS x y) (CONS 'bagels '(and lox))).
Proof.
  rewrite (equal_eq (equal_swap (CONS x y) (CONS 'bagels '(and lox)))).
Abort.

Theorem chapter1_example10 (x y:star):
  (CONS y (EQUAL (CAR (CONS (CDR x) (CAR y))) (EQUAL (ATOM x) 'NIL))).
Proof.
  rewrite (equal_eq (car_cons (CDR x) (CAR y))).
Abort.

Notation "'(oats)" := (S_ATOM (ATOM_SYM "(oats)")).
Theorem chapter1_example11 (x y z:star):
  (CONS y (EQUAL (CAR (CONS (CDR x) (CAR y))) (EQUAL (ATOM x) 'NIL))).
Proof.
  rewrite -(equal_eq (car_cons (CAR (CONS (CDR x) (CAR y))) '(oats))).
  rewrite -(equal_eq (atom_cons (ATOM (CDR (CONS x y))) (EQUAL (CONS x y) z))).
  rewrite (equal_eq (cdr_cons x y)).
  rewrite (equal_eq (equal_swap (CONS x y) z)).
Abort.

Theorem chapter1_example12 (x y:star):
  (ATOM (CAR (CONS (CAR x) (CDR y)))).
Proof.
  rewrite (equal_eq (car_cons (CAR x) (CDR y))).
Abort.