-
Notifications
You must be signed in to change notification settings - Fork 1
/
Section5.v
171 lines (134 loc) · 4.71 KB
/
Section5.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
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
Load Formulas.
Theorem T197a: Problem197aTrue. cbv. firstorder. Qed.
Theorem T198a: Problem198aFalse. cbv. firstorder.
destruct john_PN as [john person].
destruct former_A as [former]. firstorder. Qed.
Theorem FraCas199: Problem199aTrue. cbv. destruct successful_A as [successful]. destruct former_A as [former]. firstorder. (** FIXME: This is YES in the suite, but is says "yes for a former university student", which is not what the conclusion actually says. If we were to fix the conclusion then the example becomes trivial. **) Abort All. (**I suggest we do not bother with this example**)
Theorem FraCas200: Problem200aTrue. cbv. firstorder. destruct successful_A as [successful]. destruct former_A as [former]. firstorder. Abort All. (**UNK**)
Theorem FraCas200': Problem200aFalse. cbv. firstorder. destruct successful_A as [successful].
destruct former_A as [former]. firstorder. Abort All. (**UNK**)
Theorem FraCas201: Problem201aTrue. cbv. firstorder. destruct successful_A as [successful]. destruct former_A as [former]. firstorder. Abort All. (**UNK**)
Theorem FraCas201': Problem201aFalse. cbv. firstorder. destruct successful_A as [successful].
destruct former_A as [former]. firstorder. Abort All. (**UNK**)
Theorem FraCas202: Problem202aTrue. cbv. firstorder. Qed.
Theorem FraCas203: Problem203aTrue. cbv. firstorder. Qed.
Require Import Psatz.
Transparent PN2object.
Theorem FraCas204: Problem204aFalse.
cbv. intros.
assert (H' := small_and_large_opposite_K).
destruct small_A as [smallness smallThres].
destruct large_A as [largeness largeThres].
destruct (H' animal_N MICKEY) as [neg disj].
lia. Qed.
Theorem FraCas205: Problem205aFalse. cbv. intros.
cbv. intros.
assert (H' := small_and_large_opposite_K).
destruct small_A as [smallness smallThres].
destruct large_A as [largeness largeThres].
destruct (H' animal_N DUMBO) as [neg disj].
lia. Qed.
Theorem FraCas206: Problem206aTrue. cbv. intros. destruct small_A. destruct large_A. firstorder. Abort All. (* UNK *)
Theorem FraCas206': Problem206aFalse. cbv. intros. destruct small_A. destruct large_A. firstorder. Abort All. (* UNK *)
Theorem FraCas207: Problem207aTrue. cbv. intros. destruct small_A. destruct large_A. firstorder. Abort All. (* UNK *)
Theorem FraCas207': Problem207aFalse. cbv. intros. destruct small_A. destruct large_A. firstorder. Abort All. (* UNK *) (**206 and 207 are correctly captured, they are marked as UNK, but the score calculation counts them as wrong**)
Transparent PN2Class.
Theorem FraCas208: Problem208aTrue.
assert (slK := small_and_large_opposite_K).
cbv.
destruct small_A as [small].
destruct large_A as [large].
intros [[P1a P1b] [P2a P2]].
destruct (slK animal_N DUMBO) as [neg disj].
lia.
Qed.
Theorem T209: Problem209aFalse.
assert (slK := small_and_large_opposite_K).
cbv.
destruct small_A as [small].
destruct large_A as [large].
intros [[P1a P1b] [P2a P2]].
destruct (slK animal_N DUMBO) as [neg disj].
destruct (slK animal_N MICKEY) as [neg' disj'].
lia.
Qed.
Theorem FraCas210: Problem210aFalse. cbv. intros.
apply small_and_large_disjoint_K with (cn := animal_N) (o := MICKEY).
destruct small_A.
destruct large_A.
firstorder.
cbv.
firstorder.
cbv.
firstorder.
Qed.
Theorem FraCas211: Problem211aFalse.
cbv.
intros.
apply small_and_large_disjoint_K with (cn := animal_N) (o := DUMBO).
destruct small_A as [small].
destruct large_A as [large].
cbv.
firstorder.
Qed.
Theorem FraCas212: Problem212aTrue.
cbv.
assert (slK := small_and_large_opposite_K).
destruct small_A as [small smallThreshold].
destruct large_A as [large largeThreshold].
intros [P1 [P2 [[largeM mouse] [smallD eleph]]]].
destruct (slK animal_N DUMBO) as [neg disj].
destruct (slK animal_N MICKEY) as [neg' disj'].
destruct (P1 _ mouse) as [X Y].
destruct (P2 _ eleph) as [Z W].
lia.
Qed.
Theorem FraCas213: Problem213aTrue.
cbv.
destruct small_A as [small].
destruct large_A as [large].
intros.
firstorder.
Qed.
Theorem FraCas214: Problem214aTrue.
cbv.
intros.
destruct fat_A as [fat fatP].
firstorder.
Qed.
Theorem FraCas215: Problem215aTrue.
cbv.
intros P1 P2.
destruct competent_A as [competent].
firstorder.
(* UNK *)
Abort All.
(**Theorem FraCas216: Problem216aTrue.
cbv.
intros P1.
destruct fat_A as [fat fatP].
destruct bill_PN as [bill].
destruct john_PN as [john].
destruct than_Prep as [than].
firstorder.
(* FIXME: syntax wrong: should be
john is (fatter politician than bill)
not
(john is fatter politician) than bill
*)
Abort All.
Theorem FraCas217: Problem217aTrue.
cbv.
(* FIXME: syntax wrong, see 216 *)
Abort All.
*)
Theorem FraCas218: Problem218aTrue. cbv.
destruct kim_PN as [kim person].
destruct clever_A.
firstorder.
Qed.
Theorem FraCas219: Problem219aTrue. cbv.
destruct kim_PN as [kim person].
destruct clever_A.
firstorder.
Abort All. (* UNK *)