From dd6f44a45731f4f8359a8251fcdf5b791346c6d1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 13 Feb 2016 19:30:12 +0100
Subject: [PATCH] add some missing timeless instances; fix auth.v eauto usage
 and argument implicity

On branch master
	modified:   algebra/fin_maps.v
Untracked files:
	heap_lang/heap.v
no changes added to commit (use "git add" and/or "git commit -a")
---
 algebra/fin_maps.v   | 5 +++++
 algebra/option.v     | 2 ++
 program_logic/auth.v | 4 ++--
 3 files changed, 9 insertions(+), 2 deletions(-)

diff --git a/algebra/fin_maps.v b/algebra/fin_maps.v
index 910e124da..6f19ff730 100644
--- a/algebra/fin_maps.v
+++ b/algebra/fin_maps.v
@@ -57,6 +57,11 @@ Proof.
     [by constructor|by apply lookup_ne].
 Qed.
 
+Global Instance map_timeless `{!∀ a : A, Timeless a} (g : gmap K A) : Timeless g.
+Proof.
+  intros m Hm i. apply timeless; eauto with typeclass_instances.
+Qed.
+
 Instance map_empty_timeless : Timeless (∅ : gmap K A).
 Proof.
   intros m Hm i; specialize (Hm i); rewrite lookup_empty in Hm |- *.
diff --git a/algebra/option.v b/algebra/option.v
index dafa849ab..94eeac7aa 100644
--- a/algebra/option.v
+++ b/algebra/option.v
@@ -51,6 +51,8 @@ Global Instance None_timeless : Timeless (@None A).
 Proof. inversion_clear 1; constructor. Qed.
 Global Instance Some_timeless x : Timeless x → Timeless (Some x).
 Proof. by intros ?; inversion_clear 1; constructor; apply timeless. Qed.
+Global Instance option_timeless `{!∀ a : A, Timeless a} (mx : option A) : Timeless mx.
+Proof. destruct mx; auto with typeclass_instances. Qed.
 End cofe.
 
 Arguments optionC : clear implicits.
diff --git a/program_logic/auth.v b/program_logic/auth.v
index 65bd7e42c..608410086 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -62,7 +62,7 @@ Section auth.
     apply (eq_rewrite b (a â‹… a')
               (λ x, ■✓x ★ ▷φ x ★ own AuthI γ (● x ⋅ ◯ a))%I).
     { by move=>n ? ? /timeless_iff ->. }
-    { apply sep_elim_l', sep_elim_r'. done. (* FIXME why does "eauto using I" not work? *) }
+    { by eauto with I. }
     rewrite const_equiv // left_id comm.
     apply sep_mono; first done.
     by rewrite sep_elim_l.
@@ -84,7 +84,7 @@ Section auth.
      step-indices. However, since A is timeless, that should not be
      a restriction.  *)
   Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
-        `{!LocalUpdate Lv L} N E P (Q : X → iPropG Λ Σ) γ a :
+        L `{!LocalUpdate Lv L} N E P (Q : X → iPropG Λ Σ) γ a :
     nclose N ⊆ E →
     P ⊑ auth_ctx AuthI γ N φ →
     P ⊑ (auth_own AuthI γ a ★ (∀ a', ■✓(a ⋅ a') ★ ▷φ (a ⋅ a') -★
-- 
GitLab