どれが型で、値で、という区別。 どれが命題で、証明で、という区別。 慣れるしかないとはいえつらい。しばしば出て来る数学用語についても、もう少し知っておく必要がある。直積、関係、反射的、推移的、対称的、etc...学がないとつらいね。SoftwareFoundat…

Logic.v証明オブジェクトが良くわからん。論理積の交換で、Logic.vに載ってるやり方だと以下のような証明オブジェクトが作られる。 Theorem and_commut : forall P Q : Prop, P /\ Q -> Q /\ P. Proof. intros P Q H. inversion H. split. apply H1. apply H…