■

Logic.v

証明オブジェクトがどんなかたちになるかについて、
全然イメージが湧かない。
あいかわらずレバガチャ状態ではある。

Theorem or_distributes_over_and_2 : forall P Q R : Prop,
(P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R).

とか。

scriptモードでも、一度泥沼に嵌ると抜けだせないし。

3 subgoals, subgoal 1 (ID 1231)
  
  P : Prop
  Q : Prop
  R : Prop
  H : (P \/ Q) /\ (P \/ R)
  H0 : P \/ Q
  H1 : P \/ R
  H2 : P
  H3 : R
  ============================
   Q
...

Theorem or_distributes_over_and_2 : forall P Q R : Prop,
(P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R).
 intros P Q R H.
 inversion H.
 inversion H0.
 inversion H1.
 left. apply H2. right. split.

 (* あれ？ Q？ *)

Theorem or_commut : forall P Q : Prop,
P \/ Q -> Q \/ P.
Proof.
intros P Q H.
inversion H as [HP|HQ].
right. apply HP.
left. apply HQ.
Qed.
Theorem or_commut' : forall P Q : Prop,
P \/ Q -> Q \/ P.
Proof.
intros P Q H.
destruct H as [HP | HQ] eqn:H' .
right. apply HP.
left. apply HQ.
Qed.

Print or_commut.
(*
or_commut =
fun (P Q : Prop) (H : P \/ Q) =>
(fun H0 : Q \/ P => H0)
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
: forall P Q : Prop, P \/ Q -> Q \/ P
*)
 
Print or_commut'.
(*
or_commut' =
fun (P Q : Prop) (H : P \/ Q) =>
let o := H in
let H' := eq_refl in
match o as o0 return (H = o0 -> Q \/ P) with
| or_introl HP => fun _ : H = or_introl P Q HP => or_intror Q P HP
| or_intror HQ => fun _ : H = or_intror P Q HQ => or_introl Q P HQ
end H'
: forall P Q : Prop, P \/ Q -> Q \/ P
 
*)

論理和の場合は、
destructよりinversion使ったほうが簡単になるな。

あと、Software Foundationsの Caseって

destructなどで必要となる根拠にたいし、()でくるんで、
その中で一時文字列変数を宣言してるだけなのね。