From 30a89e569e304df67a6fc2ea14d7b0153b3d8327 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 9 Mar 2017 22:48:00 +0100
Subject: [PATCH] Use the new LimitPreserving stuff.
It is still not as nice as it could be; we need more automation to
prove Propers.
---
theories/typing/fixpoint.v | 31 ++++++++++++++++---------------
theories/typing/type.v | 23 ++++++++---------------
2 files changed, 24 insertions(+), 30 deletions(-)
diff --git a/theories/typing/fixpoint.v b/theories/typing/fixpoint.v
index f536bef5..e2f2e057 100644
--- a/theories/typing/fixpoint.v
+++ b/theories/typing/fixpoint.v
@@ -36,15 +36,14 @@ Section fixpoint.
- exists bool. apply _.
- done.
- (* If Copy was an Iris assertion, this would be trivial -- we'd just
- use entails_lim once. However, on the Coq side, it is more convenient
- as a record -- so this is where we pay. *)
- intros c Hc. split.
- + intros tid vl. rewrite /PersistentP. entails_lim c; [solve_proper..|].
- intros. apply (Hc n).
- + intros κ tid E F l q ? ?. entails_lim c; first solve_proper.
- * solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
- * intros n. apply (Hc n); first done. erewrite ty_size_ne; first done.
- rewrite conv_compl. done.
+ use limit_preserving_and directly. However, on the Coq side, it is
+ more convenient as a record -- so this is where we pay. *)
+ eapply (limit_preserving_ext (λ _, _ ∧ _)).
+ { split; (intros [H1 H2]; split; [apply H1|apply H2]). }
+ apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?).
+ { apply uPred.limit_preserving_PersistentP; solve_proper. }
+ apply limit_preserving_impl, uPred.limit_preserving_entails;
+ solve_proper_core ltac:(fun _ => eapply ty_size_ne || f_equiv).
Qed.
Global Instance fixpoint_send :
@@ -55,7 +54,8 @@ Section fixpoint.
- apply send_equiv.
- exists bool. apply _.
- done.
- - intros c Hc ???. entails_lim c; [solve_proper..|]. intros n. apply Hc.
+ - repeat (apply limit_preserving_forall=> ?).
+ apply uPred.limit_preserving_entails; solve_proper.
Qed.
Global Instance fixpoint_sync :
@@ -66,7 +66,8 @@ Section fixpoint.
- apply sync_equiv.
- exists bool. apply _.
- done.
- - intros c Hc ????. entails_lim c; [solve_proper..|]. intros n. apply Hc.
+ - repeat (apply limit_preserving_forall=> ?).
+ apply uPred.limit_preserving_entails; solve_proper.
Qed.
Lemma fixpoint_unfold_eqtype E L : eqtype E L (type_fixpoint T) (T (type_fixpoint T)).
@@ -90,8 +91,8 @@ Section subtyping.
- intros ?? EQ ?. etrans; last done. by apply equiv_subtype.
- by eexists _.
- intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12.
- - intros c Hc. rewrite /subtype. entails_lim c; [solve_proper..|].
- intros n. apply Hc.
+ - repeat (apply limit_preserving_forall=> ?).
+ apply uPred.limit_preserving_entails; solve_proper.
Qed.
Lemma fixpoint_proper T1 `{TypeContractive T1} T2 `{TypeContractive T2} :
@@ -103,8 +104,8 @@ Section subtyping.
- intros ?? EQ ?. etrans; last done. by apply equiv_eqtype.
- by eexists _.
- intros. setoid_rewrite (fixpoint_unfold_eqtype T2). by apply H12.
- - intros c Hc. split; rewrite /subtype; (entails_lim c; [solve_proper..|]);
- intros n; apply Hc.
+ - apply limit_preserving_and; repeat (apply limit_preserving_forall=> ?);
+ apply uPred.limit_preserving_entails; solve_proper.
Qed.
Lemma fixpoint_unfold_subtype_l ty T `{TypeContractive T} :
diff --git a/theories/typing/type.v b/theories/typing/type.v
index a7e0ecf1..6c34dabf 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -152,23 +152,16 @@ Section ofe.
Global Instance type_cofe : Cofe typeC.
Proof.
- apply: (iso_cofe_subtype P type_pack type_unpack).
+ apply (iso_cofe_subtype' P type_pack type_unpack).
+ - by intros [].
- split; [by destruct 1|by intros [[??] ?]; constructor].
- by intros [].
- - intros ? c. rewrite /P /=. split_and!.
- (* TODO: Can we do these proofs without effectively going into the model? *)
- + intros κ tid l. apply uPred.entails_equiv_and, equiv_dist=>n.
- setoid_rewrite conv_compl; simpl.
- apply equiv_dist, uPred.entails_equiv_and, ty_shr_persistent.
- + intros tid vl. apply uPred.entails_equiv_and, equiv_dist=>n.
- repeat setoid_rewrite conv_compl at 1. simpl.
- apply equiv_dist, uPred.entails_equiv_and, ty_size_eq.
- + intros E κ l tid q ?. apply uPred.entails_equiv_and, equiv_dist=>n.
- setoid_rewrite conv_compl; simpl.
- by apply equiv_dist, uPred.entails_equiv_and, ty_share.
- + intros κ κ' tid l. apply uPred.entails_equiv_and, equiv_dist=>n.
- setoid_rewrite conv_compl; simpl.
- apply equiv_dist, uPred.entails_equiv_and, ty_shr_mono.
+ - (* TODO: automate this *)
+ repeat apply limit_preserving_and; repeat (apply limit_preserving_forall; intros ?).
+ + apply uPred.limit_preserving_PersistentP=> n ty1 ty2 Hty; apply Hty.
+ + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty. apply Hty. by rewrite Hty.
+ + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
+ + apply uPred.limit_preserving_entails=> n ty1 ty2 Hty; repeat f_equiv; apply Hty.
Qed.
Inductive st_equiv' (ty1 ty2 : simple_type) : Prop :=
--
GitLab