- 作者: Daniel P. Friedman,Carl Eastlund,中野圭介
- 出版社/メーカー: ラムダノート
- 発売日: 2017/10/23
- メディア: 単行本(ソフトカバー)
- この商品を含むブログ (7件) を見る
@suharahiromichi
「The Little Prover」のCoqでの実現
この文書のソースコードは以下にあります。
https://github.com/suharahiromichi/coq/blob/master/lisp/tlp_lisp_3.v
以下のコードを実行するときは、氏のCoqコードを読み込んだ後にお願いします。
リスト型帰納法による証明をおこなう。
(** Chapter6 最後まで考え抜くのです *) (* 書き換え用に公理を付け足す *) Variable xs : star. Variable membE : memb (CONS (CAR xs) (remb (CDR xs))) = (_IF (ATOM (CONS (CAR xs) (remb (CDR xs)))) 'NIL (_IF (EQUAL (CAR (CONS (CAR xs) (remb (CDR xs)))) '?) 'T (memb (CDR (CONS (CAR xs) (remb (CDR xs))))))). Variable rembE : remb xs = (_IF (ATOM xs) '() (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs))))). Variable EQA : (EQUAL 'NIL 'NIL) = 'T. Theorem memb_remb : ~ ATOM xs -> ATOM xs -> ~ (EQUAL (CAR xs) '?) -> (EQUAL (CAR xs) '?) -> (EQUAL (memb (remb (CDR xs))) 'NIL) -> (_IF (ATOM xs) (EQUAL (memb (remb xs)) 'NIL) (_IF (EQUAL (memb (remb (CDR xs))) 'NIL) (EQUAL (memb (remb xs)) 'NIL) 'T)). Proof. move => H0 H1 H2 H3 H4. rewrite rembE. rewrite {1}(iffLR ifAP (if_nest_A (ATOM xs) '() (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs)))) )). rewrite membB. rewrite atomB. rewrite (equal_eq (if_true 'NIL (_IF (EQUAL (CAR '()) '?) 'T (memb (CDR '()))))). rewrite EQA. (* rewrite rembE. *) rewrite (iffLR ifEP (if_nest_E (ATOM xs) '() (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs)))) )). (* --- ifの持ち上げ --- *) rewrite -(equal_eq (if_same (EQUAL (CAR xs) '?) (memb (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs))))) )). rewrite {1}(iffLR ifAP (if_nest_A (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs))) )). rewrite (iffLR ifEP (if_nest_E (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs))) )). (* --- ifの持ち上げ --- *) rewrite {2}(iffLR ifAP (equal_if (memb (remb (CDR xs))) 'NIL)). rewrite membE. rewrite (equal_eq (atom_cons (CAR xs) (remb (CDR xs)))). rewrite (equal_eq (if_false 'NIL (_IF (EQUAL (CAR (CONS (CAR xs) (remb (CDR xs)))) '?) 'T (memb (CDR (CONS (CAR xs) (remb (CDR xs)))))))). rewrite (equal_eq (car_cons (CAR xs) (remb (CDR xs )))). rewrite (equal_eq (cdr_cons (CAR xs) (remb (CDR xs )))). rewrite (iffLR ifEP (if_nest_E (EQUAL (CAR xs) '?) 'T (memb (remb (CDR xs))) )). rewrite {2}(iffLR ifAP (equal_if (memb (remb (CDR xs))) 'NIL)). rewrite (equal_eq (if_same (EQUAL (CAR xs) '?) 'NIL)). rewrite EQA. rewrite (equal_eq (if_same (EQUAL (memb (remb (CDR xs))) 'NIL) 'T)). rewrite (equal_eq (if_same (ATOM xs) 'T)). done. done. done. done. done. done. done. done. Qed.