From 223250f1647eabf16a4d1fcdd456b61e7f25614c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 7 Mar 2023 18:18:37 +0100
Subject: [PATCH] Fix for contractive tweaks.
---
theories/logrel/session_types.v | 5 ++---
theories/logrel/term_types.v | 4 ++--
2 files changed, 4 insertions(+), 5 deletions(-)
diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 23b5054..95af463 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -114,9 +114,8 @@ Section session_types.
intros Ss Ts Heq. rewrite /lty_choice.
do 2 f_equiv. f_equiv => i.
rewrite !lookup_total_alt.
- specialize (Heq i).
- destruct (Ss !! i), (Ts !! i);
- [ f_contractive | contradiction | contradiction | done ].
+ specialize (Heq i). destruct (Ss !! i), (Ts !! i); simplify_eq/=; try done.
+ f_contractive.
- f_equiv. split; intros H; eauto.
- by rewrite Heq.
Qed.
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index 1b6a178..5ab5f70 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -115,7 +115,7 @@ Section term_types.
Proof.
intros A A' ? B B' ?. apply Ltty_ne=> v. f_equiv=> w.
f_equiv; [by f_contractive|].
- apply (wp_contractive _ _ _ _ _)=> v'. destruct n=> //=; by f_equiv.
+ apply (wp_contractive _ _ _ _ _)=> v'. f_contractive_core n' Hn'. by f_equiv.
Qed.
Global Instance lty_arr_ne `{heapGS Σ} : NonExpansive2 lty_arr.
Proof. solve_proper. Qed.
@@ -135,7 +135,7 @@ Section term_types.
Proof.
intros F F' A. apply Ltty_ne=> w. f_equiv=> B.
apply (wp_contractive _ _ _ _ _)=> u. specialize (A B).
- by destruct n as [|n]; simpl.
+ f_contractive_core n' Hn'. by f_equiv.
Qed.
Global Instance lty_forall_ne `{heapGS Σ} k n :
Proper (pointwise_relation _ (dist n) ==> dist n) (@lty_forall Σ _ k).
--
GitLab