From da599b51b2acc30a1623f5cecf98eb45424ba566 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Feb 2016 11:08:07 +0100
Subject: [PATCH] add a tactic to solve non-expansiveness goals

---
 algebra/cofe.v       | 2 ++
 program_logic/auth.v | 4 +---
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/algebra/cofe.v b/algebra/cofe.v
index 646c4d541..d75d8b187 100644
--- a/algebra/cofe.v
+++ b/algebra/cofe.v
@@ -21,6 +21,8 @@ Tactic Notation "cofe_subst" :=
   | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
   end.
 
+Tactic Notation "solve_ne" := move=>n; solve_proper.
+
 Record chain (A : Type) `{Dist A} := {
   chain_car :> nat → A;
   chain_cauchy n i : n < i → chain_car i ≡{n}≡ chain_car (S n)
diff --git a/program_logic/auth.v b/program_logic/auth.v
index a495acb49..5167b9aa4 100644
--- a/program_logic/auth.v
+++ b/program_logic/auth.v
@@ -56,9 +56,7 @@ Section auth.
     rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'.
     rewrite [∅ ⋅ _]left_id -(exist_intro a').
     apply (eq_rewrite b (a â‹… a')
-              (λ x, ▷φ x ★ own AuthI γ (● x ⋅ ◯ a))%I).
-    { (* TODO this asks for automation. *)
-      move=>n a1 a2 Ha. by rewrite !Ha. }
+              (λ x, ▷φ x ★ own AuthI γ (● x ⋅ ◯ a))%I); first by solve_ne.
     { by rewrite !sep_elim_r. }
     apply sep_mono; first done.
     by rewrite sep_elim_l.
-- 
GitLab