From 805e38decef797b7365665bd9c9c6596e32e22ba Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Mon, 9 Jan 2017 15:35:46 +0100
Subject: [PATCH] use solve_inG tactic
---
.gitignore | 1 +
coq/ra/adequacy.v | 12 +++++-------
coq/ra/base/ghosts.v | 10 ----------
coq/ra/escrows.v | 2 +-
coq/ra/examples/circ_buffer.v | 2 +-
coq/ra/examples/message_passing.v | 2 +-
coq/ra/examples/ticket_lock.v | 2 +-
coq/ra/gps/inst_shared.v | 2 +-
coq/ra/gps/shared.v | 7 ++-----
coq/ra/persistor.v | 2 +-
coq/ra/rsl.v | 2 +-
11 files changed, 15 insertions(+), 29 deletions(-)
diff --git a/.gitignore b/.gitignore
index 0240dcae..8c0aeb80 100644
--- a/.gitignore
+++ b/.gitignore
@@ -13,6 +13,7 @@
*.synctex.gz
*.prv
*.toc
+.lia.cache
.#*
auto
*.fmt
diff --git a/coq/ra/adequacy.v b/coq/ra/adequacy.v
index c4891e46..4f642801 100644
--- a/coq/ra/adequacy.v
+++ b/coq/ra/adequacy.v
@@ -13,14 +13,12 @@ Class basePreG Σ := BasePreG {
base_preG_info :> inG Σ (authR Infos);
}.
-Definition baseΣ : gFunctors := #[ownPΣ (language.state ra_lang); foundationΣ].
+Definition baseΣ : gFunctors := #[ownPΣ (language.state ra_lang);
+ GFunctor (authR Views);
+ GFunctor (authR Hists);
+ GFunctor (authR Infos)].
Instance subG_basePreG {Σ} : subG baseΣ Σ → basePreG Σ.
-Proof.
- intros [? [[? [? ?]%subG_inv]%subG_inv _]%subG_inv]%subG_inv. split; try apply _.
- - apply (subG_inG _ _ s0).
- - apply (subG_inG _ _ s1).
- - apply (subG_inG _ _ s2).
-Qed.
+Proof. solve_inG. Qed.
Definition to_view (σ : language.state ra_lang) : Views := (Excl <$> threads σ).
Definition loc_sets (σ : language.state ra_lang) : gmap loc (gset message) :=
diff --git a/coq/ra/base/ghosts.v b/coq/ra/base/ghosts.v
index d4954460..9e5e805e 100644
--- a/coq/ra/base/ghosts.v
+++ b/coq/ra/base/ghosts.v
@@ -32,16 +32,6 @@ Class foundationG Σ :=
Definition AuthType {Σ} {T} (X : inG Σ (authR T)) := T.
-Definition foundationΣ : gFunctors :=
- #[
- GFunctor (constRF (authR Views));
- GFunctor (constRF (authR Hists));
- GFunctor (constRF (authR Infos))
- ].
-(* Instance inGF_foundationG {Σ} : subG foundationΣ Σ → foundationG Σ. *)
-(* Proof. *)
-(* Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed. *)
-
(* Todo: figure out why this is needed and get rid of it *)
Global Instance foundationG_hist_insert `{foundationG Σ} : Insert loc (excl (gset (Val * View))) (AuthType foundationG_hist) := _.
Global Instance foundationG_hist_singleton `{foundationG Σ} : SingletonM loc (excl (gset (Val * View))) (AuthType foundationG_hist) := _.
diff --git a/coq/ra/escrows.v b/coq/ra/escrows.v
index 74a982a3..b6f03774 100644
--- a/coq/ra/escrows.v
+++ b/coq/ra/escrows.v
@@ -16,7 +16,7 @@ Definition absViewΣ : gFunctors :=
#[ GFunctor (agreeRF ViewR) ].
Instance subG_absViewΣ {Σ} : subG absViewΣ Σ → absViewG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
Section AbstractView.
diff --git a/coq/ra/examples/circ_buffer.v b/coq/ra/examples/circ_buffer.v
index 13c88c9d..de7dd5c0 100644
--- a/coq/ra/examples/circ_buffer.v
+++ b/coq/ra/examples/circ_buffer.v
@@ -53,7 +53,7 @@ Section CircBuffer.
Definition cbΣ : gFunctors := #[GFunctor (constRF circBufR)].
Instance subG_cbΣ {Σ} : subG cbΣ Σ → cbG Σ.
- Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+ Proof. solve_inG. Qed.
Section Interpretation.
Context `{fG: !foundationG Σ, aG: !absViewG Σ, cirbG: !cbG Σ}.
diff --git a/coq/ra/examples/message_passing.v b/coq/ra/examples/message_passing.v
index 96225402..78b51bf3 100644
--- a/coq/ra/examples/message_passing.v
+++ b/coq/ra/examples/message_passing.v
@@ -22,7 +22,7 @@ Class mpG Σ := MpG { mp_tokG :> inG Σ (exclR unitC) }.
Definition mpΣ : gFunctors := #[GFunctor (constRF (exclR unitC))].
Instance subG_mpΣ {Σ} : subG mpΣ Σ → mpG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
Section Interpretation.
Context `{foundationG Σ} `{!absViewG Σ} `{mespG : !mpG Σ}.
diff --git a/coq/ra/examples/ticket_lock.v b/coq/ra/examples/ticket_lock.v
index 0c834fb4..440b6beb 100644
--- a/coq/ra/examples/ticket_lock.v
+++ b/coq/ra/examples/ticket_lock.v
@@ -15,7 +15,7 @@ Class tklG Σ := TklG { tkl_tokG :> inG Σ ticketLockR }.
Definition tklΣ : gFunctors := #[GFunctor (constRF ticketLockR)].
Instance subG_tklΣ {Σ} : subG tklΣ Σ → tklG Σ.
-Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
Section TicketLock.
diff --git a/coq/ra/gps/inst_shared.v b/coq/ra/gps/inst_shared.v
index 9cd14bb3..56d4ba1c 100644
--- a/coq/ra/gps/inst_shared.v
+++ b/coq/ra/gps/inst_shared.v
@@ -12,4 +12,4 @@ Notation gps_agreeG Σ Prtcl := (inG Σ (dec_agreeR (EqDecision0 := state_sort_e
Definition gps_agreeΣ Prtcl (PF : protocol_facts Prtcl) : gFunctors := #[ GFunctor (constRF ((dec_agreeR (EqDecision0 := state_sort_eqdec Prtcl%type) (state_sort Prtcl)))) ].
Instance subG_gps_agreeΣ Σ Prtcl PF : subG (gps_agreeΣ Prtcl PF) Σ → gps_agreeG Σ Prtcl.
-Proof. intros [? ?]%subG_inv. apply (subG_inG _ _ s). Qed.
\ No newline at end of file
+Proof. solve_inG. Qed.
diff --git a/coq/ra/gps/shared.v b/coq/ra/gps/shared.v
index 6c5494e1..f72dec20 100644
--- a/coq/ra/gps/shared.v
+++ b/coq/ra/gps/shared.v
@@ -81,12 +81,9 @@ Class gpsG Σ Prtcl (PF : protocol_facts Prtcl) :=
}.
Definition gpsΣ Prtcl (PF : protocol_facts Prtcl) : gFunctors :=
#[ GFunctor (constRF stateR); GFunctor (constRF (authR (optionUR (prodR fracR (dec_agreeR (state_sort Prtcl)))))) ].
+
Instance subG_gpsG {Σ} Prtcl PF : subG (gpsΣ Prtcl PF) Σ → gpsG Σ Prtcl PF.
-Proof.
- intros [? [? ?]%subG_inv]%subG_inv. split; try apply _.
- - apply (subG_inG _ _ s).
- - apply (subG_inG _ _ s0).
-Qed.
+Proof. solve_inG. Qed.
Arguments st_prst [_] _ /.
Arguments st_val [_] _ /.
diff --git a/coq/ra/persistor.v b/coq/ra/persistor.v
index 72e16cf5..c99e62af 100644
--- a/coq/ra/persistor.v
+++ b/coq/ra/persistor.v
@@ -27,7 +27,7 @@ Class persistorPreG Σ :=
persistorPreG_perinfo :> inG Σ (authR PerInfos)
}.
Instance subG_persistorPreG {Σ} : subG persistorΣ Σ → persistorPreG Σ.
-Proof. intros [? ?]%subG_inv; constructor. apply (subG_inG _ _ s). Qed.
+Proof. solve_inG. Qed.
Section Persistor.
Context `{!foundationG Σ, !persistorG Σ}.
diff --git a/coq/ra/rsl.v b/coq/ra/rsl.v
index c33237a4..76b77d52 100644
--- a/coq/ra/rsl.v
+++ b/coq/ra/rsl.v
@@ -25,7 +25,7 @@ Definition rslΣ : gFunctors
:= #[stsΣ rsl_sts; savedPropΣ (ofe_funCF Z (ofe_funCF View idCF))].
Instance subG_rslΣ {Σ} : subG rslΣ Σ → rslG Σ.
-Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
+Proof. solve_inG. Qed.
Section proof.
--
GitLab