-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathC1_ex2.v
139 lines (106 loc) · 1.99 KB
/
C1_ex2.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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
Parameter it_is_raining : Prop.
Parameters P Q R T : Prop.
Check P.
Check P -> Q.
Check P /\ Q.
Check P \/ Q.
Check ~ P.
Check P <-> Q.
Lemma imp_dist : (P -> Q -> R) -> (P -> Q) -> P -> R.
Proof.
intros H1 H2 H3.
apply H1.
assumption.
apply H2; assumption.
Qed.
Print imp_dist.
Definition imp_trans : (P -> Q) -> (Q -> R) -> (P -> R) := fun H1 H2 H3 => H2 (H1 H3).
Goal P /\ Q -> P.
Proof.
intros H.
destruct H as [ H1 ? ].
exact H1.
Qed.
Fact conj_comm : P /\ Q -> Q /\ P.
Proof.
intros [ ]; split; trivial.
Qed.
Fact conj_comm' : P /\ Q -> Q /\ P.
Proof.
intros H; split; destruct H; trivial.
Qed.
Fact conj_comm'' : P /\ Q -> Q /\ P.
Proof.
intros H.
destruct H as [ H1 H2 ].
split; assumption.
Qed.
Fact conj_comm''' : P /\ Q -> Q /\ P.
Proof.
intros H.
destruct H as [ H1 H2 ].
split; [ assumption | trivial ].
Qed.
Section assert.
Hypothesis (H : P -> Q)
(H0 : Q -> R)
(H1 : (P -> R) -> T -> Q)
(H2 : (P -> R) -> T).
Lemma L8 : Q.
Proof.
assert (H3 : P -> R).
+ intros H3.
apply H0.
apply H.
apply H3.
+ apply H1.
* trivial.
* apply H2.
trivial.
Qed.
End assert.
Section Ex5.
Hypothesis (H : T -> R -> (P \/ Q))
(H0 : ~ (R /\ Q))
(H1 : T).
Lemma R5 : R -> P.
Proof.
intros H2.
destruct H as [ G1 | G2 ]; trivial.
destruct H0.
split; assumption.
Qed.
End Ex5.
Lemma L2 : (P \/ Q) /\ ~P -> Q.
Proof.
intros [ [ H1 | H1 ] H2 ]; [ destruct H2 | ]; assumption.
Qed.
Print conj_comm.
Print conj_comm'.
Fact disj_comm : P \/ Q -> Q \/ P.
Proof.
intros H.
destruct H as [ H1 | H2 ].
right; trivial.
left; trivial.
Qed.
Print disj_comm.
Fact absurd_1 : False -> False.
Proof.
intros H.
exact H.
Qed.
Fact absurd_2 : False -> False.
Proof.
intros H.
destruct H.
Qed.
Print absurd_1.
Print absurd_2.
Fact absurd_3 : ~ False.
Proof.
intros [].
Qed.
exact H1.
destruct H as [ H1 H2 ].
exact H1.