Example given at DeepSpec workshop

1 files changed, 107 insertions, 34 deletions

diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index eadba47b8..34238fe13 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -1,42 +1,115 @@
+Module Backtracking.
+  Class A := { foo : nat }.
 
-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 *)
+    Fail all:((once typeclasses eauto) + apply eq_refl).
+    (* Does backtrack if other goals fail *)
+    all:((typeclasses eauto) + reflexivity).
+    Show Proof.  
+  Qed.
 
-Instance A_1 : A | 2 := { foo := 42 }.
-Instance A_0 : A | 1 := { foo := 0 }.
-Lemma aeq (a : A) : foo = foo.
-  reflexivity.
-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.
+End Backtracking.
 
-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).
+
+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.
+  Fail Timeout 1 eauto 1000.
+
+  typeclasses eauto with core.
 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).
+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).
+
+Hint Mode Equality + : typeclass_instances.
+
+(* No more defaulting, reduce "trigger-happiness" *)
+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.