blob: 3178c6fc15635a54b4c8e9ded3b6eb00543985da (
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
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
|
Require Import Program.Tactics.
Module Backtracking.
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.
Arguments foo A : clear implicits.
Example find42 : exists n, n = 42.
Proof.
eexists.
eapply eq_trans.
evar (a : A). subst a.
refine (@aeq ?a).
Unshelve. all:cycle 1.
typeclasses eauto.
Fail reflexivity.
Undo 2.
(* Without multiple successes it fails *)
Set Typeclasses Debug Verbosity 2.
Fail all:((once (typeclasses eauto with typeclass_instances))
+ apply eq_refl).
(* Does backtrack if other goals fail *)
all:[> typeclasses eauto + reflexivity .. ].
Undo 1.
all:(typeclasses eauto + reflexivity). (* Note "+" is a focussing combinator *)
Show Proof.
Qed.
Print find42.
Hint Extern 0 (_ = _) => reflexivity : equality.
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.
(* Does backtrack between individual goals *)
Set Typeclasses Debug.
all:(typeclasses eauto with typeclass_instances equality).
Qed.
Unset Typeclasses Debug.
Module Leivant.
Axiom A : Type.
Existing Class A.
Axioms a b c d e: A.
Ltac get_value H := eval cbv delta [H] in H.
Goal True.
Fail refine (let H := _ : A in _); let v := get_value H in idtac v; fail.
Admitted.
Goal exists x:A, x=a.
unshelve evar (t : A). all:cycle 1.
refine (@ex_intro _ _ t _).
all:cycle 1.
all:(typeclasses eauto + reflexivity).
Qed.
End Leivant.
End Backtracking.
Hint Resolve 100 eq_sym eq_trans : core.
Hint Cut [(_)* eq_sym eq_sym] : core.
Hint Cut [_* eq_trans eq_trans] : core.
Hint Cut [_* eq_trans eq_sym eq_trans] : core.
Goal forall x y z : nat, x = y -> z = y -> x = z.
Proof.
intros.
typeclasses eauto with core.
Qed.
Module Hierarchies.
Class A := mkA { data : nat }.
Class B := mkB { aofb :> A }.
Existing Instance mkB.
Definition makeB (a : A) : B := _.
Definition makeA (a : B) : A := _.
Fail Timeout 1 Definition makeA' : A := _.
Hint Cut [_* mkB aofb] : typeclass_instances.
Fail Definition makeA' : A := _.
Fail Definition makeB' : B := _.
End Hierarchies.
(** Hint modes *)
Class Equality (A : Type) := { eqp : A -> A -> Prop }.
Check (eqp 0%nat 0).
Instance nat_equality : Equality nat := { eqp := eq }.
Instance default_equality A : Equality A | 1000 :=
{ eqp := eq }.
Check (eqp 0%nat 0).
(* Defaulting *)
Check (fun x y => eqp x y).
(* No more defaulting, reduce "trigger-happiness" *)
Definition ambiguous x y := eqp x y.
Hint Mode Equality ! : typeclass_instances.
Fail Definition ambiguous' x y := eqp x y.
Definition nonambiguous (x y : nat) := eqp x y.
(** Typical looping instances with defaulting: *)
Definition flip {A B C} (f : A -> B -> C) := fun x y => f y x.
Class SomeProp {A : Type} (f : A -> A -> A) :=
{ prf : forall x y, f x y = f x y }.
Instance propflip (A : Type) (f : A -> A -> A) :
SomeProp f -> SomeProp (flip f).
Proof.
intros []. constructor. reflexivity.
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.
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.
|
