From c924930501716de8e36c4ef44019786cda41f6f8 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 28 Mar 2025 17:42:03 +0100
Subject: [PATCH] Bump Iris (Transfinite algebra).
---
actris/channel/proto.v | 2 +-
actris/channel/proto_model.v | 4 ++--
actris/utils/cofe_solver_2.v | 4 ++--
coq-actris.opam | 2 +-
multris/channel/proto.v | 2 +-
multris/channel/proto_model.v | 4 ++--
multris/utils/cofe_solver_2.v | 4 ++--
7 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/actris/channel/proto.v b/actris/channel/proto.v
index 531c871..bb3e9c6 100644
--- a/actris/channel/proto.v
+++ b/actris/channel/proto.v
@@ -526,7 +526,7 @@ Section proto.
destruct (iProto_case p1) as [->|(a&m&->)].
{ by rewrite !left_id. }
rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv.
- f_contractive. apply IH; eauto using dist_le with lia.
+ f_contractive. apply IH; eauto using dist_lt.
Qed.
Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
Proof. apply (ne_proper_2 _). Qed.
diff --git a/actris/channel/proto_model.v b/actris/channel/proto_model.v
index 9f73151..ed17291 100644
--- a/actris/channel/proto_model.v
+++ b/actris/channel/proto_model.v
@@ -213,7 +213,7 @@ Proof.
induction (lt_wf n) as [n _ IH]=>
PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
- apply proto_map_aux_contractive; constructor=> n' ?. symmetry. apply: IH. lia.
+ apply proto_map_aux_contractive; constructor=> n' ?. symmetry. by apply: IH.
Qed.
Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
@@ -241,7 +241,7 @@ Proof.
destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=.
apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
- apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_le with lia.
+ apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_lt.
Qed.
Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
diff --git a/actris/utils/cofe_solver_2.v b/actris/utils/cofe_solver_2.v
index 7a2425b..43a65db 100644
--- a/actris/utils/cofe_solver_2.v
+++ b/actris/utils/cofe_solver_2.v
@@ -14,8 +14,8 @@ Global Existing Instance solution_2_cofe.
Section cofe_solver_2.
Context (F : ofe → oFunctor).
Context `{Fcontr : !∀ T, oFunctorContractive (F T)}.
- Context `{Fcofe : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
- Context `{Finh : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
+ Context `{Fcofe : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
+ Context `{Finh : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
Notation map := (oFunctor_map (F _)).
Definition F_2 (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : oFunctor :=
diff --git a/coq-actris.opam b/coq-actris.opam
index 05d5994..9513402 100644
--- a/coq-actris.opam
+++ b/coq-actris.opam
@@ -8,7 +8,7 @@ bug-reports: "https://gitlab.mpi-sws.org/iris/actris/issues"
dev-repo: "git+https://gitlab.mpi-sws.org/iris/actris.git"
depends: [
- "coq-iris-heap-lang" { (= "dev.2025-02-27.1.c773500a") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2025-03-28.0.fa344cbe") | (= "dev") }
]
build: ["./make-package" "actris" "-j%{jobs}%"]
diff --git a/multris/channel/proto.v b/multris/channel/proto.v
index 3dc1441..4b8df7a 100644
--- a/multris/channel/proto.v
+++ b/multris/channel/proto.v
@@ -389,7 +389,7 @@ Section proto.
destruct (iProto_case p1) as [->|(a&i&m&->)].
{ by rewrite !left_id. }
rewrite !iProto_app_message. f_equiv=> v p' /=. do 4 f_equiv.
- f_contractive. apply IH; eauto using dist_le with lia.
+ f_contractive. apply IH; eauto using dist_lt.
Qed.
Global Instance iProto_app_proper : Proper ((≡) ==> (≡) ==> (≡)) (@iProto_app Σ V).
Proof. apply (ne_proper_2 _). Qed.
diff --git a/multris/channel/proto_model.v b/multris/channel/proto_model.v
index 77a71e1..25fb596 100644
--- a/multris/channel/proto_model.v
+++ b/multris/channel/proto_model.v
@@ -214,7 +214,7 @@ Proof.
induction (lt_wf n) as [n _ IH]=>
PROPn Hcn PROPn' Hcn' PROP Hc PROP' Hc' gn g p.
etrans; [apply equiv_dist, (fixpoint_unfold (proto_map_aux_2 gn g))|].
- apply proto_map_aux_contractive; constructor=> n' ?. symmetry. apply: IH. lia.
+ apply proto_map_aux_contractive. constructor=> n' ?. symmetry. by apply: IH.
Qed.
Lemma proto_map_end {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn : PROPn' -n> PROPn) (g : PROP -n> PROP') :
@@ -242,7 +242,7 @@ Proof.
destruct (proto_case p) as [->|(a & m & ->)]; [by rewrite !proto_map_end|].
rewrite !proto_map_message /=.
apply proto_message_ne=> // v p' /=. f_equiv; [done|]. f_equiv.
- apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_le with lia.
+ apply Next_contractive; dist_later_intro as n' Hn'; eauto using dist_lt.
Qed.
Lemma proto_map_ext {V} `{!Cofe PROPn, !Cofe PROPn', !Cofe PROP, !Cofe PROP'}
(gn1 gn2 : PROPn' -n> PROPn) (g1 g2 : PROP -n> PROP') p :
diff --git a/multris/utils/cofe_solver_2.v b/multris/utils/cofe_solver_2.v
index 7a2425b..43a65db 100644
--- a/multris/utils/cofe_solver_2.v
+++ b/multris/utils/cofe_solver_2.v
@@ -14,8 +14,8 @@ Global Existing Instance solution_2_cofe.
Section cofe_solver_2.
Context (F : ofe → oFunctor).
Context `{Fcontr : !∀ T, oFunctorContractive (F T)}.
- Context `{Fcofe : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
- Context `{Finh : !∀ `{!Cofe T, Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
+ Context `{Fcofe : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Cofe (oFunctor_car (F T) Bn B)}.
+ Context `{Finh : !∀ `{!Cofe T, !Cofe Bn, !Cofe B}, Inhabited (oFunctor_car (F T) Bn B)}.
Notation map := (oFunctor_map (F _)).
Definition F_2 (An : ofe) `{!Cofe An} (A : ofe) `{!Cofe A} : oFunctor :=
--
GitLab