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
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
|
Module onlyclasses.
(* In 8.6 we still allow non-class subgoals *)
Variable Foo : Type.
Variable foo : Foo.
Hint Extern 0 Foo => exact foo : typeclass_instances.
Goal Foo * Foo.
split. shelve.
Set Typeclasses Debug.
typeclasses eauto.
Unshelve. typeclasses eauto.
Qed.
Module RJung.
Class Foo (x : nat).
Instance foo x : x = 2 -> Foo x.
Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
Typeclasses eauto := debug.
Check (_ : Foo 2).
Fail Definition foo := (_ : 0 = 0).
End RJung.
End onlyclasses.
Module shelve_non_class_subgoals.
Variable Foo : Type.
Variable foo : Foo.
Hint Extern 0 Foo => exact foo : typeclass_instances.
Class Bar := {}.
Instance bar1 (f:Foo) : Bar := {}.
Typeclasses eauto := debug.
Set Typeclasses Debug Verbosity 2.
Goal Bar.
(* Solution has shelved subgoals (of non typeclass type) *)
typeclasses eauto.
Abort.
End shelve_non_class_subgoals.
Module RefineVsNoTceauto.
Class Foo (A : Type) := foo : A.
Instance: Foo nat := { foo := 0 }.
Instance: Foo nat := { foo := 42 }.
Hint Extern 0 (_ = _) => refine eq_refl : typeclass_instances.
Goal exists (f : Foo nat), @foo _ f = 0.
Proof.
unshelve (notypeclasses refine (ex_intro _ _ _)).
Set Typeclasses Debug. Set Printing All.
all:once (typeclasses eauto).
Fail idtac. (* Check no subgoals are left *)
Undo 3.
(** In this case, the (_ = _) subgoal is not considered
by typeclass resolution *)
refine (ex_intro _ _ _). Fail reflexivity.
Abort.
End RefineVsNoTceauto.
Module Leivantex2PR339.
(** Was a bug preventing to find hints associated with no pattern *)
Class Bar := {}.
Instance bar1 (t:Type) : Bar.
Hint Extern 0 => exact True : typeclass_instances.
Typeclasses eauto := debug.
Goal Bar.
Set Typeclasses Debug Verbosity 2.
typeclasses eauto. (* Relies on resolution of a non-class subgoal *)
Undo 1.
typeclasses eauto with typeclass_instances.
Qed.
End Leivantex2PR339.
Module bt.
Require Import Equivalence.
Record Equ (A : Type) (R : A -> A -> Prop).
Definition equiv {A} R (e : Equ A R) := R.
Record Refl (A : Type) (R : A -> A -> Prop).
Axiom equ_refl : forall A R (e : Equ A R), Refl _ (@equiv A R e).
Hint Extern 0 (Refl _ _) => unshelve class_apply @equ_refl; [shelve|] : foo.
Variable R : nat -> nat -> Prop.
Lemma bas : Equ nat R.
Admitted.
Hint Resolve bas : foo.
Hint Extern 1 => match goal with |- (_ -> _ -> Prop) => shelve end : foo.
Goal exists R, @Refl nat R.
eexists.
Set Typeclasses Debug.
(* Fail solve [unshelve eauto with foo]. *)
Set Typeclasses Debug Verbosity 1.
Test Typeclasses Depth.
solve [typeclasses eauto with foo].
Qed.
Set Typeclasses Compatibility "8.5".
Parameter f : nat -> Prop.
Parameter g : nat -> nat -> Prop.
Parameter h : nat -> nat -> nat -> Prop.
Axiom a : forall x y, g x y -> f x -> f y.
Axiom b : forall x (y : Empty_set), g (fst (x,y)) x.
Axiom c : forall x y z, h x y z -> f x -> f y.
Hint Resolve a b c : mybase.
Goal forall x y z, h x y z -> f x -> f y.
intros.
Fail Timeout 1 typeclasses eauto with mybase. (* Loops now *)
Unshelve.
Abort.
End bt.
Generalizable All Variables.
Module mon.
Reserved Notation "'return' t" (at level 0).
Reserved Notation "x >>= y" (at level 65, left associativity).
Record Monad {m : Type -> Type} := {
unit : forall {α}, α -> m α where "'return' t" := (unit t) ;
bind : forall {α β}, m α -> (α -> m β) -> m β where "x >>= y" := (bind x y) ;
bind_unit_left : forall {α β} (a : α) (f : α -> m β), return a >>= f = f a }.
Print Visibility.
Print unit.
Arguments unit {m m0 α}.
Arguments Monad : clear implicits.
Notation "'return' t" := (unit t).
(* Test correct handling of existentials and defined fields. *)
Class A `(e: T) := { a := True }.
Class B `(e_: T) := { e := e_; sg_ass :> A e }.
(* Set Typeclasses Debug. *)
(* Set Typeclasses Debug Verbosity 2. *)
Goal forall `{B T}, Prop.
intros. apply a.
Defined.
Goal forall `{B T}, Prop.
intros. refine (@a _ _ _).
Defined.
Class B' `(e_: T) := { e' := e_; sg_ass' :> A e_ }.
Goal forall `{B' T}, a.
intros. exact I.
Defined.
End mon.
(* Correct treatment of dependent goals *)
(* First some preliminaries: *)
Section sec.
Context {N: Type}.
Class C (f: N->N) := {}.
Class E := { e: N -> N }.
Context
(g: N -> N) `(E) `(C e)
`(forall (f: N -> N), C f -> C (fun x => f x))
(U: forall f: N -> N, C f -> False).
(* Now consider the following: *)
Let foo := U (fun x => e x).
Check foo _.
(* This type checks fine, so far so good. But now
let's try to get rid of the intermediate constant foo.
Surely we can just expand it inline, right? Wrong!: *)
Check U (fun x => e x) _.
End sec.
Module UniqueSolutions.
Set Typeclasses Unique Solutions.
Class Eq (A : Type) : Set.
Instance eqa : Eq nat := {}.
Instance eqb : Eq nat := {}.
Goal Eq nat.
try apply _.
Fail exactly_once typeclasses eauto.
Abort.
End UniqueSolutions.
Module UniqueInstances.
(** Optimize proof search on this class by never backtracking on (closed) goals
for it. *)
Set Typeclasses Unique Instances.
Class Eq (A : Type) : Set.
Instance eqa : Eq nat := _. constructor. Qed.
Instance eqb : Eq nat := {}.
Class Foo (A : Type) (e : Eq A) : Set.
Instance fooa : Foo _ eqa := {}.
Tactic Notation "refineu" open_constr(c) := unshelve refine c.
Set Typeclasses Debug.
Goal { e : Eq nat & Foo nat e }.
unshelve refineu (existT _ _ _).
all:simpl.
(** Does not backtrack on the (wrong) solution eqb *)
Fail all:typeclasses eauto.
Abort.
End UniqueInstances.
Module IterativeDeepening.
Class A.
Class B.
Class C.
Instance: B -> A | 0.
Instance: C -> A | 0.
Instance: C -> B -> A | 0.
Instance: A -> A | 0.
Goal C -> A.
intros.
Set Typeclasses Debug.
Fail Timeout 1 typeclasses eauto.
Set Typeclasses Iterative Deepening.
Fail typeclasses eauto 1.
typeclasses eauto 2.
Undo.
Unset Typeclasses Iterative Deepening.
Fail Timeout 1 typeclasses eauto.
Set Typeclasses Iterative Deepening.
typeclasses eauto.
Qed.
End IterativeDeepening.
Module AxiomsAreInstances.
Set Typeclasses Axioms Are Instances.
Class TestClass1 := {}.
Axiom testax1 : TestClass1.
Definition testdef1 : TestClass1 := _.
Unset Typeclasses Axioms Are Instances.
Class TestClass2 := {}.
Axiom testax2 : TestClass2.
Fail Definition testdef2 : TestClass2 := _.
(* we didn't break typeclasses *)
Existing Instance testax2.
Definition testdef2 : TestClass2 := _.
End AxiomsAreInstances.
|
