diff --git a/algebra/cofe.v b/algebra/cofe.v index 646c4d54135cecfc26eb8ebc01893add812601d9..d75d8b18712d342c99fac57fe44ebb33c6b9cb9b 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 a495acb49573f43a061cecad7b12a8a10da0de6c..5167b9aa4db96465accf0a2092ac648747721020 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.