- 作者: 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コードを読み込んだ後にお願いします。
まともにやってもうまくいかない。
色々と手を尽くしております。
(** Chapter5 何回も何回も何回も考えよう *) Require Import Recdef. (* Coq上で停止性をクリアするためにVariableを使う *) Variable meas_memb : forall xs : star, (SIZE (CDR xs) < SIZE xs)%coq_nat. Function memb (xs : star) {measure SIZE xs} : star := (_IF (ATOM xs) 'NIL (_IF (EQUAL (CAR xs) '?) 'T (memb (CDR xs)))). Proof. apply meas_memb. Defined. (* 尺度の証明 *) Theorem measure_memb (xs : star) : ~ ATOM xs -> (_IF (ATOM xs) 'T (_IF (EQUAL (CAR xs) '?) 'T (LT (SIZE (CDR xs)) (SIZE xs)))). Proof. move => H. rewrite (iffLR ifEP (size_cdr xs)). rewrite (equal_eq (if_same (EQUAL (CAR xs) '?) 'T)). rewrite (equal_eq (if_same (ATOM xs) 'T)). done. done. Qed. (* Coq上で停止性をクリアするためにVariableを使う *) Variable meas_remb : forall xs : star, (SIZE (CDR xs) < SIZE xs)%coq_nat. Function remb (xs : star) {measure SIZE xs} : star := (_IF (ATOM xs) '() (_IF (EQUAL (CAR xs) '?) (remb (CDR xs)) (CONS (CAR xs) (remb (CDR xs))))). Proof. apply meas_remb. Defined. (* 尺度の証明 *) Theorem measure_remb (xs : star) : ~ ATOM xs -> (_IF (ATOM xs) 'T (_IF (EQUAL (CAR xs) '?) (LT (SIZE (CDR xs)) (SIZE xs)) (LT (SIZE (CDR xs)) (SIZE xs)))). Proof. move => H. rewrite (equal_eq (if_same (EQUAL (CAR xs) '?) (LT (SIZE (CDR xs)) (SIZE xs)))). rewrite (iffLR ifEP (size_cdr xs)). rewrite (equal_eq (if_same (ATOM xs) 'T)). done. done. Qed. (* rembを展開するとremb_terminateになってしまう *) Theorem memb_remb0 : (EQUAL (memb (remb '())) 'NIL). Proof. rewrite /remb. rewrite /remb_terminate. Abort. Lemma atomB : (ATOM '()) = 'T. Proof. done. Qed. (* 書き換え用に公理を付け足す *) Variable membB : memb '() = (_IF (ATOM '()) 'NIL (_IF (EQUAL (CAR '()) '?) 'T (memb (CDR '())))). Variable rembB : remb '() = (_IF (ATOM '()) '() (_IF (EQUAL (CAR '()) '?) (remb (CDR '())) (CONS (CAR '()) (remb (CDR '()))))). (* 再チャレンジ *) Theorem memb_remb0_B : (EQUAL (memb (remb '())) 'NIL). Proof. rewrite rembB. rewrite atomB. rewrite (equal_eq (if_true '() (_IF (EQUAL (CAR '()) '?) (remb (CDR '())) (CONS (CAR '()) (remb (CDR '())))))). rewrite membB. rewrite atomB. rewrite (equal_eq (if_true 'NIL (_IF (EQUAL (CAR '()) '?) 'T (memb (CDR '()))))). rewrite (equal_same 'NIL). done. Qed. (* 書き換え用に公理を付け足す *) Variable x1 : star. Variable membC : memb (CONS x1 (remb '())) = (_IF (ATOM (CONS x1 (remb '()))) 'NIL (_IF (EQUAL (CAR (CONS x1 (remb '()))) '?) 'T (memb (CDR (CONS x1 (remb '())))))). Variable rembC : remb (CONS x1 '()) = (_IF (ATOM (CONS x1 '())) (CONS x1 '()) (_IF (EQUAL (CAR (CONS x1 '())) '?) (remb (CDR (CONS x1 '()))) (CONS (CAR (CONS x1 '())) (remb (CDR (CONS x1 '())))))). Theorem memb_remb1 : ~ EQUAL x1 '? -> EQUAL x1 '? -> (EQUAL (memb (remb (CONS x1 '()))) 'NIL). Proof. move => H0 H1. rewrite rembC. rewrite (equal_eq (atom_cons x1 '())). rewrite (equal_eq (if_false (CONS x1 '()) (_IF (EQUAL (CAR (CONS x1 '())) '?) (remb (CDR (CONS x1 '()))) (CONS (CAR (CONS x1 '())) (remb (CDR (CONS x1 '()))))))). rewrite (equal_eq (car_cons x1 '())). rewrite (equal_eq (cdr_cons x1 '())). (* --- ifの持ち上げ --- *) rewrite -(equal_eq (if_same (EQUAL x1 '?) (memb (_IF (EQUAL x1 '?) (remb '()) (CONS x1 (remb '())))) )). rewrite {1}(iffLR ifAP (if_nest_A (EQUAL x1 '?) (remb '()) (CONS x1 (remb '())) )). rewrite (iffLR ifEP (if_nest_E (EQUAL x1 '?) (remb '()) (CONS x1 (remb '())) )). (* --- ifの持ち上げ --- *) rewrite (equal_eq memb_remb0_B). rewrite membC. rewrite (equal_eq (atom_cons x1 (remb '()))). rewrite (equal_eq (if_false 'NIL (_IF (EQUAL (CAR (CONS x1 (remb '()))) '?) 'T (memb (CDR (CONS x1 (remb '()))))))). rewrite (equal_eq (car_cons x1 (remb '()))). rewrite (equal_eq (cdr_cons x1 (remb '()))). rewrite (iffLR ifEP (if_nest_E (EQUAL x1 '?) 'T (memb (remb '())) )). rewrite (equal_eq memb_remb0_B). rewrite (equal_eq (if_same (EQUAL x1 '?) 'NIL)). done. done. done. done. Qed. (* 書き換え用に公理を付け足す *) Variable x2 : star. Variable membD : memb (CONS x2 (remb (CONS x1 '()))) = (_IF (ATOM (CONS x2 (remb (CONS x1 '())))) 'NIL (_IF (EQUAL (CAR (CONS x2 (remb (CONS x1 '())))) '?) 'T (memb (CDR (CONS x2 (remb (CONS x1 '()))))))). Variable rembD : remb (CONS x2 (CONS x1 '())) = (_IF (ATOM (CONS x2 (CONS x1 '()))) (CONS x2 (CONS x1 '())) (_IF (EQUAL (CAR (CONS x2 (CONS x1 '()))) '?) (remb (CDR (CONS x2 (CONS x1 '())))) (CONS (CAR (CONS x2 (CONS x1 '()))) (remb (CDR (CONS x2 (CONS x1 '()))))))). Variable memb_remb1_D : (EQUAL (memb (remb (CONS x1 '()))) 'NIL). Theorem memb_remb2 : ~ EQUAL x2 '? -> EQUAL x2 '? -> (EQUAL (memb (remb (CONS x2 (CONS x1 '())))) 'NIL). Proof. move => H0 H1. rewrite rembD. rewrite (equal_eq (atom_cons x2 (CONS x1 '()))). rewrite (equal_eq (if_false (CONS x2 (CONS x1 '())) (_IF (EQUAL (CAR (CONS x2 (CONS x1 '()))) '?) (remb (CDR (CONS x2 (CONS x1 '())))) (CONS (CAR (CONS x2 (CONS x1 '()))) (remb (CDR (CONS x2 (CONS x1 '())))))))). rewrite (equal_eq (car_cons x2 (CONS x1 '()))). rewrite (equal_eq (cdr_cons x2 (CONS x1 '()))). (* --- ifの持ち上げ --- *) rewrite -(equal_eq (if_same (EQUAL x2 '?) (memb (_IF (EQUAL x2 '?) (remb (CONS x1 '())) (CONS x2 (remb (CONS x1 '()))))) )). rewrite {1}(iffLR ifAP (if_nest_A (EQUAL x2 '?) (remb (CONS x1 '())) (CONS x2 (remb (CONS x1 '()))) )). rewrite (iffLR ifEP (if_nest_E (EQUAL x2 '?) (remb (CONS x1 '())) (CONS x2 (remb (CONS x1 '()))) )). (* --- ifの持ち上げ --- *) rewrite (equal_eq memb_remb1_D). rewrite membD. rewrite (equal_eq (atom_cons x2 (remb (CONS x1 '())))). rewrite (equal_eq (if_false 'NIL (_IF (EQUAL (CAR (CONS x2 (remb (CONS x1 '())))) '?) 'T (memb (CDR (CONS x2 (remb (CONS x1 '())))))))). rewrite (equal_eq (car_cons x2 (remb (CONS x1 '())))). rewrite (equal_eq (cdr_cons x2 (remb (CONS x1 '())))). rewrite (iffLR ifEP (if_nest_E (EQUAL x2 '?) 'T (memb (remb (CONS x1 '()))) )). rewrite (equal_eq memb_remb1_D). rewrite (equal_eq (if_same (EQUAL x2 '?) 'NIL)). done. done. done. done. Qed.
