Commit f5bceb45 authored by Ralf Jung's avatar Ralf Jung

play with avoid auto-generalization

parent 9c04e2b4
......@@ -2,6 +2,7 @@ From iris.algebra Require Import functions gmap.
From iris.base_logic.lib Require Export iprop.
From iris.algebra Require Import proofmode_classes.
Set Default Proof Using "Type".
Generalizable No Variables.
Import uPred.
(** The class [inG Σ A] expresses that the CMRA [A] is in the list of functors
......@@ -47,11 +48,11 @@ Ltac solve_inG :=
split; (assumption || by apply _).
(** * Definition of the connective [own] *)
Definition iRes_singleton `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
Definition iRes_singleton {Σ A} `{i : inG Σ A} (γ : gname) (a : A) : iResUR Σ :=
ofe_fun_singleton (inG_id i) {[ γ := cmra_transport inG_prf a ]}.
Instance: Params (@iRes_singleton) 4 := {}.
Definition own_def `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
Definition own_def {Σ A} `{inG Σ A} (γ : gname) (a : A) : iProp Σ :=
uPred_ownM (iRes_singleton γ a).
Definition own_aux : seal (@own_def). by eexists. Qed.
Definition own {Σ A i} := own_aux.(unseal) Σ A i.
......@@ -61,7 +62,7 @@ Typeclasses Opaque own.
(** * Properties about ghost ownership *)
Section global.
Context `{inG Σ A}.
Context {Σ A} `{inG Σ A}.
Implicit Types a : A.
(** ** Properties of [iRes_singleton] *)
......@@ -196,7 +197,7 @@ Arguments own_update {_ _} [_] _ _ _ _.
Arguments own_update_2 {_ _} [_] _ _ _ _ _.
Arguments own_update_3 {_ _} [_] _ _ _ _ _ _.
Lemma own_unit A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Lemma own_unit {Σ} A `{inG Σ (A:ucmraT)} γ : (|==> own γ ε)%I.
Proof.
rewrite /uPred_valid /bi_emp_valid (ownM_unit emp) !own_eq /own_def.
apply bupd_ownM_update, ofe_fun_singleton_update_empty.
......@@ -206,13 +207,13 @@ Proof.
Qed.
(** Big op class instances *)
Instance own_cmra_sep_homomorphism `{inG Σ (A:ucmraT)} :
Instance own_cmra_sep_homomorphism {Σ A} `{inG Σ (A:ucmraT)} γ :
WeakMonoidHomomorphism op uPred_sep () (own γ).
Proof. split; try apply _. apply own_op. Qed.
(** Proofmode class instances *)
Section proofmode_classes.
Context `{inG Σ A}.
Context {Σ A} `{inG Σ A}.
Implicit Types a b : A.
Global Instance into_sep_own γ a b1 b2 :
......
......@@ -3,13 +3,14 @@ From iris.bi.lib Require Import fixpoint.
From stdpp Require Import coPset namespaces.
From iris.proofmode Require Import coq_tactics tactics reduction.
Set Default Proof Using "Type".
Generalizable No Variables.
(** Conveniently split a conjunction on both assumption and conclusion. *)
Local Tactic Notation "iSplitWith" constr(H) :=
iApply (bi.and_parallel with H); iSplit; iIntros H.
Section definition.
Context `{BiFUpd PROP} {TA TB : tele}.
Context {PROP} `{BiFUpd PROP} {TA TB : tele}.
Implicit Types
(Eo Ei : coPset) (* outer/inner masks *)
(α : TA PROP) (* atomic pre-condition *)
......@@ -88,7 +89,7 @@ End definition.
(** Seal it *)
Definition atomic_update_aux : seal (@atomic_update_def). by eexists. Qed.
Definition atomic_update `{BiFUpd PROP} {TA TB : tele} := atomic_update_aux.(unseal) PROP _ TA TB.
Definition atomic_update {PROP} `{BiFUpd PROP} {TA TB : tele} := atomic_update_aux.(unseal) PROP _ TA TB.
Definition atomic_update_eq :
@atomic_update = @atomic_update_def := atomic_update_aux.(seal_eq).
......@@ -221,7 +222,7 @@ Notation "'AACC' '<<' α 'ABORT' P '>>' @ Eo , Ei '<<' β , 'COMM' Φ '>>'" :=
(** Lemmas about AU *)
Section lemmas.
Context `{BiFUpd PROP} {TA TB : tele}.
Context {PROP} `{BiFUpd PROP} {TA TB : tele}.
Implicit Types (α : TA PROP) (β Φ : TA TB PROP) (P : PROP).
Local Existing Instance atomic_update_pre_mono.
......@@ -425,7 +426,7 @@ End lemmas.
(** ProofMode support for atomic updates *)
Section proof_mode.
Context `{BiFUpd PROP} {TA TB : tele}.
Context {PROP} `{BiFUpd PROP} {TA TB : tele}.
Implicit Types (α : TA PROP) (β Φ : TA TB PROP) (P : PROP).
Lemma tac_aupd_intro Γp Γs n α β Eo Ei Φ P :
......
......@@ -4,6 +4,7 @@ From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.bi.lib Require Import fractional.
Set Default Proof Using "Type".
Generalizable No Variables.
(** A general logically atomic interface for a heap. *)
Class atomic_heap {Σ} `{!heapG Σ} := AtomicHeap {
......@@ -69,7 +70,7 @@ Definition primitive_cas : val :=
λ: "l" "e1" "e2", CAS "l" "e1" "e2".
Section proof.
Context `{!heapG Σ}.
Context {Σ} `{!heapG Σ}.
Lemma primitive_alloc_spec (v : val) :
{{{ True }}} primitive_alloc v {{{ l, RET #l; l v }}}.
......@@ -111,7 +112,7 @@ End proof.
(* NOT an instance because users should choose explicitly to use it
(using [Explicit Instance]). *)
Definition primitive_atomic_heap `{!heapG Σ} : atomic_heap Σ :=
Definition primitive_atomic_heap {Σ} `{!heapG Σ} : atomic_heap Σ :=
{| alloc_spec := primitive_alloc_spec;
load_spec := primitive_load_spec;
store_spec := primitive_store_spec;
......
From iris.heap_lang Require Export spawn.
From iris.heap_lang Require Import proofmode notation.
Set Default Proof Using "Type".
Generalizable No Variables.
Import uPred.
Definition parN : namespace := nroot .@ "par".
......@@ -16,7 +17,7 @@ Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !spawnG Σ}.
Context {Σ} `{!heapG Σ, !spawnG Σ}.
(* Notice that this allows us to strip a later *after* the two Ψ have been
brought together. That is strictly stronger than first stripping a later
......
......@@ -5,6 +5,7 @@ From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import excl.
Set Default Proof Using "Type".
Generalizable No Variables.
Definition spawn : val :=
λ: "f",
......@@ -27,7 +28,7 @@ Proof. solve_inG. Qed.
(** Now we come to the Iris part of the proof. *)
Section proof.
Context `{!heapG Σ, !spawnG Σ} (N : namespace).
Context {Σ} `{!heapG Σ, !spawnG Σ} (N : namespace).
Definition spawn_inv (γ : gname) (l : loc) (Ψ : val iProp Σ) : iProp Σ :=
( lv, l lv (lv = NONEV
......
......@@ -4,10 +4,11 @@ From iris.proofmode Require Import tactics classes.
From iris.bi.lib Require Export atomic.
From iris.bi Require Import telescopes.
Set Default Proof Using "Type".
Generalizable No Variables.
(* This hard-codes the inner mask to be empty, because we have yet to find an
example where we want it to be anything else. *)
Definition atomic_wp `{irisG Λ Σ} {TA TB : tele}
Definition atomic_wp {Λ Σ} `{irisG Λ Σ} {TA TB : tele}
(e: expr Λ) (* expression *)
(Eo : coPset) (* (outer) mask *)
(α: TA iProp Σ) (* atomic pre-condition *)
......@@ -94,7 +95,7 @@ Notation "'<<<' α '>>>' e @ Eo '<<<' β , 'RET' v '>>>'" :=
(** Theory *)
Section lemmas.
Context `{irisG Λ Σ} {TA TB : tele}.
Context {Λ Σ} `{irisG Λ Σ} {TA TB : tele}.
Notation iProp := (iProp Σ).
Implicit Types (α : TA iProp) (β : TA TB iProp) (f : TA TB val Λ).
......
......@@ -3,6 +3,7 @@ From iris.program_logic Require Export language.
From iris.bi Require Export weakestpre.
From iris.proofmode Require Import base tactics classes.
Set Default Proof Using "Type".
Generalizable No Variables.
Import uPred.
Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
......@@ -22,7 +23,7 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
}.
Global Opaque iris_invG.
Definition wp_pre `{irisG Λ Σ} (s : stuckness)
Definition wp_pre {Λ Σ} `{irisG Λ Σ} (s : stuckness)
(wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ := λ E e1 Φ,
match to_val e1 with
......@@ -36,20 +37,20 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
[ list] i ef efs, wp ef fork_post
end%I.
Local Instance wp_pre_contractive `{irisG Λ Σ} s : Contractive (wp_pre s).
Local Instance wp_pre_contractive {Λ Σ} `{irisG Λ Σ} s : Contractive (wp_pre s).
Proof.
rewrite /wp_pre=> n wp wp' Hwp E e1 Φ.
repeat (f_contractive || f_equiv); apply Hwp.
Qed.
Definition wp_def `{irisG Λ Σ} (s : stuckness) :
Definition wp_def {Λ Σ} `{irisG Λ Σ} (s : stuckness) :
coPset expr Λ (val Λ iProp Σ) iProp Σ := fixpoint (wp_pre s).
Definition wp_aux `{irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
Instance wp' `{irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
Definition wp_eq `{irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
Definition wp_aux {Λ Σ} `{irisG Λ Σ} : seal (@wp_def Λ Σ _). by eexists. Qed.
Instance wp' {Λ Σ} `{irisG Λ Σ} : Wp Λ (iProp Σ) stuckness := wp_aux.(unseal).
Definition wp_eq {Λ Σ} `{irisG Λ Σ} : wp = @wp_def Λ Σ _ := wp_aux.(seal_eq).
Section wp.
Context `{irisG Λ Σ}.
Context {Λ Σ} `{irisG Λ Σ}.
Implicit Types s : stuckness.
Implicit Types P : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
......@@ -252,7 +253,7 @@ End wp.
(** Proofmode class instances *)
Section proofmode_classes.
Context `{irisG Λ Σ}.
Context {Λ Σ} `{irisG Λ Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
......
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