blob: eadba47b812af51529703795ecae1bb6dc72b835 (
plain)
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
|
Class A := { foo : nat }.
Instance A_1 : A | 2 := { foo := 42 }.
Instance A_0 : A | 1 := { foo := 0 }.
Lemma aeq (a : A) : foo = foo.
reflexivity.
Qed.
Goal exists n, n = 42.
eexists.
eapply eq_trans.
evar (a : A). subst a.
refine (@aeq ?a).
Unshelve. all:cycle 1.
typeclasses eauto.
Fail reflexivity.
Undo 2.
Set Typeclasses Debug.
(* Without multiple successes it fails *)
Fail all:((once typeclasses eauto) + reflexivity).
(* Does backtrack if other goals fail *)
all:((typeclasses eauto) + reflexivity).
Qed.
Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
Goal exists n, n = 42.
eexists.
eapply eq_trans.
evar (a : A). subst a.
refine (@aeq ?a).
Unshelve. all:cycle 1.
typeclasses eauto.
Fail reflexivity.
Undo 2.
Set Typeclasses Debug.
(* Does backtrack between individual goals *)
all:(typeclasses eauto).
Qed.
Fail Timeout 1 Check prf.
Hint Mode SomeProp + + : typeclass_instances.
Check prf.
Check (fun H : SomeProp plus => _ : SomeProp (flip plus)).
(** Iterative deepening / breadth-first search *)
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 := debug 3.
typeclasses eauto.
Qed.
End IterativeDeepening.
|
