Commit da599b51 authored by Ralf Jung's avatar Ralf Jung

add a tactic to solve non-expansiveness goals

parent 74ca0005
...@@ -21,6 +21,8 @@ Tactic Notation "cofe_subst" := ...@@ -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 | H:@dist ?A ?d ?n _ ?x |- _ => symmetry in H;setoid_subst_aux (@dist A d n) x
end. end.
Tactic Notation "solve_ne" := move=>n; solve_proper.
Record chain (A : Type) `{Dist A} := { Record chain (A : Type) `{Dist A} := {
chain_car :> nat A; chain_car :> nat A;
chain_cauchy n i : n < i chain_car i {n} chain_car (S n) chain_cauchy n i : n < i chain_car i {n} chain_car (S n)
......
...@@ -56,9 +56,7 @@ Section auth. ...@@ -56,9 +56,7 @@ Section auth.
rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'. rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'.
rewrite [ _]left_id -(exist_intro a'). rewrite [ _]left_id -(exist_intro a').
apply (eq_rewrite b (a a') apply (eq_rewrite b (a a')
(λ x, ▷φ x own AuthI γ ( x a))%I). (λ x, ▷φ x own AuthI γ ( x a))%I); first by solve_ne.
{ (* TODO this asks for automation. *)
move=>n a1 a2 Ha. by rewrite !Ha. }
{ by rewrite !sep_elim_r. } { by rewrite !sep_elim_r. }
apply sep_mono; first done. apply sep_mono; first done.
by rewrite sep_elim_l. by rewrite sep_elim_l.
......
Markdown is supported
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