diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-06-09 21:49:10 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-06-16 18:21:08 +0200 |
commit | af7a9a4e44739968b68aeb1cb0a1f70a1aa34e88 (patch) | |
tree | e9d14b99a6024a40a3d3cf4a34c95a7251c119bb | |
parent | 4b29ca791bdfc810feabb883dc3d96a4ebd130a1 (diff) |
Example given at DeepSpec workshop
-rw-r--r-- | test-suite/success/bteauto.v | 141 |
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. |