-
Notifications
You must be signed in to change notification settings - Fork 0
/
ex01.v
113 lines (87 loc) · 1.51 KB
/
ex01.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
(* Problem 0-2 *)
Theorem tautology : forall P : Prop, P -> P.
Proof.
intros P H.
assumption.
Qed.
(*
Theorem wrong : forall P : Prop, P.
Proof.
intros P.
Qed.
Error: Attempt to save an incomplete proof
*)
(* Problem 1 *)
Theorem Modus_ponens : forall P Q : Prop, P -> (P -> Q) -> Q.
Proof.
intro.
intro.
intro.
intro.
apply H0.
apply H.
Qed.
(* Problem 2 *)
Theorem Modus_tollens : forall P Q : Prop, ~Q /\ (P -> Q) -> ~P.
Proof.
intros.
destruct H.
intro.
apply H0 in H1.
apply H in H1.
apply H1.
Qed.
(* Problem 3 *)
Theorem Disjunctive_syllogism : forall P Q : Prop, (P \/ Q) -> ~P -> Q.
Proof.
intros.
destruct H.
apply H0 in H.
destruct H.
apply H.
Qed.
(* Problem 4 *)
Theorem DeMorgan1 : forall P Q : Prop, ~P \/ ~Q -> ~(P /\ Q).
Proof.
intros.
intro.
destruct H as [HA | HB].
destruct H0 as [H0A H0B].
apply HA in H0A. apply H0A.
destruct H0 as [H0A H0B].
apply HB in H0B. apply H0B.
Qed.
Theorem DeMorgan2 : forall P Q : Prop, ~P /\ ~Q -> ~(P \/ Q).
Proof.
intros.
intro.
destruct H0 as [H0A | H0B].
destruct H as [HA HB].
apply HA in H0A. apply H0A.
destruct H as [HA HB].
apply HB in H0B. apply H0B.
Qed.
Theorem DeMorgan3 : forall P Q : Prop, ~(P \/ Q) -> ~P /\ ~Q.
Proof.
intros.
apply conj.
intro.
apply H.
left. apply H0.
intro.
apply H.
right.
apply H0.
Qed.
(* Problem 5 *)
Theorem NotNot_LEM : forall P : Prop, ~ ~(P \/ ~P).
Proof.
intros.
intro.
apply H.
right.
intro.
apply H.
left.
apply H0.
Qed.