Commit be81fb92 authored by Ralf Jung's avatar Ralf Jung

add a tactic to automatically solve goals that show inG from subG

parent 673f0a14
Pipeline #3649 passed with stage
in 10 minutes and 37 seconds
......@@ -14,7 +14,7 @@ Class authG Σ (A : ucmraT) := AuthG {
Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (authR A) ].
Instance subG_authΣ Σ A : subG (authΣ A) Σ CMRADiscrete A authG Σ A.
Proof. intros ?%subG_inG ?. by split. Qed.
Proof. solve_inG. Qed.
Section definitions.
Context `{invG Σ, authG Σ A} {T : Type} (γ : gname).
......
......@@ -16,7 +16,7 @@ Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
Instance subG_stsΣ Σ :
subG boxΣ Σ boxG Σ.
Proof. apply subG_inG. Qed.
Proof. solve_inG. Qed.
Section box_defs.
Context `{invG Σ, boxG Σ} (N : namespace).
......
......@@ -24,7 +24,7 @@ Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
subG (gen_heapΣ L V) Σ gen_heapPreG L V Σ.
Proof. intros ?%subG_inG; split; apply _. Qed.
Proof. solve_inG. Qed.
Section definitions.
Context `{gen_heapG L V Σ}.
......
......@@ -17,6 +17,33 @@ Arguments inG_id {_ _} _.
Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (F (iPreProp Σ)).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
Ltac solve_inG :=
(* Get all assumptions *)
intros;
(* Unfold the top-level xΣ *)
lazymatch goal with
| H : subG (?xΣ _) _ |- _ => try unfold xΣ in H
| H : subG ?xΣ _ |- _ => try unfold xΣ in H
end;
(* Take apart subG for non-"atomic" lists *)
repeat match goal with
| H : subG (gFunctors.app _ _) _ |- _ => apply subG_inv in H; destruct H
end;
(* Try to turn singleton subG into inG; but also keep the subG for typeclass
resolution -- to keep them, we put them onto the goal. *)
repeat match goal with
| H : subG _ _ |- _ => move:(H); (apply subG_inG in H || clear H)
end;
(* Again get all assumptions *)
intros;
(* We support two kinds of goals: Things convertible to inG;
and records with inG and typeclass fields. Try to solve the
first case. *)
try done;
(* That didn't work, now we're in for the second case. *)
split; (assumption || by apply _).
(** * Definition of the connective [own] *)
Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
iprod_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
......
......@@ -10,7 +10,7 @@ Definition savedPropΣ (F : cFunctor) : gFunctors :=
#[ GFunctor (agreeRF ( F)) ].
Instance subG_savedPropΣ {Σ F} : subG (savedPropΣ F) Σ savedPropG Σ F.
Proof. apply subG_inG. Qed.
Proof. solve_inG. Qed.
Definition saved_prop_own `{savedPropG Σ F}
(γ : gname) (x : F (iProp Σ)) : iProp Σ :=
......
......@@ -13,7 +13,7 @@ Class stsG Σ (sts : stsT) := StsG {
Definition stsΣ (sts : stsT) : gFunctors := #[ GFunctor (stsR sts) ].
Instance subG_stsΣ Σ sts :
subG (stsΣ sts) Σ Inhabited (sts.state sts) stsG Σ sts.
Proof. intros ?%subG_inG ?. by split. Qed.
Proof. solve_inG. Qed.
Section definitions.
Context `{stsG Σ sts} (γ : gname).
......
......@@ -12,7 +12,7 @@ Class heapPreG Σ := HeapPreG {
Definition heapΣ : gFunctors := #[invΣ; gen_heapΣ loc val].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. intros [? ?]%subG_inv; split; apply _. Qed.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
( `{heapG Σ}, True WP e {{ v, ⌜φ v }})
......
......@@ -8,7 +8,6 @@ From iris.heap_lang.lib.barrier Require Import protocol.
Set Default Proof Using "Type".
(** The CMRAs/functors we need. *)
(* Not bundling heapG, as it may be shared with other users. *)
Class barrierG Σ := BarrierG {
barrier_stsG :> stsG Σ sts;
barrier_savedPropG :> savedPropG Σ idCF;
......@@ -16,7 +15,7 @@ Class barrierG Σ := BarrierG {
Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ idCF].
Instance subG_barrierΣ {Σ} : subG barrierΣ Σ barrierG Σ.
Proof. intros [? [? _]%subG_inv]%subG_inv. split; apply _. Qed.
Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
......
......@@ -17,7 +17,7 @@ Class mcounterG Σ := MCounterG { mcounter_inG :> inG Σ (authR mnatUR) }.
Definition mcounterΣ : gFunctors := #[GFunctor (authR mnatUR)].
Instance subG_mcounterΣ {Σ} : subG mcounterΣ Σ mcounterG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Proof. solve_inG. Qed.
Section mono_proof.
Context `{!heapG Σ, !mcounterG Σ} (N : namespace).
......
......@@ -23,7 +23,7 @@ Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitC) }.
Definition spawnΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_spawnΣ {Σ} : subG spawnΣ Σ spawnG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
......
......@@ -18,7 +18,7 @@ Class lockG Σ := LockG { lock_tokG :> inG Σ (exclR unitC) }.
Definition lockΣ : gFunctors := #[GFunctor (exclR unitC)].
Instance subG_lockΣ {Σ} : subG lockΣ Σ lockG Σ.
Proof. intros ?%subG_inG. split; apply _. Qed.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ} (N : namespace).
......
......@@ -34,7 +34,7 @@ Definition tlockΣ : gFunctors :=
#[ GFunctor (authR (prodUR (optionUR (exclR natC)) (gset_disjUR nat))) ].
Instance subG_tlockΣ {Σ} : subG tlockΣ Σ tlockG Σ.
Proof. by intros ?%subG_inG. Qed.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !tlockG Σ} (N : namespace).
......
......@@ -19,9 +19,7 @@ Class invPreG (Σ : gFunctors) : Set := WsatPreG {
}.
Instance subG_invΣ {Σ} : subG invΣ Σ invPreG Σ.
Proof.
intros [?%subG_inG [?%subG_inG ?%subG_inG]%subG_inv]%subG_inv; by constructor.
Qed.
Proof. solve_inG. Qed.
(* Allocation *)
Lemma wsat_alloc `{invPreG Σ} : (|==> _ : invG Σ, wsat ownE )%I.
......
......@@ -29,7 +29,7 @@ Class ownPPreG' (Λstate : Type) (Σ : gFunctors) : Set := IrisPreG {
Notation ownPPreG Λ Σ := (ownPPreG' (state Λ) Σ).
Instance subG_ownPΣ {Λstate Σ} : subG (ownPΣ Λstate) Σ ownPPreG' Λstate Σ.
Proof. intros [??%subG_inG]%subG_inv; constructor; apply _. Qed.
Proof. solve_inG. Qed.
(** Ownership *)
Definition ownP `{ownPG' Λstate Σ} (σ : Λstate) : iProp Σ :=
......
......@@ -75,7 +75,7 @@ End M.
Class counterG Σ := CounterG { counter_tokG :> inG Σ M_UR }.
Definition counterΣ : gFunctors := #[GFunctor M_UR].
Instance subG_counterΣ {Σ} : subG counterΣ Σ counterG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Proof. solve_inG. Qed.
Section proof.
Context `{!heapG Σ, !counterG Σ}.
......
......@@ -17,7 +17,7 @@ Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
Definition oneShotΣ (F : cFunctor) : gFunctors :=
#[ GFunctor (csumRF (exclRF unitC) (agreeRF ( F))) ].
Instance subG_oneShotΣ {Σ F} : subG (oneShotΣ F) Σ oneShotG Σ F.
Proof. apply subG_inG. Qed.
Proof. solve_inG. Qed.
Definition client eM eW1 eW2 : expr :=
let: "b" := newbarrier #() in
......
......@@ -27,7 +27,7 @@ Definition Shot (n : Z) : one_shotR := (Cinr (to_agree n) : one_shotR).
Class one_shotG Σ := { one_shot_inG :> inG Σ one_shotR }.
Definition one_shotΣ : gFunctors := #[GFunctor one_shotR].
Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ one_shotG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Proof. solve_inG. Qed.
Section proof.
Set Default Proof Using "Type*".
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment