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

定理証明手習い

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

「The Little Prover」のCoqでの実現

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

(** Chapter2 もう少し、いつものゲームを *)

Notation "'or" := (S_ATOM (ATOM_SYM "or")).
Notation "'black" := (S_ATOM (ATOM_SYM "black")).
Notation "'(coffee)" := (S_ATOM (ATOM_SYM "(coffee)")).
Theorem chapter2_example1 (a b c:star):
  (_IF (CAR (CONS a b)) c c).
Proof.
  rewrite (equal_eq (car_cons a b)).
  rewrite (equal_eq (if_same a c)).
  rewrite -(equal_eq (if_same
    (_IF (EQUAL a 'T) (_IF (EQUAL 'NIL 'NIL) a b) (EQUAL 'or (CONS 'black '(coffee))))
    c
  )).
  rewrite equal_same2.
  rewrite (equal_eq (if_true a b)).
  rewrite {2}(iffLR ifAP (equal_if a 'T)).
Abort.

Notation "'hominy" := (S_ATOM (ATOM_SYM "hominy")).
Notation "'grits" := (S_ATOM (ATOM_SYM "grits")).
Notation "'(hash browns)" := (S_ATOM (ATOM_SYM "(hash browns)")).
Notation "'ketchup" := (S_ATOM (ATOM_SYM "ketchup")).
Notation "'mustard" := (S_ATOM (ATOM_SYM "mustard")).
Theorem chapter2_example2 (a:star):
  (_IF (ATOM (CAR a))
         (_IF (EQUAL (CAR a) (CDR a)) 'hominy 'grits)
         (_IF (EQUAL (CDR (CAR a)) '(hash browns))
             (CONS 'ketchup (CAR a))
             (CONS 'mustard (CAR a)))).
Proof.
  rewrite -{4}(iffLR ifEP (cons_car_cdr (CAR a))).
  rewrite -{1}(iffLR ifAP (equal_if (CDR (CAR a)) '(hash browns))).
Abort.

Notation "'statement" := (S_ATOM (ATOM_SYM "statement")).
Notation "'question" := (S_ATOM (ATOM_SYM "question")).
Notation "'(answer)" := (S_ATOM (ATOM_SYM "(answer)")).
Notation "'(else)" := (S_ATOM (ATOM_SYM "(else)")).
Notation "'(other answer)" := (S_ATOM (ATOM_SYM "(other answer)")).
Notation "'(other else)" := (S_ATOM (ATOM_SYM "(other else)")).
Theorem chapter2_example3 (a n:star):
  (CONS 'statement
    (CONS (_IF (EQUAL a 'question) (CONS n '(answer)) (CONS n '(else)))
      (_IF (EQUAL a 'question) (CONS n '(other answer)) (CONS n '(other else))))).
Proof.
  rewrite -(equal_eq (if_same
    (EQUAL a 'question)
    (CONS (_IF (EQUAL a 'question) (CONS n '(answer)) (CONS n '(else)))
          (_IF (EQUAL a 'question) (CONS n '(other answer)) (CONS n '(other else))))
  )).
  rewrite {1}(iffLR ifAP (if_nest_A
    (EQUAL a 'question)
    (CONS n '(answer))
    (CONS n '(else))
  )).
  rewrite {1}(iffLR ifEP (if_nest_E
    (EQUAL a 'question)
    (CONS n '(answer))
    (CONS n '(else))
  )).
  rewrite {1}(iffLR ifAP (if_nest_A
    (EQUAL a 'question)
    (CONS n '(other answer))
    (CONS n '(other else))
  )).
  rewrite {1}(iffLR ifEP (if_nest_E
    (EQUAL a 'question)
    (CONS n '(other answer))
    (CONS n '(other else))
  )).
Abort.