Commit ec0816bf by Robbert Krebbers

### Carry `saved_anything_agree` out in the proof mode.

```It does not really help since the main work of the proof is in showing that
`cFunctor_map F (iProp_fold, iProp_unfold)` is injective, but whatever.```
parent 1da32c56
 ... @@ -42,15 +42,15 @@ Section saved_anything. ... @@ -42,15 +42,15 @@ Section saved_anything. Lemma saved_anything_agree γ x y : Lemma saved_anything_agree γ x y : saved_anything_own γ x -∗ saved_anything_own γ y -∗ x ≡ y. saved_anything_own γ x -∗ saved_anything_own γ y -∗ x ≡ y. Proof. Proof. (* TODO: Use the proof mode. *) iIntros "Hx Hy". rewrite /saved_anything_own. apply wand_intro_r. iDestruct (own_valid_2 with "Hx Hy") as "Hv". rewrite -own_op own_valid agree_validI agree_equivI. rewrite agree_validI agree_equivI. set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)). set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)). set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)). set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)). assert (∀ z, G2 (G1 z) ≡ z) as help. assert (∀ z, G2 (G1 z) ≡ z) as help. { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id. { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id. apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. } apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. } rewrite -{2}[x]help -{2}[y]help. apply f_equiv, _. rewrite -{2}[x]help -{2}[y]help. by iApply f_equiv. Qed. Qed. End saved_anything. End saved_anything. ... ...
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