Commit a988acd6 authored by Robbert Krebbers's avatar Robbert Krebbers

Make use of OFE isomorphisms in COFE solver.

parent 415685af
......@@ -4,13 +4,8 @@ Set Default Proof Using "Type".
Record solution (F : oFunctor) := Solution {
solution_car :> ofeT;
solution_cofe : Cofe solution_car;
solution_unfold : solution_car -n> F solution_car _;
solution_fold : F solution_car _ -n> solution_car;
solution_fold_unfold X : solution_fold (solution_unfold X) X;
solution_unfold_fold X : solution_unfold (solution_fold X) X
solution_iso :> ofe_iso (F solution_car _) solution_car;
}.
Arguments solution_unfold {_} _.
Arguments solution_fold {_} _.
Existing Instance solution_cofe.
Module solver. Section solver.
......@@ -210,7 +205,7 @@ Proof. by intros n X Y HXY k; rewrite /fold /= HXY. Qed.
Theorem result : solution F.
Proof using Type*.
apply (Solution F T _ (OfeMor unfold) (OfeMor fold)).
refine (Solution F T _ (OfeIso (OfeMor fold) (OfeMor unfold) _ _)).
- move=> X /=. rewrite equiv_dist=> n k; rewrite /unfold /fold /=.
rewrite -g_tower -(gg_tower _ n); apply (_ : Proper (_ ==> _) (g _)).
trans (map (ff n, gg n) (X (S (n + k)))).
......
......@@ -147,12 +147,13 @@ Module Export iProp_solution : iProp_solution_sig.
Notation iPropO Σ := (uPredO (iResUR Σ)).
Definition iProp_unfold {Σ} : iPropO Σ -n> iPrePropO Σ :=
solution_fold (iProp_result Σ).
Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ := solution_unfold _.
ofe_iso_1 (iProp_result Σ).
Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ :=
ofe_iso_2 (iProp_result Σ).
Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) P.
Proof. apply solution_unfold_fold. Qed.
Proof. apply ofe_iso_21. Qed.
Lemma iProp_unfold_fold {Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) P.
Proof. apply solution_fold_unfold. Qed.
Proof. apply ofe_iso_12. Qed.
End iProp_solution.
......
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