Commit d90c495b authored by Robbert Krebbers's avatar Robbert Krebbers

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 07d525a0 10ccbc24
......@@ -376,8 +376,8 @@ Lemma exist_elim {A} (P : A → uPred M) Q : (∀ a, P a ⊑ Q) → (∃ a, P a)
Proof. by intros HPQ x n ? [a ?]; apply HPQ with a. Qed.
Lemma eq_refl {A : cofeT} (a : A) P : P (a a).
Proof. by intros x n ??; simpl. Qed.
Lemma eq_rewrite {A : cofeT} P (Q : A uPred M)
`{HQ:∀ n, Proper (dist n ==> dist n) Q} a b : P (a b) P Q a P Q b.
Lemma eq_rewrite {A : cofeT} a b (Q : A uPred M) P
`{HQ:∀ n, Proper (dist n ==> dist n) Q} : P (a b) P Q a P Q b.
Proof.
intros Hab Ha x n ??; apply HQ with n a; auto. by symmetry; apply Hab with x.
Qed.
......@@ -435,7 +435,7 @@ Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
Proof. intros ->; apply eq_refl. Qed.
Lemma eq_sym {A : cofeT} (a b : A) : (a b) (b a).
Proof.
refine (eq_rewrite _ (λ b, b a)%I a b _ _); auto using eq_refl.
apply (eq_rewrite a b (λ b, b a)%I); auto using eq_refl.
intros n; solve_proper.
Qed.
......@@ -752,7 +752,7 @@ Qed.
Lemma always_eq {A:cofeT} (a b : A) : ( (a b))%I (a b : uPred M)%I.
Proof.
apply (anti_symmetric ()); auto using always_elim.
refine (eq_rewrite _ (λ b, (a b))%I a b _ _); auto.
apply (eq_rewrite a b (λ b, (a b))%I); auto.
{ intros n; solve_proper. }
rewrite -(eq_refl _ True) always_const; auto.
Qed.
......
......@@ -40,6 +40,8 @@ Section auth.
by rewrite always_and_sep_l'.
Qed.
Context {Hφ : n, Proper (dist n ==> dist n) φ}.
Lemma auth_opened a γ :
(auth_inv γ auth_own γ a) ( a', φ (a a') own AuthI γ ( (a a') a)).
Proof.
......@@ -48,6 +50,13 @@ Section auth.
rewrite /auth_own [(_ φ _)%I]commutative -associative -own_op.
rewrite own_valid_r auth_valid !sep_exist_l /=. apply exist_elim=>a'.
rewrite [ _]left_id -(exist_intro a').
Abort.
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. }
{ by rewrite !sep_elim_r. }
apply sep_mono; first done.
by rewrite sep_elim_l.
Qed.
End auth.
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