今日のCoq

自分が理解したであろうところの証明オブジェクトの書き方。

XXX -> YYY :=
fun (H :  XXX) =>
 (fun (H1 : YYY) => H1)    （← ここで YYY型の変数H1を返す関数を生成してそのまま実行。
  ... YYY型の変数 を組み立てる何かの処理 ...  ←上の行の関数の実行に対して渡している H1をここで生成。

例

Definition or_ommut_def : forall P Q : Prop,
  P \/ Q -> Q \/ P :=
 fun (P Q : Prop) =>
  fun (H : P \/ Q) =>
   (fun (H' : Q \/ P) => H')
    match H with 
     | or_introl HP => (fun (HP0 : P) => or_intror Q P HP0) HP
     | or_intror HQ => (fun (HQ0 : Q) => or_introl Q P HQ0) HQ
    end.

やはり単なる関数に過ぎない。

バックスラッシュが円記号になるフォントやだー

---

論理積、論理和の命題のタクティック使用方針。

• conj、iff (/\ ,<->)

splitを使用する。

• or (\/)

left,right（apply or_intro[rl]）を使用する。

バックスラッシュが円記号になるフォントやだー
firefoxはフォント全部rictyに変えたらバックスラッシュが表示された。
Chromiumだめだ。変わらん。