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で証明オブジェクトには変化がない。
よりプリミティブなものに置き換わったものに対して、定理や仮説を適用していくイメージか。そのへんの匙加減は、定理や仮説の形とかによるのだろうか。

しかし、今書いてるものが、命題なのか、命題に対する証明なのか、未だに混乱するときがある。