Commit 24e91f98 authored by Ralf Jung's avatar Ralf Jung
Browse files

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

parents 078ec73d 09d97eae
Pipeline #3916 passed with stage
in 3 minutes and 51 seconds
...@@ -1095,22 +1095,22 @@ Proof. ...@@ -1095,22 +1095,22 @@ Proof.
- intros n y1 y2. rewrite !g_dist. apply dist_S. - intros n y1 y2. rewrite !g_dist. apply dist_S.
Qed. Qed.
Program Definition iso_cofe_subtype {A B : ofeT} `{Cofe A} Section iso_cofe_subtype.
(P : A Prop) `{!LimitPreserving P} Context {A B : ofeT} `{Cofe A} (P : A Prop) (f : x, P x B) (g : B A).
(f : x, P x B) (g : B A) Context (Pg : y, P (g y)).
(Pg : y, P (g y)) Context (g_dist : n y1 y2, y1 {n} y2 g y1 {n} g y2).
(g_dist : n y1 y2, y1 {n} y2 g y1 {n} g y2) Let Hgne : NonExpansive g.
(gf : x Hx, g (f x Hx) x) : Cofe B := Proof. intros n y1 y2. apply g_dist. Qed.
let _ : NonExpansive g := _ in Existing Instance Hgne.
{| compl c := f (compl (chain_map g c)) _ |}. Context (gf : x Hx, g (f x Hx) x).
Next Obligation. intros A B ? P _ f g _ g_dist _ n y1 y2. apply g_dist. Qed. Context (Hlimit : c : chain B, P (compl (chain_map g c))).
Next Obligation. Program Definition iso_cofe_subtype : Cofe B :=
intros A B ? P ? f g ? g_dist gf ? c. apply limit_preserving=> n. apply Pg. {| compl c := f (compl (chain_map g c)) _ |}.
Qed. Next Obligation. apply Hlimit. Qed.
Next Obligation. Next Obligation.
intros A B ? P ? f g ? g_dist gf ? n c; simpl. intros n c; simpl. apply g_dist. by rewrite gf conv_compl.
apply g_dist. by rewrite gf conv_compl. Qed.
Qed. End iso_cofe_subtype.
Definition iso_cofe {A B : ofeT} `{Cofe A} (f : A B) (g : B A) Definition iso_cofe {A B : ofeT} `{Cofe A} (f : A B) (g : B A)
(g_dist : n y1 y2, y1 {n} y2 g y1 {n} g y2) (g_dist : n y1 y2, y1 {n} y2 g y1 {n} g y2)
...@@ -1141,7 +1141,11 @@ Section sigma. ...@@ -1141,7 +1141,11 @@ Section sigma.
Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin. Canonical Structure sigC : ofeT := OfeT (sig P) sig_ofe_mixin.
Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigC. Global Instance sig_cofe `{Cofe A, !LimitPreserving P} : Cofe sigC.
Proof. by apply (iso_cofe_subtype P (exist P) proj1_sig proj2_sig). Qed. Proof.
apply: (iso_cofe_subtype P (exist P) proj1_sig).
- done.
- intros c. apply limit_preserving=> n. apply proj2_sig.
Qed.
Global Instance sig_timeless (x : sig P) : Timeless (`x) Timeless x. Global Instance sig_timeless (x : sig P) : Timeless (`x) Timeless x.
Proof. intros ? y. rewrite sig_dist_alt sig_equiv_alt. apply (timeless _). Qed. Proof. intros ? y. rewrite sig_dist_alt sig_equiv_alt. apply (timeless _). Qed.
......
...@@ -15,12 +15,10 @@ Section ofe. ...@@ -15,12 +15,10 @@ Section ofe.
Global Instance list_cofe `{Cofe A} m : Cofe (vecC m). Global Instance list_cofe `{Cofe A} m : Cofe (vecC m).
Proof. Proof.
assert (LimitPreserving (λ l, length l = m)). apply: (iso_cofe_subtype (λ l : list A, length l = m)
{ apply limit_preserving_timeless=> l k -> //. }
apply (iso_cofe_subtype (λ l : list A, length l = m)
(λ l, eq_rect _ (vec A) (list_to_vec l) m) vec_to_list)=> //. (λ l, eq_rect _ (vec A) (list_to_vec l) m) vec_to_list)=> //.
- intros v. by rewrite vec_to_list_length.
- intros v []. by rewrite /= vec_to_list_of_list. - intros v []. by rewrite /= vec_to_list_of_list.
- intros c. by rewrite (conv_compl 0 (chain_map _ c)) /= vec_to_list_length.
Qed. Qed.
Global Instance vnil_timeless : Timeless (@vnil A). Global Instance vnil_timeless : Timeless (@vnil A).
......
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