From 1b9dfa34e33b7d3aeb473dbfce746fef82e79221 Mon Sep 17 00:00:00 2001 From: Dan Frumin Date: Thu, 5 Oct 2017 18:08:53 +0200 Subject: [PATCH] Move out the `bin_log_related_seq` lemma --- theories/examples/various.v | 17 ----------------- theories/logrel/fundamental_binary.v | 16 ++++++++++++++++ 2 files changed, 16 insertions(+), 17 deletions(-) diff --git a/theories/examples/various.v b/theories/examples/various.v index 6e73521..313d2fa 100644 --- a/theories/examples/various.v +++ b/theories/examples/various.v @@ -6,23 +6,6 @@ From iris.proofmode Require Import tactics. From iris.algebra Require Import csum agree excl. From iris_logrel Require Import logrel. -Lemma bin_log_related_seq `{logrelG Σ} τ1 E Δ Γ e1 e2 e1' e2' τ2 -`{Closed ∅ e2} `{Closed ∅ e2'} : - ↑logrelN ⊆ E → - {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗ - {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗ - {E,E;Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2. -Proof. - iIntros (?) "He1 He2". - rel_bind_l e1. - rel_bind_r e1'. - iApply (related_bind with "He1 [He2]"). - iIntros (?) "? /=". - rel_rec_l. - rel_rec_r. - done. -Qed. - Section refinement. Context `{logrelG Σ}. Notation D := (prodC valC valC -n> iProp Σ). diff --git a/theories/logrel/fundamental_binary.v b/theories/logrel/fundamental_binary.v index 5c6c5ca..1412342 100644 --- a/theories/logrel/fundamental_binary.v +++ b/theories/logrel/fundamental_binary.v @@ -197,6 +197,22 @@ Section masked. iApply ("Ht" with "Hj"). Qed. + Lemma bin_log_related_seq Δ Γ e1 e2 e1' e2' τ1 τ2 `{Closed ∅ e2} `{Closed ∅ e2'} : + ↑logrelN ⊆ E → + {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗ + {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗ + {E,E;Δ;Γ} ⊨ (e1;; e2) ≤log≤ (e1';; e2') : τ2. + Proof. + iIntros (?) "He1 He2". + rel_bind_l e1. + rel_bind_r e1'. + iApply (related_bind with "He1 [He2]"). + iIntros (?) "? /=". + rel_rec_l. + rel_rec_r. + done. + Qed. + Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 : ↑ logrelN ⊆ E → {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ1 -∗ -- GitLab