Software Foundations

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 H0.
Qed.
Print and_commut.
(*
and_commut = 
fun (P Q : Prop) (H : P /\ Q) =>
(fun H0 : Q /\ P => H0)
  match H with
  | conj H0 H1 => (fun (H2 : P) (H3 : Q) => conj Q P H3 H2) H0 H1
  end
     : forall P Q : Prop, P /\ Q -> Q /\ P
*)

作られた、証明オブジェクトがどうなってるのかというレベルで(どれが関数の引数で、本体で、というレベルで)良くわからん。

(fun H0 : Q /\ P => H0) は何だろう？

• Q/\P型の命題の証明を受け取ってそのまま返す関数
• その関数に、match式で作った、Q/\P型の命題の証明をそのまま渡す。

でいいのか？

また、コンテキストに、
P : Prop
H : P
のようにある場合、Pは命題。 Hは、命題Pの証明(根拠)。であってるんだっけ。大丈夫そうだな。

inversionではなく、destructを使用して証明すると、ずっとすっきりした証明オブジェクトが作られる。
こちらはなんとか分かる。気がする。

Theorem and_commut' : forall P Q : Prop,
  P /\ Q -> Q /\ P.
Proof.
  intros P Q H.
  destruct H.  
  apply conj. apply H0. apply H.
Qed.
(* これくらいなら、destructでも問題ない *)
Print and_commut'.
(*
and_commut' = 
fun (P Q : Prop) (H : P /\ Q) =>
match H with
| conj H0 H1 => conj Q P H1 H0
end
     : forall P Q : Prop, P /\ Q -> Q /\ P
*)