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
|
Coq <
Coq < Coq < 1 goal
============================
forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
(dependent evars: ; in current goal:)
strange_imp_trans <
strange_imp_trans < No more goals.
(dependent evars: ; in current goal:)
strange_imp_trans <
Coq < Coq < 1 goal
============================
forall P Q : Prop, (P -> Q) /\ P -> Q
(dependent evars: ; in current goal:)
modpon <
modpon < No more goals.
(dependent evars: ; in current goal:)
modpon <
Coq < Coq <
Coq < P1 is declared
P2 is declared
P3 is declared
P4 is declared
Coq < p12 is declared
Coq < p123 is declared
Coq < p34 is declared
Coq < Coq < 1 goal
P1, P2, P3, P4 : Prop
p12 : P1 -> P2
p123 : (P1 -> P2) -> P3
p34 : P3 -> P4
============================
P4
(dependent evars: ; in current goal:)
p14 <
p14 < Second proof:
p14 < 4 focused goals
(shelved: 2)
P1, P2, P3, P4 : Prop
p12 : P1 -> P2
p123 : (P1 -> P2) -> P3
p34 : P3 -> P4
============================
?Q -> P4
goal 2 is:
?P -> ?Q
goal 3 is:
?P -> ?Q
goal 4 is:
?P
(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
p14 < 1 focused goal
(shelved: 2)
P1, P2, P3, P4 : Prop
p12 : P1 -> P2
p123 : (P1 -> P2) -> P3
p34 : P3 -> P4
============================
?Q -> P4
(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
p14 < This subproof is complete, but there are some unfocused goals.
Try unfocusing with "}".
3 goals
(shelved: 2)
goal 1 is:
?P -> (?P0 -> P4) /\ ?P0
goal 2 is:
?P -> (?P0 -> P4) /\ ?P0
goal 3 is:
?P
(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal:)
p14 < 3 focused goals
(shelved: 2)
P1, P2, P3, P4 : Prop
p12 : P1 -> P2
p123 : (P1 -> P2) -> P3
p34 : P3 -> P4
============================
?P -> (?P0 -> P4) /\ ?P0
goal 2 is:
?P -> (?P0 -> P4) /\ ?P0
goal 3 is:
?P
(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?P0; in current goal: ?X4 ?X5 ?X10 ?X11)
p14 <
Coq <
Coq <
|
