From 60eeca59ead87a980920790db0577f2ca7252aef Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2017 12:19:06 +0100
Subject: [PATCH] Declare some Params instances to speed up rewrites.
---
theories/typing/fixpoint.v | 5 ++-
theories/typing/type.v | 65 ++++++++++++++++++--------------------
2 files changed, 32 insertions(+), 38 deletions(-)
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index 308fb517..f536bef5 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -8,7 +8,7 @@ Section fixpoint_def.
Context (T : type → type) {HT: TypeContractive T}.
Global Instance type_inhabited : Inhabited type := populate bool.
-
+
Local Instance type_2_contractive : Contractive (Nat.iter 2 T).
Proof using Type*.
intros n ? **. simpl.
@@ -19,7 +19,7 @@ Section fixpoint_def.
End fixpoint_def.
Lemma type_fixpoint_ne `{typeG Σ} (T1 T2 : type → type)
- `{!TypeContractive T1, !TypeContractive T2} n :
+ `{!TypeContractive T1, !TypeContractive T2} n :
(∀ t, T1 t ≡{n}≡ T2 t) → type_fixpoint T1 ≡{n}≡ type_fixpoint T2.
Proof. eapply fixpointK_ne; apply type_contractive_ne, _. Qed.
@@ -107,7 +107,6 @@ Section subtyping.
intros n; apply Hc.
Qed.
- (* FIXME: Some rewrites here are slower than one would expect. *)
Lemma fixpoint_unfold_subtype_l ty T `{TypeContractive T} :
subtype E L ty (T (type_fixpoint T)) → subtype E L ty (type_fixpoint T).
Proof. intros. by rewrite fixpoint_unfold_eqtype. Qed.
diff --git a/theories/typing/type.v b/theories/typing/type.v
index e083ca78..bebb4d58 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -468,12 +468,24 @@ Section type.
Qed.
End type.
-Section subtyping.
- Context `{typeG Σ}.
- Definition type_incl (ty1 ty2 : type) : iProp Σ :=
+Definition type_incl `{typeG Σ} (ty1 ty2 : type) : iProp Σ :=
(⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
(□ ∀ tid vl, ty1.(ty_own) tid vl -∗ ty2.(ty_own) tid vl) ∗
(□ ∀ κ tid l, ty1.(ty_shr) κ tid l -∗ ty2.(ty_shr) κ tid l))%I.
+Instance: Params (@type_incl) 2.
+(* Typeclasses Opaque type_incl. *)
+
+Definition subtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+ elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ type_incl ty1 ty2.
+Instance: Params (@subtype) 4.
+
+(* TODO: The prelude should have a symmetric closure. *)
+Definition eqtype `{typeG Σ} (E : elctx) (L : llctx) (ty1 ty2 : type) : Prop :=
+ subtype E L ty1 ty2 ∧ subtype E L ty2 ty1.
+Instance: Params (@eqtype) 4.
+
+Section subtyping.
+ Context `{typeG Σ}.
Global Instance type_incl_ne : NonExpansive2 type_incl.
Proof.
@@ -482,7 +494,6 @@ Section subtyping.
Qed.
Global Instance type_incl_persistent ty1 ty2 : PersistentP (type_incl ty1 ty2) := _.
- (* Typeclasses Opaque type_incl. *)
Lemma type_incl_refl ty : type_incl ty ty.
Proof. iSplit; first done. iSplit; iAlways; iIntros; done. Qed.
@@ -497,31 +508,20 @@ Section subtyping.
- iApply "Hs23". iApply "Hs12". done.
Qed.
- Context (E : elctx) (L : llctx).
-
- Definition subtype (ty1 ty2 : type) : Prop :=
- elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗ type_incl ty1 ty2.
-
- Lemma subtype_refl ty : subtype ty ty.
+ Lemma subtype_refl E L ty : subtype E L ty ty.
Proof. iIntros. iApply type_incl_refl. Qed.
- Global Instance subtype_preorder : PreOrder subtype.
+ Global Instance subtype_preorder E L : PreOrder (subtype E L).
Proof.
split; first by intros ?; apply subtype_refl.
intros ty1 ty2 ty3 H12 H23. iIntros.
- iApply (type_incl_trans with "[] []").
- - iApply (H12 with "[] []"); done.
- - iApply (H23 with "[] []"); done.
+ iApply type_incl_trans. by iApply H12. by iApply H23.
Qed.
- Lemma equiv_subtype ty1 ty2 : ty1 ≡ ty2 → subtype ty1 ty2.
+ Lemma equiv_subtype E L ty1 ty2 : ty1 ≡ ty2 → subtype E L ty1 ty2.
Proof. unfold subtype, type_incl=>EQ. setoid_rewrite EQ. apply subtype_refl. Qed.
- (* TODO: The prelude should have a symmetric closure. *)
- Definition eqtype (ty1 ty2 : type) : Prop :=
- subtype ty1 ty2 ∧ subtype ty2 ty1.
-
- Lemma eqtype_unfold ty1 ty2 :
- eqtype ty1 ty2 ↔
+ Lemma eqtype_unfold E L ty1 ty2 :
+ eqtype E L ty1 ty2 ↔
(elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
(⌜ty1.(ty_size) = ty2.(ty_size)⌝ ∗
(□ ∀ tid vl, ty1.(ty_own) tid vl ↔ ty2.(ty_own) tid vl) ∗
@@ -545,17 +545,17 @@ Section subtyping.
+ iIntros "!#* H". by iApply "Hshr".
Qed.
- Lemma eqtype_refl ty : eqtype ty ty.
+ Lemma eqtype_refl E L ty : eqtype E L ty ty.
Proof. by split. Qed.
- Lemma equiv_eqtype ty1 ty2 : ty1 ≡ ty2 → eqtype ty1 ty2.
+ Lemma equiv_eqtype E L ty1 ty2 : ty1 ≡ ty2 → eqtype E L ty1 ty2.
Proof. by split; apply equiv_subtype. Qed.
- Global Instance subtype_proper :
- Proper (eqtype ==> eqtype ==> iff) subtype.
+ Global Instance subtype_proper E L :
+ Proper (eqtype E L ==> eqtype E L ==> iff) (subtype E L).
Proof. intros ??[] ??[]. split; intros; by etrans; [|etrans]. Qed.
- Global Instance eqtype_equivalence : Equivalence eqtype.
+ Global Instance eqtype_equivalence E L : Equivalence (eqtype E L).
Proof.
split.
- by split.
@@ -563,21 +563,16 @@ Section subtyping.
- intros ??? H1 H2. split; etrans; (apply H1 || apply H2).
Qed.
- Lemma subtype_simple_type (st1 st2 : simple_type) :
+ Lemma subtype_simple_type E L (st1 st2 : simple_type) :
(∀ tid vl, elctx_interp_0 E -∗ ⌜llctx_interp_0 L⌝ -∗
st1.(st_own) tid vl -∗ st2.(st_own) tid vl) →
- subtype st1 st2.
+ subtype E L st1 st2.
Proof.
intros Hst. iIntros. iSplit; first done. iSplit; iAlways.
- iIntros. iApply Hst; done.
- - iIntros (???) "H".
- iDestruct "H" as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
+ - iIntros (???). iDestruct 1 as (vl) "[Hf Hown]". iExists vl. iFrame "Hf".
by iApply Hst.
Qed.
-End subtyping.
-
-Section weakening.
- Context `{typeG Σ}.
Lemma subtype_weaken E1 E2 L1 L2 ty1 ty2 :
E1 ⊆+ E2 → L1 ⊆+ L2 →
@@ -589,7 +584,7 @@ Section weakening.
- iDestruct "HL" as %HL. iPureIntro. intros ??. apply HL.
eauto using elem_of_submseteq.
Qed.
-End weakening.
+End subtyping.
Hint Resolve subtype_refl eqtype_refl : lrust_typing.
Hint Opaque subtype eqtype : lrust_typing.
--
GitLab