1 files changed, 170 insertions, 0 deletions
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
new file mode 100644
index 00000000..3178c6fc
--- /dev/null
+++ b/test-suite/success/bteauto.v
@@ -0,0 +1,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.