Commit 87e002de authored by Michael Sammler's avatar Michael Sammler
Browse files

add multisuccess

parent 8ec08fe4
......@@ -4,4 +4,4 @@ This repository contain a collection of interesting tricks and facts about Coq t
- [slow_qed.v](theories/slow_qed.v): Causes for slow Qed times
- [custom_typeclass_db.v](theories/custom_typeclass_db.v): How to use custom typeclass databases
- TODO: How to iterate over all solutions for typeclass search
- [multisuccess.v](theories/multisuccess.v): How to iterate over all solutions for typeclass search
......@@ -8,4 +8,5 @@
-Q theories tricks
theories/slow_qed.v
theories/custom_typeclass_db.v
\ No newline at end of file
theories/custom_typeclass_db.v
theories/multisuccess.v
\ No newline at end of file
(** This file shows how to use iterate over all possible solutions for typeclass search. *)
From Coq Require Export Utf8.
Ltac print_goal := lazymatch goal with | |- ?G => idtac G end.
(** Consider a typeclass that guesses a number. *)
Class GuessANumber := {
guess : nat
}.
(** and the following three instances to guess 0, 1 and 2 respectively. *)
Global Instance guess_0 : GuessANumber := {| guess := 0 |}.
Global Instance guess_1 : GuessANumber := {| guess := 1 |}.
Global Instance guess_2 : GuessANumber := {| guess := 2 |}.
(** We want to use [GuessANumber] to guess some instantiatiations for
an existential quantifier: *)
Lemma use_guess (P : nat Prop) `{!GuessANumber}:
P guess
x, P x.
Proof. eauto. Qed.
Goal x, x = 1.
(** But if we use [use_guess] naively, there is a problem: *)
eapply use_guess; simpl.
(** Coq simply picks the first guess (2 in this case) and makes the goal unprovable! *)
Fail reflexivity.
Abort.
Goal x, x = 1.
(** What we want is to iterate over all the possible guesses and
pick the one that succeeds. To do this, we exploit that [typeclasses
eauto] returns multiple successes for each possible instance.
Concretely, the following succeeds: *)
simple notypeclasses refine (use_guess _ _); [typeclasses eauto | reflexivity].
Abort.
Goal x, x = 1.
(** What happended there? If proof search after [typeclasses eauto]
fails, Coq backtracks and tries another possible instance. To see
this, let us print all the instantiations: (Note that the fail
triggers backtracking and trying the next instance.) *)
try (simple notypeclasses refine (use_guess _ _); [typeclasses eauto |
simpl; print_goal; fail]).
(** This prints:
(2 = 1)
(1 = 1)
(0 = 1)
*)
(** However, one needs to be a bit careful to let the backtracking
not get out of hand. In particular, the following prints
(1 = 1)
(0 = 1)
since Coq tries more instances even if the failure comes outside the [ | ].
*)
try (simple notypeclasses refine (use_guess _ _); [typeclasses eauto |
simpl; lazymatch goal with | |- 1 = 1 => idtac | |- 0 = 1 => idtac end ]; print_goal; fail).
(** Thus, one should use [once] when relying on multiple successes
of typeclass search as [once] stops further backtracking. In
particular, the following only prints
(1 = 1)
*)
try (once (simple notypeclasses refine (use_guess _ _); [typeclasses eauto |
simpl; lazymatch goal with | |- 1 = 1 => idtac | |- 0 = 1 => idtac end ]); print_goal; fail).
Abort.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment