From 2a7755fee187492a6bf36a89f5f3ec0b5407a637 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 16 Nov 2016 00:49:47 +0100
Subject: [PATCH] Different treatment of atomic premise in type class.
In Coq 8.6 type class search is not called recursively on premises
that are not type classes. To that end, we use a hint extern to invoke
an ordinary auto.
---
heap_lang/tactics.v | 2 +-
program_logic/weakestpre.v | 7 ++++---
2 files changed, 5 insertions(+), 4 deletions(-)
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index 4d9c1633c..f399d09d3 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -230,7 +230,7 @@ Ltac solve_atomic :=
end.
Hint Extern 10 (language.atomic _) => solve_atomic.
(* For the side-condition of elim_upd_fupd_wp_atomic *)
-Hint Extern 10 (language.atomic _) => solve_atomic : typeclass_instances.
+Hint Extern 10 (language.atomic _) => solve_atomic : atomic.
(** Substitution *)
Ltac simpl_subst :=
diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index 97fee1f57..699172b24 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -310,12 +310,13 @@ Section proofmode_classes.
ElimModal (|={E}=> P) P (WP e @ E {{ Φ }}) (WP e @ E {{ Φ }}).
Proof. by rewrite /ElimModal fupd_frame_r wand_elim_r fupd_wp. Qed.
- (* lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
- Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
+ Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
atomic e →
ElimModal (|={E1,E2}=> P) P
(WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
End proofmode_classes.
-Hint Extern 0 (atomic _) => assumption : typeclass_instances.
+(* Lower precedence, if possible, it should always pick elim_upd_fupd_wp *)
+Hint Extern 100 (ElimModal (|={_,_}=> _) _ (WP _ @ _ {{ _ }}) _) =>
+ eapply elim_modal_fupd_wp_atomic; solve [auto with atomic] : typeclass_instances.
--
GitLab