Software Foundations
ProofObject.v
これこそが知りたかったことだけど、すでに前の版で大半は日本語訳されてた。例とかは少ないけど。
以前読んだときは目に入ってなかったのか、理解出来てなかっただけか、両方か。
しかし、Printとかの使い方はなかった気もする。
Theorem b_times2PO: forall n, beautiful n -> beautiful (2*n). Proof. Show Proof. intros n H. Show Proof. (* (fun (n : nat) (H : beautiful n) => ?117) *) simpl. Show Proof. (* (fun (n : nat) (H : beautiful n) => ?118) *) apply b_sum. Show Proof. (* (fun (n : nat) (H : beautiful n) => b_sum n (n + 0) ?119 ?120) *) apply H. Show Proof. (* (fun (n : nat) (H : beautiful n) => b_sum n (n + 0) H ?120) *) apply b_sum. Show Proof. (* (fun (n : nat) (H : beautiful n) => b_sum n (n + 0) H (b_sum n 0 ?121 ?122)) *) apply H. Show Proof. (* (fun (n : nat) (H : beautiful n) => b_sum n (n + 0) H (b_sum n 0 H ?122)) *) apply b_0. Show Proof. (* (fun (n : nat) (H : beautiful n) => b_sum n (n + 0) H (b_sum n 0 H b_0)) *) Qed.
simplで証明オブジェクトには変化がない。
よりプリミティブなものに置き換わったものに対して、定理や仮説を適用していくイメージか。そのへんの匙加減は、定理や仮説の形とかによるのだろうか。
しかし、今書いてるものが、命題なのか、命題に対する証明なのか、未だに混乱するときがある。