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
|
Goal forall a b c : nat, a = b -> b = c -> forall d, a+d=c+d.
intros.
(* "compatibility" mode: specializing a global name
means a kind of generalize *)
specialize eq_trans. intros _.
specialize eq_trans with (1:=H)(2:=H0). intros _.
specialize eq_trans with (x:=a)(y:=b)(z:=c). intros _.
specialize eq_trans with (1:=H)(z:=c). intros _.
specialize eq_trans with nat a b c. intros _.
specialize (@eq_trans nat). intros _.
specialize (@eq_trans _ a b c). intros _.
specialize (eq_trans (x:=a)). intros _.
specialize (eq_trans (x:=a)(y:=b)). intros _.
specialize (eq_trans H H0). intros _.
specialize (eq_trans H0 (z:=b)). intros _.
(* incomplete bindings: y is left quantified and z is instantiated. *)
specialize eq_trans with (x:=a)(z:=c).
intro h.
(* y can be instantiated now *)
specialize h with (y:=b).
(* z was instantiated above so this must fail. *)
Fail specialize h with (z:=c).
clear h.
(* incomplete bindings: 1st dep hyp is instantiated thus A, x and y
instantiated too. *)
specialize eq_trans with (1:=H).
intro h.
(* 2nd dep hyp can be instantiated now, which instatiates z too. *)
specialize h with (1:=H0).
(* checking that there is no more products in h. *)
match type of h with
| _ = _ => idtac
| _ => fail "specialize test failed: hypothesis h should be an equality at this point"
end.
clear h.
(* local "in place" specialization *)
assert (Eq:=eq_trans).
specialize Eq.
specialize Eq with (1:=H)(2:=H0). Undo.
specialize Eq with (x:=a)(y:=b)(z:=c). Undo.
specialize Eq with (1:=H)(z:=c). Undo.
specialize Eq with nat a b c. Undo.
specialize (Eq nat). Undo.
specialize (Eq _ a b c). Undo.
(* no implicit argument for Eq, hence no (Eq (x:=a)) *)
specialize (Eq _ _ _ _ H H0). Undo.
specialize (Eq _ _ _ b H0). Undo.
(* incomplete binding *)
specialize Eq with (y:=b).
(* A and y have been instantiated so this works *)
specialize (Eq _ _ H H0).
Undo 2.
(* incomplete binding (dependent) *)
specialize Eq with (1:=H).
(* A, x and y have been instantiated so this works *)
specialize (Eq _ H0).
Undo 2.
(* incomplete binding (dependent) *)
specialize Eq with (1:=H) (2:=H0).
(* A, x and y have been instantiated so this works *)
match type of Eq with
| _ = _ => idtac
| _ => fail "specialize test failed: hypothesis Eq should be an equality at this point"
end.
Undo 2.
(*
(** strange behavior to inspect more precisely *)
(* 1) proof aspect : let H:= ... in (fun H => ..) H
presque ok... *)
(* 2) echoue moins lorsque zero premise de mangé *)
specialize eq_trans with (1:=Eq). (* mal typé !! *)
(* 3) Seems fixed.*)
specialize eq_trans with _ a b c. intros _.
(* Anomaly: Evar ?88 was not declared. Please report. *)
*)
Abort.
(* Test use of pose proof and assert as a specialize *)
Goal True -> (True -> 0=0) -> False -> 0=0.
intros H0 H H1.
pose proof (H I) as H.
(* Check that the hypothesis is in 2nd position by removing the top one *)
match goal with H:_ |- _ => clear H end.
match goal with H:_ |- _ => exact H end.
Qed.
Goal True -> (True -> 0=0) -> False -> 0=0.
intros H0 H H1.
assert (H:=H I).
(* Check that the hypothesis is in 2nd position by removing the top one *)
match goal with H:_ |- _ => clear H end.
match goal with H:_ |- _ => exact H end.
Qed.
(* let ins should be supported int he type of the specialized hypothesis *)
Axiom foo: forall (m1:nat) (m2: nat), let n := 2 * m1 in (m1 = m2 -> False).
Goal False.
pose proof foo as P.
assert (2 = 2) as A by reflexivity.
(* specialize P with (m2:= 2). *)
specialize P with (1 := A).
match type of P with
| let n := 2 * 2 in False => idtac
| _ => fail "test failed"
end.
assumption.
Qed.
(* Another more subtle test on letins: they should not interfere with foralls. *)
Goal forall (P: forall a c:nat,
let b := c in
let d := 1 in
forall n : a = d, a = c+1),
True.
intros P.
specialize P with (1:=eq_refl).
match type of P with
| forall c : nat, let f := c in let d := 1 in 1 = c + 1 => idtac
| _ => fail "test failed"
end.
constructor.
Qed.
(* Test specialize as *)
Goal (forall x, x=0) -> 1=0.
intros.
specialize (H 1) as ->.
reflexivity.
Qed.
(* A test from corn *)
Goal (forall x y, x=0 -> y=0 -> True) -> True.
intros.
specialize (fun z => H 0 z eq_refl).
exact (H 0 eq_refl).
Qed.
|
