Last active
August 29, 2015 14:02
-
-
Save yuga/a4e8895b60128e3d3221 to your computer and use it in GitHub Desktop.
Logic_J.vより抜粋。tacticを使わずに証明オブジェクトを手書きするのを試しているけど僕には難しい。
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(* **** Exercise: 1 star (bool_prop) *) | |
(** **** 練習問題: ★ (bool_prop) *) | |
Theorem andb_false : forall b c, | |
andb b c = false -> b = false \/ c = false. | |
Proof. | |
intros b c H. | |
unfold andb in H. | |
destruct b. | |
right. apply H. | |
left. reflexivity. | |
Qed. | |
Definition andb_false' : forall b c, | |
andb b c = false -> b = false \/ c = false := | |
fun b c H => | |
match | |
b | |
return | |
(match b with | |
| true => c | |
| false => false | |
end = false -> b = false \/ c = false) | |
with | |
| true => fun H0 : c = false => or_intror (true = false) (c = false) H0 | |
| false => fun _ : false = false => or_introl (false = false) (c = false) eq_refl | |
end H. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Theorem or_distributes_over_and_1 : forall P Q R : Prop, | |
P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R). | |
Proof. | |
intros P Q R. intros H. inversion H as [HP | [HQ HR]]. | |
Case "left". split. | |
SCase "left". left. apply HP. | |
SCase "right". left. apply HP. | |
Case "right". split. | |
SCase "left". right. apply HQ. | |
SCase "right". right. apply HR. Qed. | |
Definition or_distributes_over_and_1' : forall (P Q R : Prop), | |
P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R) := | |
fun P Q R H => | |
match H with | |
| or_introl HP => | |
conj (P \/ Q) (P \/ R) (or_introl P Q HP) (or_introl P R HP) | |
| or_intror HQR => | |
match HQR with | |
| conj HQ HR => | |
conj (P \/ Q) (P \/ R) (or_intror P Q HQ) (or_intror P R HR) | |
end | |
end. | |
(* and_ind : forall P Q P0 : Prop, (P -> Q -> P0) -> and P Q -> P0. *) | |
(* **** Exercise: 2 stars, recommended (or_distributes_over_and_2) *) | |
(** **** 練習問題: ★★, recommended (or_distributes_over_and_2) *) | |
Theorem or_distributes_over_and_2 : forall P Q R : Prop, | |
(P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R). | |
Proof. | |
intros P Q R. intros H. | |
inversion H as [ [HP0 | HQ] [HP1 | HR] ]. | |
left. apply HP0. (* HP0 HP1, P *) | |
left. apply HP0. (* HP0 HR, P *) | |
left. apply HP1. (* HQ HP1, P *) | |
right. split. (* HQ HR, Q /\ R *) | |
apply HQ. (* HQ HR, Q *) | |
apply HR. (* HQ HR, R *) | |
Qed. | |
Definition or_distributes_over_and_2' : forall (P Q R : Prop), | |
(P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R) := | |
fun P Q R H => | |
match H with | |
| conj HPQ HPR' => | |
match HPQ with | |
| or_introl HP0 => | |
fun HPR : P \/ R => | |
match HPR with | |
| or_introl HP1 => or_introl P (Q /\ R) HP0 | |
| or_intror HR => or_introl P (Q /\ R) HP0 | |
end | |
(* fun _ : P \/ R => or_introl P (Q /\ R) HP0 *) | |
| or_intror HQ => | |
fun HPR : P \/ R => | |
match HPR with | |
| or_introl HP1 => or_introl P (Q /\ R) HP1 | |
| or_intror HR => or_intror P (Q /\ R) (conj Q R HQ HR) | |
end | |
end HPR' | |
end. | |
Definition or_distributes_over_and_2'' : forall (P Q R : Prop), | |
(P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R) := | |
fun P Q R H => | |
match H with | |
| conj HPQ HPR => | |
match HPQ with | |
| or_introl HP0 => or_introl P (Q /\ R) HP0 | |
| or_intror HQ => | |
match HPR with | |
| or_introl HP1 => or_introl P (Q /\ R) HP1 | |
| or_intror HR => or_intror P (Q /\ R) (conj Q R HQ HR) | |
end | |
end | |
end. | |
(** [] *) | |
(* **** Exercise: 1 star (or_distributes_over_and) *) | |
(** **** 練習問題: ★ (or_distributes_over_and) *) | |
Theorem or_distributes_over_and : forall P Q R : Prop, | |
P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R). | |
Proof. | |
intros P Q R. | |
split. | |
apply or_distributes_over_and_1'. | |
apply or_distributes_over_and_2''. | |
Qed. | |
Definition or_distributes_over_and' : forall P Q R, | |
P \/ (Q /\ R) <-> (P \/ Q) /\ (P \/ R) := | |
fun P Q R => | |
conj (P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R)) | |
((P \/ Q) /\ (P \/ R) -> P \/ (Q /\ R)) | |
(or_distributes_over_and_1' P Q R) | |
(or_distributes_over_and_2' P Q R). | |
(** [] *) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment