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
|
(* Wish #2154 by E. van der Weegen *)
(* auto was not using f_equal-style lemmas with metavariables occurring
only in the type of an evar of the concl, but not directly in the
concl itself *)
Parameters
(F: Prop -> Prop)
(G: forall T, (T -> Prop) -> Type)
(L: forall A (P: A -> Prop), G A P -> forall x, F (P x))
(Q: unit -> Prop).
Hint Resolve L.
Goal G unit Q -> F (Q tt).
intro.
eauto.
Qed.
(* Test implicit arguments in "using" clause *)
Goal forall n:nat, nat * nat.
auto using (pair O).
Undo.
eauto using (pair O).
Qed.
Create HintDb test discriminated.
Parameter foo : forall x, x = x + 0.
Hint Resolve foo : test.
Variable C : nat -> Type -> Prop.
Variable c_inst : C 0 nat.
Hint Resolve c_inst : test.
Hint Mode C - + : test.
Hint Resolve c_inst : test2.
Hint Mode C + + : test2.
Goal exists n, C n nat.
Proof.
eexists. Fail progress debug eauto with test2.
progress eauto with test.
Qed.
(** Patterns of Extern have a "matching" semantics.
It is not so for apply/exact hints *)
Class B (A : Type).
Class I.
Instance i : I.
Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y.
Class D (f : nat -> nat -> nat).
Definition ftest (x y : nat) := x + y.
Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f).
Admitted.
Module Instnopat.
Local Instance: B nat.
(* pattern_of_constr -> B nat *)
(* exact hint *)
Check (_ : B nat).
(* map_eauto -> B_instance0 *)
(* NO Constr_matching.matches !!! *)
Check (_ : B _).
Goal exists T, B T.
eexists.
eauto with typeclass_instances.
Qed.
Local Instance: D ftest.
Local Hint Resolve flipD | 0 : typeclass_instances.
(* pattern: D (flip _) *)
Fail Timeout 1 Check (_ : D _). (* loops applying flipD *)
End Instnopat.
Module InstnopatApply.
Local Instance: I -> B nat.
(* pattern_of_constr -> B nat *)
(* apply hint *)
Check (_ : B nat).
(* map_eauto -> B_instance0 *)
(* NO Constr_matching.matches !!! *)
Check (_ : B _).
Goal exists T, B T.
eexists.
eauto with typeclass_instances.
Qed.
End InstnopatApply.
Module InstPat.
Hint Extern 3 (B nat) => split : typeclass_instances.
(* map_eauto -> Extern hint *)
(* Constr_matching.matches -> true *)
Check (_ : B nat).
(* map_eauto -> Extern hint *)
(* Constr_matching.matches -> false:
Because an inductive in the pattern does not match an evar in the goal *)
Check (_ : B _).
Goal exists T, B T.
eexists.
(* map_existential -> Extern hint *)
(* Constr_matching.matches -> false *)
Fail progress eauto with typeclass_instances.
(* map_eauto -> Extern hint *)
(* Constr_matching.matches -> false *)
Fail typeclasses eauto.
Abort.
Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances.
Module withftest.
Local Instance: D ftest.
Check (_ : D _).
(* D_instance_0 : D ftest *)
Check (_ : D (flip _)).
(* ... : D (flip ftest) *)
End withftest.
Module withoutftest.
Hint Extern 0 (D ftest) => split : typeclass_instances.
Check (_ : D _).
(* ? : D ?, _not_ looping *)
Check (_ : D (flip _)).
(* ? : D (flip ?), _not_ looping *)
Check (_ : D (flip ftest)).
(* flipD ftest {| |} : D (flip ftest) *)
End withoutftest.
End InstPat.
|
